mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
this✝ : Nonempty { l // ↑l ≤ k }
this : Directed (fun x1 x2 ↦ x1 ≤ x2) fun i ↦ ((f - μ • 1) ^ ↑i).ker
⊢ x ∈ (f.genEigenspace μ) k ↔ ∃ l, ↑l ≤ k ∧ x ∈ ((f - μ • 1) ^ l).ker

Tactic:
genEigenspace,

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
this✝ : Nonempty { l // ↑l ≤ k }
this : Directed (fun x1 x2 ↦ x1 ≤ x2) fun i ↦ ((f - μ • 1) ^ ↑i).ker
⊢ x ∈ { toFun := fun k ↦ ⨆ l, ⨆ (_ : ↑l ≤ k), ((f - μ • 1) ^ l).ker, monotone' := ⋯ } k ↔
    ∃ l, ↑l ≤ k ∧ x ∈ ((f - μ • 1) ^ l).ker
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
⊢ (f.genEigenspace μ) k = ⨆ l, ((f - μ • 1) ^ ↑l).ker

Tactic:
genEigenspace,

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
⊢ { toFun := fun k ↦ ⨆ l, ⨆ (_ : ↑l ≤ k), ((f - μ • 1) ^ l).ker, monotone' := ⋯ } k = ⨆ l, ((f - μ • 1) ^ ↑l).ker
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case inl
R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon R
i j : n
x y : R
h : c x y
i' j' : n
hi : i ≠ i'
⊢ c (Matrix.single i j x i' j') (Matrix.single i j y i' j')

pp: case inr
R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon R
i j : n
x y : R
h : c x y
j' : n
⊢ c (Matrix.single i j x i j') (Matrix.single i j y i j')

Tactic:
· simpa [hi] using c.refl 0

Goal state after:
case inr
R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon R
i j : n
x y : R
h : c x y
j' : n
⊢ c (Matrix.single i j x i j') (Matrix.single i j y i j')
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
s : Finset I
⊢ ∏ i ∈ s, (1 - e i) = 1 - ∑ i ∈ s, e i

Tactic:
by
  induction s using Finset.cons_induction with
  | empty => simp
  | cons a s has ih =>
    simp [ih, sub_mul, mul_sub, he.mul_sum_of_notMem has, sub_sub]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
h : f.HasUnifEigenvector μ k x
⊢ (f.genEigenspace μ) k ≠ ⊥

Tactic:
Submodule.ne_bot_iff

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
h : f.HasUnifEigenvector μ k x
⊢ ∃ x ∈ (f.genEigenspace μ) k, x ≠ 0
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
h : f.HasUnifEigenvalue μ 1
n : ℕ
⊢ ((f ^ n).genEigenspace (μ ^ n)) 1 ≠ ⊥

Tactic:
Submodule.ne_bot_iff

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
h : f.HasUnifEigenvalue μ 1
n : ℕ
⊢ ∃ x ∈ ((f ^ n).genEigenspace (μ ^ n)) 1, x ≠ 0
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
hμ : f.HasUnifEigenvalue μ 1
⊢ μ ∈ spectrum R f

Tactic:
refine spectrum.mem_iff.mpr fun h_unit ↦ ?_
  set f' := LinearMap.GeneralLinearGroup.toLinearEquiv h_unit.unit
  rcases hμ.exists_hasUnifEigenvector with ⟨v, hv⟩
  refine hv.2 ((LinearMap.ker_eq_bot'.mp f'.ker) v (?_ : μ • v - f v = 0))
  rw [hv.apply_eq_smul, sub_self]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
n : ℕ∞
x : M
hx : ∃ l, ↑l ≤ n ∧ ((f - μ • 1) ^ l) x = 0
⊢ ∃ l, ↑l ≤ n ∧ ((f - μ • 1) ^ l) (f x) = 0

Tactic:
obtain ⟨k, hk, hx⟩ := hx

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
n : ℕ∞
x : M
k : ℕ
hk : ↑k ≤ n
hx : ((f - μ • 1) ^ k) x = 0
⊢ ∃ l, ↑l ≤ n ∧ ((f - μ • 1) ^ l) (f x) = 0
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset M
b : Basis (↥s) R M
f : M →ₗ[R] M
this : ∃ s, Nonempty (Basis (↥s) R M)
⊢ (trace R M) f = ((toMatrix b b) f).trace

Tactic:
trace,

Goal state after:
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset M
b : Basis (↥s) R M
f : M →ₗ[R] M
this : ∃ s, Nonempty (Basis (↥s) R M)
⊢ (if H : ∃ s, Nonempty (Basis (↥s) R M) then traceAux R ⋯.some else 0) f = ((toMatrix b b) f).trace
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := (f.genEigenspace μ₁) ↑k ⊓ (f.genEigenspace μ₂) ↑l
hp : Nontrivial ↥p
f₁ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₁) ⋯
f₂ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₂) ⋯
this : IsNilpotent (f₂ - f₁)
hf₁₂ : f₂ - f₁ = (algebraMap R (End R ↥p)) (μ₁ - μ₂)
⊢ False

Tactic:
rw [hf₁₂, IsNilpotent.map_iff (FaithfulSMul.algebraMap_injective R (End R p)),
    isNilpotent_iff_eq_zero, sub_eq_zero] at this

Goal state after:
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := (f.genEigenspace μ₁) ↑k ⊓ (f.genEigenspace μ₂) ↑l
hp : Nontrivial ↥p
f₁ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₁) ⋯
f₂ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₂) ⋯
this : μ₁ = μ₂
hf₁₂ : f₂ - f₁ = (algebraMap R (End R ↥p)) (μ₁ - μ₂)
⊢ False
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k l : ℕ∞
⊢ Disjoint ((f.genEigenspace μ₁) k) ((f.genEigenspace μ₂) l)

Tactic:
rw [genEigenspace_eq_iSup_genEigenspace_nat, genEigenspace_eq_iSup_genEigenspace_nat]
  simp_rw [genEigenspace_directed.disjoint_iSup_left, genEigenspace_directed.disjoint_iSup_right]
  rintro ⟨k, -⟩ ⟨l, -⟩
  nontriviality M
  rw [disjoint_iff]
  set p := f.genEigenspace μ₁ k ⊓ f.genEigenspace μ₂ l
  by_contra hp
  replace hp : Nontrivial p := Submodule.nontrivial_iff_ne_bot.mpr hp
  let f₁ : End R p := (f - algebraMap R (End R M) μ₁).restrict <| MapsTo.inter_inter
    (mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f μ₁) μ₁ k)
    (mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f μ₁) μ₂ l)
  let f₂ : End R p := (f - algebraMap R (End R M) μ₂).restrict <| MapsTo.inter_inter
    (mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f μ₂) μ₁ k)
    (mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f μ₂) μ₂ l)
  have : IsNilpotent (f₂ - f₁) := by
    apply Commute.isNilpotent_sub (x := f₂) (y := f₁) _
      (isNilpotent_restrict_of_le inf_le_right _)
      (isNilpotent_restrict_of_le inf_le_left _)
    · ext; simp [f₁, f₂, smul_sub, sub_sub, smul_comm μ₁, add_sub_left_comm]
    · apply mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f _)
    · apply isNilpotent_restrict_genEigenspace_nat
    · apply mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f _)
    apply isNilpotent_restrict_genEigenspace_nat
  have hf₁₂ : f₂ - f₁ = algebraMap R (End R p) (μ₁ - μ₂) := by ext; simp [f₁, f₂]
  rw [hf₁₂, IsNilpotent.map_iff (FaithfulSMul.algebraMap_injective R (End R p)),
    isNilpotent_iff_eq_zero, sub_eq_zero] at this
  contradiction

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: case neg
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
H : ¬∃ s, Nonempty (Basis (↥s) R M)
⊢ (trace R M) (f * g) = (trace R M) (g * f)

Tactic:
trace,

Goal state after:
case neg
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
H : ¬∃ s, Nonempty (Basis (↥s) R M)
⊢ (if H : ∃ s, Nonempty (Basis (↥s) R M) then traceAux R ⋯.some else 0) (f * g) =
    (if H : ∃ s, Nonempty (Basis (↥s) R M) then traceAux R ⋯.some else 0) (g * f)
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
x : ↥p
this : ∀ (l : ℕ), (genEigenspace (LinearMap.restrict f hfp) μ) ↑l = Submodule.comap p.subtype ((f.genEigenspace μ) ↑l)
⊢ (∃ l, ↑l ≤ k ∧ p.subtype x ∈ (f.genEigenspace μ) ↑l) ↔ p.subtype x ∈ (f.genEigenspace μ) k

Tactic:
mem_genEigenspace (k := k),

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
x : ↥p
this : ∀ (l : ℕ), (genEigenspace (LinearMap.restrict f hfp) μ) ↑l = Submodule.comap p.subtype ((f.genEigenspace μ) ↑l)
⊢ (∃ l, ↑l ≤ k ∧ p.subtype x ∈ (f.genEigenspace μ) ↑l) ↔ ∃ l, ↑l ≤ k ∧ p.subtype x ∈ ((f - μ • 1) ^ l).ker
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
x : ↥p
this : ∀ (l : ℕ), (genEigenspace (LinearMap.restrict f hfp) μ) ↑l = Submodule.comap p.subtype ((f.genEigenspace μ) ↑l)
⊢ x ∈ (genEigenspace (LinearMap.restrict f hfp) μ) k ↔ x ∈ Submodule.comap p.subtype ((f.genEigenspace μ) k)

Tactic:
by
    simp_rw [mem_genEigenspace, ← mem_genEigenspace_nat, this,
      Submodule.mem_comap, mem_genEigenspace (k := k), mem_genEigenspace_nat]

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
hM : ¬∃ s, Nonempty (Basis (↥s) R M)
⊢ (trace R N) (e.conj f) = (trace R M) f

Tactic:
trace,

Goal state after:
case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
hM : ¬∃ s, Nonempty (Basis (↥s) R M)
⊢ (if H : ∃ s, Nonempty (Basis (↥s) R N) then traceAux R ⋯.some else 0) (e.conj f) = (trace R M) f
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
hM : ¬∃ s, Nonempty (Basis (↥s) R M)
⊢ (if H : ∃ s, Nonempty (Basis (↥s) R N) then traceAux R ⋯.some else 0) (e.conj f) = (trace R M) f

Tactic:
trace,

Goal state after:
case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
hM : ¬∃ s, Nonempty (Basis (↥s) R M)
⊢ (if H : ∃ s, Nonempty (Basis (↥s) R N) then traceAux R ⋯.some else 0) (e.conj f) =
    (if H : ∃ s, Nonempty (Basis (↥s) R M) then traceAux R ⋯.some else 0) f
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case h.right.inr
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
m : M
l₁ : ℕ
hlk₁ : ↑l₁ ≤ k₁
hl₁ : ((f₁ - μ₁ • 1) ^ l₁) m = 0
l₂ : ℕ
hlk₂ : ↑l₂ ≤ k₂
hl₂ : ((f₂ - μ₂ • 1) ^ l₂) m = 0
this : f₁ + f₂ - (μ₁ + μ₂) • 1 = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)
h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1)
x✝ : ℕ × ℕ
i j : ℕ
hij : (i, j).1 + (i, j).2 = l₁ + l₂
hj : l₂ ≤ j
⊢ ((f₁ - μ₁ • 1) ^ i * (f₂ - μ₂ • 1) ^ j) m = 0

Tactic:
· rw [Module.End.mul_apply, Module.End.pow_map_zero_of_le hj hl₂, map_zero]

Goal state after:
Module: Mathlib.Algebra.Field.ModEq

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
a b c p : K
hc : c ≠ 0
⊢ a * c ≡ b * c [PMOD p] ↔ a / c⁻¹ ≡ b / c⁻¹ [PMOD p]

Tactic:
div_inv_eq_mul,

Goal state after:
K : Type u_1
inst✝ : DivisionSemiring K
a b c p : K
hc : c ≠ 0
⊢ a * c ≡ b * c [PMOD p] ↔ a * c ≡ b / c⁻¹ [PMOD p]
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case mk
α : Type u_1
inst✝ : DecidableEq α
x : FreeGroup α
L : List (α × Bool)
⊢ (mk (invRev L)).toWord = invRev (mk L).toWord

Tactic:
toWord_mk,

Goal state after:
case mk
α : Type u_1
inst✝ : DecidableEq α
x : FreeGroup α
L : List (α × Bool)
⊢ reduce (invRev L) = invRev (mk L).toWord
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case mk
α : Type u_1
inst✝ : DecidableEq α
x : FreeGroup α
L : List (α × Bool)
⊢ reduce (invRev L) = invRev (mk L).toWord

Tactic:
toWord_mk,

Goal state after:
case mk
α : Type u_1
inst✝ : DecidableEq α
x : FreeGroup α
L : List (α × Bool)
⊢ reduce (invRev L) = invRev (reduce L)
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
L₁ L₂ : List (α × Bool)
inst✝ : DecidableEq α
⊢ reduce (reduce L₁ ++ reduce L₂) = reduce ((mk L₁).toWord ++ (mk L₂).toWord)

Tactic:
toWord_mk,

Goal state after:
α : Type u_1
L₁ L₂ : List (α × Bool)
inst✝ : DecidableEq α
⊢ reduce (reduce L₁ ++ reduce L₂) = reduce (reduce L₁ ++ (mk L₂).toWord)
Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup

Goal state before:
pp: case inr
α : Type u_1
x : FreeMonoid α
b : α
y : FreeSemigroup α
⊢ FreeMonoid.of b * toFreeMonoid y = 1 ∨ ∃ y_1, toFreeMonoid y_1 = FreeMonoid.of b * toFreeMonoid y

Tactic:
exact Or.inr ⟨of b * y, by simp⟩

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n✝ : ℕ
i : n✝ < p.natDegree
⊢ p.coeff n✝ * x ^ (p.natDegree - n✝) ∈ P

Tactic:
← tsub_pos_iff_lt

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n✝ : ℕ
i : 0 < p.natDegree - n✝
⊢ p.coeff n✝ * x ^ (p.natDegree - n✝) ∈ P
Module: Mathlib.Algebra.Group.Action.Option

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
inst✝² : SMul M α
inst✝¹ : SMul N α
a : M
b✝ : α
x : Option α
inst✝ : FaithfulSMul M α
m₁✝ m₂✝ : M
h : ∀ (a : Option α), m₁✝ • a = m₂✝ • a
b : α
⊢ m₁✝ • b = m₂✝ • b

Tactic:
by injection h (some b)

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n + s
hs : map (algebraMap R K) s = 0
hn0 : n = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n = 0
⊢ q ∣ C g.leadingCoeff * q ^ m * s

Tactic:
exact ((dvd_pow_self q hm).mul_left _).mul_right _

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: case of_mul
M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x x₁ x₂ : M
hxy✝ : x₁ * x₂ ∈ s.saturation
ih : ∃ y, x₁ * x₂ * y ∈ s
⊢ (∃ y, x₁ * y ∈ s) ∧ ∃ y, x₂ * y ∈ s

Tactic:
exact ih.elim fun y h ↦ ⟨⟨x₂ * y, by rwa [← mul_assoc]⟩,
      ⟨x₁ * y, by rwa [mul_left_comm, ← mul_assoc]⟩⟩

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x : M
⊢ x ∈ s.saturation ↔ ∃ y, x * y ∈ s

Tactic:
by
  refine ⟨fun h ↦ ?_, fun ⟨y, hxy⟩ ↦ (s.saturation.2 <| le_toSubmonoid_saturation hxy).1⟩
  induction h using saturation_induction with
  | mem _ hx => exact ⟨1, by simpa⟩
  | mul _ _ _ _ ih₁ ih₂ =>
    exact ih₁.elim fun y₁ h₁ ↦ ih₂.elim fun y₂ h₂ ↦
      ⟨y₁ * y₂, by rw [mul_mul_mul_comm]; exact mul_mem h₁ h₂⟩
  | of_mul x₁ x₂ _ ih =>
    exact ih.elim fun y h ↦ ⟨⟨x₂ * y, by rwa [← mul_assoc]⟩,
      ⟨x₁ * y, by rwa [mul_left_comm, ← mul_assoc]⟩⟩

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
this :
  ⇑invMonoidHom '' v '' baseOf v ((invMonoidHom.comp invMonoidHom).comp f) ⊆
    ⇑invMonoidHom '' ⇑invMonoidHom ∘ v '' baseOf v (invMonoidHom.comp f)
⊢ ⇑invMonoidHom ∘ v '' baseOf v f ⊆ v '' baseOf v (invMonoidHom.comp f)

Tactic:
invMonoidHom_comp_invMonoidHom,

Goal state after:
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
this :
  ⇑invMonoidHom '' v '' baseOf v ((MonoidHom.id S).comp f) ⊆
    ⇑invMonoidHom '' ⇑invMonoidHom ∘ v '' baseOf v (invMonoidHom.comp f)
⊢ ⇑invMonoidHom ∘ v '' baseOf v f ⊆ v '' baseOf v (invMonoidHom.comp f)
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
this : ⇑invMonoidHom '' v '' baseOf v f ⊆ ⇑(invMonoidHom.comp invMonoidHom) '' v '' baseOf v (invMonoidHom.comp f)
⊢ ⇑invMonoidHom ∘ v '' baseOf v f ⊆ v '' baseOf v (invMonoidHom.comp f)

Tactic:
invMonoidHom_comp_invMonoidHom,

Goal state after:
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
this : ⇑invMonoidHom '' v '' baseOf v f ⊆ ⇑(MonoidHom.id G) '' v '' baseOf v (invMonoidHom.comp f)
⊢ ⇑invMonoidHom ∘ v '' baseOf v f ⊆ v '' baseOf v (invMonoidHom.comp f)
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
a : α
inst✝ : Fintype β
ha : a ≠ 0
⊢ a • Set.univ = Set.univ

Tactic:
exact Set.smul_set_univ₀ ha

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroClass β
zero : Zero α := e.zero
mul : Mul α := e.mul
⊢ MulZeroClass α

Tactic:
apply e.injective.mulZeroClass _ <;> intros

Goal state after:
case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroClass β
zero : Zero α := ⋯
mul : Mul α := ⋯
⊢ e 0 = 0

case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroClass β
zero : Zero α := e.zero
mul : Mul α := e.mul
a✝ b✝ : α
⊢ e (a✝ * b✝) = e a✝ * e b✝
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
r₁ s₁ r₂ s₂ : A
hr₁ : f r₁ ≠ 0
hs₁ : f s₁ ≠ 0
hr₂ : f r₂ ≠ 0
hs₂ : f s₂ ≠ 0
⊢ Units.mk0 (f s₂) hs₂ * Units.mk0 (f r₁) hr₁ = Units.mk0 (f s₁) hs₁ * Units.mk0 (f r₂) hr₂ ↔ f r₁ * f s₂ = f r₂ * f s₁

Tactic:
simp [Units.ext_iff, mul_comm (f r₂), mul_comm (f s₂)]

Goal state after:
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun x ↦ a₁, monotone' := ⋯ }
g₂ : X ⟶ A := ofHom { toFun := fun x ↦ a₂, monotone' := ⋯ }
eq : g₁ ≫ f = g₂ ≫ f
⊢ (ConcreteCategory.hom g₁) { down := 0 } = (ConcreteCategory.hom g₂) { down := 0 }

Tactic:
cancel_mono

Goal state after:
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun x ↦ a₁, monotone' := ⋯ }
g₂ : X ⟶ A := ofHom { toFun := fun x ↦ a₂, monotone' := ⋯ }
eq : g₁ = g₂
⊢ (ConcreteCategory.hom g₁) { down := 0 } = (ConcreteCategory.hom g₂) { down := 0 }
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: case refine_1
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y.toLinOrd), Nonempty ↑(⇑(ConcreteCategory.hom f) ⁻¹' {y})
φ : ↑Y.toLinOrd → ↑X.toLinOrd := fun y ↦ ↑⋯.some
hφ : ∀ (y : ↑Y.toLinOrd), (ConcreteCategory.hom f) (φ y) = y
a b : ↑Y.1
⊢ a ≤ b → φ a ≤ φ b

Tactic:
contrapose

Goal state after:
case refine_1
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y.toLinOrd), Nonempty ↑(⇑(ConcreteCategory.hom f) ⁻¹' {y})
φ : ↑Y.toLinOrd → ↑X.toLinOrd := ⋯
hφ : ∀ (y : ↑Y.toLinOrd), (ConcreteCategory.hom f) (φ y) = y
a b : ↑Y.1
⊢ ¬φ a ≤ φ b → ¬a ≤ b
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ i = (i ≫ e) ≫ i

Tactic:
h₁,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ i = 𝟙 Y ≫ i
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case h.left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ε.functor.map (i ≫ e) = 𝟙 (ε.functor.obj Y)

Tactic:
h₁,

Goal state after:
case h.left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ε.functor.map (𝟙 Y) = 𝟙 (ε.functor.obj Y)
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i n m : ℕ
h : n + i = m
⊢ σ₀Iter (i + 1) ⋯ = σ 0 ≫ σ₀Iter i h

Tactic:
by
  induction i generalizing n m with
  | zero =>
    obtain rfl : n = m := by lia
    simp
  | succ i hi' =>
    rw [σ₀Iter_succ, hi' (by lia), σ₀Iter_succ, Category.assoc]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
inst✝¹ : Epi f₁
y₁ : ↑(X.nonDegenerate m₁)
hy₁ : x = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
inst✝ : Epi f₂
y₂ : ↑(X.nonDegenerate m₂)
hy₂ : x = (ConcreteCategory.hom (X.map f₂.op)) ↑y₂
hf₁ : SplitEpi f₁
⊢ m₁ = m₂

Tactic:
obtain ⟨⟨hf₂⟩⟩ := isSplitEpi_of_epi f₂

Goal state after:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
inst✝¹ : Epi f₁
y₁ : ↑(X.nonDegenerate m₁)
hy₁ : x = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
inst✝ : Epi f₂
y₂ : ↑(X.nonDegenerate m₂)
hy₂ : x = (ConcreteCategory.hom (X.map f₂.op)) ↑y₂
hf₁ : SplitEpi f₁
hf₂ : SplitEpi f₂
⊢ m₁ = m₂