mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case succ
q : ℚ
n✝ n : ℕ
IH : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
ifp_succ_n : IntFractPair ℚ
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
ifp_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
⊢ ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - ↑n

Tactic:
have : ifp_succ_n.fr.num < ifp_n.fr.num :=
      stream_succ_nth_fr_num_lt_nth_fr_num_rat stream_nth_eq stream_succ_nth_eq

Goal state after:
case succ
q : ℚ
n✝ n : ℕ
IH : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
ifp_succ_n : IntFractPair ℚ
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
ifp_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
this : ifp_succ_n.fr.num < ifp_n.fr.num
⊢ ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - ↑n
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝¹ : CommRing R
inst✝ : IsDomain R
h0 : P.toPoly ≠ 0
x : R
⊢ x ∈ P.roots ↔ P.a * x ^ 3 + P.b * x ^ 2 + P.c * x + P.d = 0

Tactic:
by
  rw [roots, mem_roots h0, IsRoot, toPoly]
  simp only [eval_C, eval_X, eval_add, eval_mul, eval_pow]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: case succ
K : Type u_1
v : K
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
g : GenContFract K := of v
ifp_fr_ne_zero : ifp.fr ≠ 0
n' : ℕ
stream_nth_eq : IntFractPair.stream v (n' + 1) = some ifp
conts : Pair K := g.contsAux (n' + 1 + 1)
pred_conts : Pair K := g.contsAux (n' + 1)
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
⊢ n' + 1 = 0 ∨ ¬g.TerminatedAt (n' + 1 - 1)

Tactic:
· have : IntFractPair.stream v (n' + 1) ≠ none := by simp [stream_nth_eq]
        have : ¬g.TerminatedAt n' :=
          (not_congr of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none).2 this
        exact Or.inr this

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
⊢ OrthogonalIdempotents (⇑f ∘ e)

Tactic:
by
  classical
  simp [iff_mul_eq, he.mul_eq, ← map_mul f, apply_ite f]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case some.some
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i, e i = 0
hx₂ : (∑ i, e i) * x = 0
i j : I
ne : some i ≠ some j
⊢ (some i).elim x e * (some j).elim x e = 0

Tactic:
exact he.ortho (Option.some_inj.ne.mp ne)

Goal state after:
Module: Mathlib.GroupTheory.Congruence.BigOperators

Goal state before:
pp: case nil
ι : Type u_1
M : Type u_2
inst✝ : MulOneClass M
c : Con M
f g : ι → M
h : ∀ x ∈ [], c (f x) (g x)
⊢ c (List.map f []).prod (List.map g []).prod

Tactic:
simpa only [List.map_nil, List.prod_nil] using c.refl 1

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case a
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
⊢ (matrix n I).jacobson ≤ matrix n I.jacobson

Tactic:
apply jacobson_matrix_le

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case a
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
⊢ matrix n I.jacobson ≤ (matrix n I).jacobson

Tactic:
change asIdeal (I.matrix n).jacobson ≥ asIdeal (I.jacobson.matrix n)
    simp [asIdeal_jacobson, asIdeal_matrix, Ideal.matrix_jacobson_le]

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
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
⊢ iSupIndep fun x ↦ (f.genEigenspace x) k

Tactic:
classical
  suffices ∀ μ₁ (s : Finset R), μ₁ ∉ s → Disjoint (f.genEigenspace μ₁ k)
    (s.sup fun μ ↦ f.genEigenspace μ k) by
    simp_rw [iSupIndep_iff_supIndep,
      Finset.supIndep_iff_disjoint_erase]
    exact fun s μ _ ↦ this _ _ (s.notMem_erase μ)
  intro μ₁ s
  induction s using Finset.induction_on with
  | empty => simp
  | insert μ₂ s _ ih =>
  intro hμ₁₂
  obtain ⟨hμ₁₂ : μ₁ ≠ μ₂, hμ₁ : μ₁ ∉ s⟩ := by rwa [Finset.mem_insert, not_or] at hμ₁₂
  specialize ih hμ₁
  rw [Finset.sup_insert, disjoint_iff, Submodule.eq_bot_iff]
  rintro x ⟨hx, hx'⟩
  simp only [SetLike.mem_coe] at hx hx'
  suffices x ∈ genEigenspace f μ₂ k by
    rw [← Submodule.mem_bot (R := R), ← (f.disjoint_genEigenspace hμ₁₂ k k).eq_bot]
    exact ⟨hx, this⟩
  obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.mem_sup.mp hx'; clear hx'
  let g := f - μ₂ • 1
  simp_rw [mem_genEigenspace, ← exists_prop] at hy ⊢
  peel hy with l hlk hl
  simp only [LinearMap.mem_ker] at hl
  have hyz : (g ^ l) (y + z) ∈
      (f.genEigenspace μ₁ k) ⊓ s.sup fun μ ↦ f.genEigenspace μ k := by
    refine ⟨f.mapsTo_genEigenspace_of_comm (g := g ^ l) ?_ μ₁ k hx, ?_⟩
    · exact Algebra.mul_sub_algebraMap_pow_commutes f μ₂ l
    · rw [SetLike.mem_coe, map_add, hl, zero_add]
      suffices (s.sup fun μ ↦ f.genEigenspace μ k).map (g ^ l) ≤
          s.sup fun μ ↦ f.genEigenspace μ k by exact this (Submodule.mem_map_of_mem hz)
      simp_rw [Finset.sup_eq_iSup, Submodule.map_iSup (ι := R), Submodule.map_iSup (ι := _ ∈ s)]
      refine iSup₂_mono fun μ _ ↦ ?_
      rintro - ⟨u, hu, rfl⟩
      refine f.mapsTo_genEigenspace_of_comm ?_ μ k hu
      exact Algebra.mul_sub_algebraMap_pow_commutes f μ₂ l
  rwa [ih.eq_bot, Submodule.mem_bot] at hyz

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

Goal state before:
pp: case h
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)
⊢ ↑(l₁ + l₂) ≤ k₁ + k₂ ∧
    (∑ i ∈ Finset.antidiagonal (l₁ + l₂), ⇑((l₁ + l₂).choose i.1 • ((f₁ - μ₁ • 1) ^ i.1 * (f₂ - μ₂ • 1) ^ i.2))) m = 0

Tactic:
Finset.sum_apply

Goal state after:
case h
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)
⊢ ↑(l₁ + l₂) ≤ k₁ + k₂ ∧
    ∑ c ∈ Finset.antidiagonal (l₁ + l₂), ((l₁ + l₂).choose c.1 • ((f₁ - μ₁ • 1) ^ c.1 * (f₂ - μ₂ • 1) ^ c.2)) m = 0
Module: Mathlib.Algebra.Exact.Sequence

Goal state before:
pp: k : Type u_1
inst✝¹⁸ : DivisionRing k
V₀ V₁ V₂ V₃ V₄ V₅ : Type u₀
inst✝¹⁷ : AddCommGroup V₀
inst✝¹⁶ : Module k V₀
inst✝¹⁵ : FiniteDimensional k V₀
inst✝¹⁴ : AddCommGroup V₁
inst✝¹³ : Module k V₁
inst✝¹² : FiniteDimensional k V₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : FiniteDimensional k V₂
inst✝⁸ : AddCommGroup V₃
inst✝⁷ : Module k V₃
inst✝⁶ : FiniteDimensional k V₃
inst✝⁵ : AddCommGroup V₄
inst✝⁴ : Module k V₄
inst✝³ : FiniteDimensional k V₄
inst✝² : AddCommGroup V₅
inst✝¹ : Module k V₅
inst✝ : FiniteDimensional k V₅
f₀ : V₀ →ₗ[k] V₁
f₁ : V₁ →ₗ[k] V₂
f₂ : V₂ →ₗ[k] V₃
f₃ : V₃ →ₗ[k] V₄
f₄ : V₄ →ₗ[k] V₅
inj : Injective ⇑f₀
exact₁ : Exact ⇑f₀ ⇑f₁
exact₂ : Exact ⇑f₁ ⇑f₂
exact₃ : Exact ⇑f₂ ⇑f₃
exact₄ : Exact ⇑f₃ ⇑f₄
surj : Surjective ⇑f₄
Vs : Fin (Nat.succ 0).succ.succ.succ.succ.succ → Type u₀ := ![V₀, V₁, V₂, V₃, V₄, V₅]
this✝¹ : (i : Fin 6) → AddCommGroup (Vs i) :=
  fun i ↦
    match i with
    | 0 => inst✝¹⁷
    | 1 => inst✝¹⁴
    | 2 => inst✝¹¹
    | 3 => inst✝⁸
    | 4 => inst✝⁵
    | 5 => inst✝²
this✝ : (i : Fin 6) → Module k (Vs i) :=
  fun i ↦
    match i with
    | 0 => inst✝¹⁶
    | 1 => inst✝¹³
    | 2 => inst✝¹⁰
    | 3 => inst✝⁷
    | 4 => inst✝⁴
    | 5 => inst✝¹
this : ∀ (i : Fin 6), FiniteDimensional k (Vs i)
⊢ ↑(finrank k V₀) - ↑(finrank k V₁) + ↑(finrank k V₂) - ↑(finrank k V₃) + ↑(finrank k V₄) - ↑(finrank k V₅) = 0

Tactic:
let fs (i : Fin 5) : Vs i.castSucc →ₗ[k] Vs i.succ := match i with
  | 0 => f₀ | 1 => f₁ | 2 => f₂ | 3 => f₃ | 4 => f₄

Goal state after:
k : Type u_1
inst✝¹⁸ : DivisionRing k
V₀ V₁ V₂ V₃ V₄ V₅ : Type u₀
inst✝¹⁷ : AddCommGroup V₀
inst✝¹⁶ : Module k V₀
inst✝¹⁵ : FiniteDimensional k V₀
inst✝¹⁴ : AddCommGroup V₁
inst✝¹³ : Module k V₁
inst✝¹² : FiniteDimensional k V₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : FiniteDimensional k V₂
inst✝⁸ : AddCommGroup V₃
inst✝⁷ : Module k V₃
inst✝⁶ : FiniteDimensional k V₃
inst✝⁵ : AddCommGroup V₄
inst✝⁴ : Module k V₄
inst✝³ : FiniteDimensional k V₄
inst✝² : AddCommGroup V₅
inst✝¹ : Module k V₅
inst✝ : FiniteDimensional k V₅
f₀ : V₀ →ₗ[k] V₁
f₁ : V₁ →ₗ[k] V₂
f₂ : V₂ →ₗ[k] V₃
f₃ : V₃ →ₗ[k] V₄
f₄ : V₄ →ₗ[k] V₅
inj : Injective ⇑f₀
exact₁ : Exact ⇑f₀ ⇑f₁
exact₂ : Exact ⇑f₁ ⇑f₂
exact₃ : Exact ⇑f₂ ⇑f₃
exact₄ : Exact ⇑f₃ ⇑f₄
surj : Surjective ⇑f₄
Vs : Fin (Nat.succ 0).succ.succ.succ.succ.succ → Type u₀ := ![V₀, V₁, V₂, V₃, V₄, V₅]
this✝¹ : (i : Fin 6) → AddCommGroup (Vs i) :=
  fun i ↦
    match i with
    | 0 => inst✝¹⁷
    | 1 => inst✝¹⁴
    | 2 => inst✝¹¹
    | 3 => inst✝⁸
    | 4 => inst✝⁵
    | 5 => inst✝²
this✝ : (i : Fin 6) → Module k (Vs i) :=
  fun i ↦
    match i with
    | 0 => inst✝¹⁶
    | 1 => inst✝¹³
    | 2 => inst✝¹⁰
    | 3 => inst✝⁷
    | 4 => inst✝⁴
    | 5 => inst✝¹
this : ∀ (i : Fin 6), FiniteDimensional k (Vs i)
fs : (i : Fin 5) → Vs i.castSucc →ₗ[k] Vs i.succ :=
  fun i ↦
    match i with
    | 0 => f₀
    | 1 => f₁
    | 2 => f₂
    | 3 => f₃
    | 4 => f₄
⊢ ↑(finrank k V₀) - ↑(finrank k V₁) + ↑(finrank k V₂) - ↑(finrank k V₃) + ↑(finrank k V₄) - ↑(finrank k V₅) = 0
Module: Mathlib.Algebra.DualQuaternion

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ ∀ (x y : ℍ[DualNumber R]),
    ({ re := TrivSqZeroExt.fst (x + y).re, imI := TrivSqZeroExt.fst (x + y).imI, imJ := TrivSqZeroExt.fst (x + y).imJ,
          imK := TrivSqZeroExt.fst (x + y).imK },
        { re := TrivSqZeroExt.snd (x + y).re, imI := TrivSqZeroExt.snd (x + y).imI,
          imJ := TrivSqZeroExt.snd (x + y).imJ, imK := TrivSqZeroExt.snd (x + y).imK }) =
      ({ re := TrivSqZeroExt.fst x.re, imI := TrivSqZeroExt.fst x.imI, imJ := TrivSqZeroExt.fst x.imJ,
            imK := TrivSqZeroExt.fst x.imK },
          { re := TrivSqZeroExt.snd x.re, imI := TrivSqZeroExt.snd x.imI, imJ := TrivSqZeroExt.snd x.imJ,
            imK := TrivSqZeroExt.snd x.imK }) +
        ({ re := TrivSqZeroExt.fst y.re, imI := TrivSqZeroExt.fst y.imI, imJ := TrivSqZeroExt.fst y.imJ,
            imK := TrivSqZeroExt.fst y.imK },
          { re := TrivSqZeroExt.snd y.re, imI := TrivSqZeroExt.snd y.imI, imJ := TrivSqZeroExt.snd y.imJ,
            imK := TrivSqZeroExt.snd y.imK })

Tactic:
by
    intros
    rfl

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
h : Periodic f c
hc✝ : c ≠ 0
a : α
hc : c < 0
⊢ f '' Icc (a + c) a = range f

Tactic:
← h.neg.image_Icc (neg_pos.2 hc) (a + c),

Goal state after:
case inl
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
h : Periodic f c
hc✝ : c ≠ 0
a : α
hc : c < 0
⊢ f '' Icc (a + c) a = f '' Icc (a + c) (a + c + -c)
Module: Mathlib.Algebra.FreeAlgebra.Cardinality

Goal state before:
pp: case inr
R : Type u
inst✝ : CommSemiring R
X : Type v
h✝ : Nontrivial R
⊢ #(FreeAlgebra R X) ≤ max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀

Tactic:
cases isEmpty_or_nonempty X

Goal state after:
case inr.inl
R : Type u
inst✝ : CommSemiring R
X : Type v
h✝¹ : Nontrivial R
h✝ : IsEmpty X
⊢ #(FreeAlgebra R X) ≤ max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀

case inr.inr
R : Type u
inst✝ : CommSemiring R
X : Type v
h✝¹ : Nontrivial R
h✝ : Nonempty X
⊢ #(FreeAlgebra R X) ≤ max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
B : Type u_3
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : IsIntegrallyClosedIn A B
inst✝ : Algebra.IsIntegral R A
⊢ IsIntegralClosure A R B

Tactic:
refine ⟨IsIntegralClosure.algebraMap_injective _ A _, fun {x} ↦
    ⟨fun hx ↦ IsIntegralClosure.isIntegral_iff.mp (IsIntegral.tower_top (A := A) hx), ?_⟩⟩
  rintro ⟨y, rfl⟩
  exact IsIntegral.map (IsScalarTower.toAlgHom A A B) (Algebra.IsIntegral.isIntegral y)

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

Goal state before:
pp: case hr
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 := ⋯
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
this : f %ₘ q = r * s %ₘ q
n : ℕ
x : ℕ × ℕ
⊢ r.coeff x.1 ∈ P

Tactic:
rw [mem_ker, ← coeff_map, hr, coeff_zero]

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.IntegrallyClosed

Goal state before:
pp: case h
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : p.Monic
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
a✝ : GCDMonoid R
x y : R
hg : IsUnit (gcd x y)
he : X * (algebraMap R (FractionRing R)) y = (algebraMap R (FractionRing R)) x
this✝ : y ∣ x ^ p.natDegree
this : IsUnit y
coe_map_inv : ↑((Units.map ↑(algebraMap R (FractionRing R))) this.unit)⁻¹ = (algebraMap R (FractionRing R)) ↑this.unit⁻¹
⊢ X = (algebraMap R (FractionRing R)) x * ↑((Units.map ↑(algebraMap R (FractionRing R))) this.unit)⁻¹

Tactic:
Units.eq_mul_inv_iff_mul_eq

Goal state after:
case h
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : p.Monic
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
a✝ : GCDMonoid R
x y : R
hg : IsUnit (gcd x y)
he : X * (algebraMap R (FractionRing R)) y = (algebraMap R (FractionRing R)) x
this✝ : y ∣ x ^ p.natDegree
this : IsUnit y
coe_map_inv : ↑((Units.map ↑(algebraMap R (FractionRing R))) this.unit)⁻¹ = (algebraMap R (FractionRing R)) ↑this.unit⁻¹
⊢ X * ↑((Units.map ↑(algebraMap R (FractionRing R))) this.unit) = (algebraMap R (FractionRing R)) x
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x y : R
a b : ℍ[R]
⊢ (0 * star 0).re = 0

Tactic:
by simp only [star_zero, zero_mul, re_zero]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
⊢ ker (algebraMap R (FractionRing (R ⧸ P))) = P

Tactic:
rw [IsScalarTower.algebraMap_eq R (R ⧸ P) (FractionRing (R ⧸ P))]
      rw [ker_comp_of_injective]
      · ext a; simp
      · exact FaithfulSMul.algebraMap_injective (R ⧸ P) (FractionRing (R ⧸ P))

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
q : ℚ
⊢ ↑(↑q ^ 2) = ↑↑q ^ 2

Tactic:
coe_pow

Goal state after:
R : Type u_1
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
q : ℚ
⊢ ↑↑q ^ 2 = ↑↑q ^ 2
Module: Mathlib.Algebra.Group.PNatPowAssoc

Goal state before:
pp: case succ
M : Type u_1
inst✝² : Mul M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
m k : ℕ+
hk : x ^ (m * k) = (x ^ m) ^ k
⊢ x ^ (m * k) * x ^ m = (x ^ m) ^ k * x ^ m

Tactic:
hk

Goal state after:
case succ
M : Type u_1
inst✝² : Mul M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
m k : ℕ+
hk : x ^ (m * k) = (x ^ m) ^ k
⊢ (x ^ m) ^ k * x ^ m = (x ^ m) ^ k * x ^ m
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas

Goal state before:
pp: a b x✝ : ℤ
⊢ x✝ ∈ zmultiples a ⊓ zmultiples b ↔ x✝ ∈ zmultiples ↑(a.lcm b)

Tactic:
simp [mem_zmultiples_iff, coe_lcm_dvd_iff]

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

Goal state before:
pp: case e'_3.e'_3
M : Type u_1
inst✝ : MulOneClass M
f : Set (SaturatedSubmonoid M)
x✝ : M
⊢ x✝ ∈ ⋂ s ∈ f, ↑s ↔ x✝ ∈ (sInf (toSubmonoid '' f)).1.carrier

Tactic:
simp [Submonoid.mem_sInf]

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

Goal state before:
pp: G₀ : Type u_1
H₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero H₀
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : DecidablePred fun x ↦ x = 0
m : G₀
n : H₀
⊢ Commute ((inl G₀ H₀) m) ((inr G₀ H₀) n)

Tactic:
obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit m <;>
  obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit n

Goal state after:
case inl.inl
G₀ : Type u_1
H₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero H₀
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : DecidablePred fun x ↦ x = 0
⊢ Commute ((inl G₀ H₀) 0) ((inr G₀ H₀) 0)

case inl.inr
G₀ : Type u_1
H₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero H₀
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : DecidablePred fun x ↦ x = 0
w✝ : H₀ˣ
⊢ Commute ((inl G₀ H₀) 0) ((inr G₀ H₀) ↑w✝)

case inr.inl
G₀ : Type u_1
H₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero H₀
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : DecidablePred fun x ↦ x = 0
w✝ : G₀ˣ
⊢ Commute ((inl G₀ H₀) ↑w✝) ((inr G₀ H₀) 0)

case inr.inr
G₀ : Type u_1
H₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero H₀
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : DecidablePred fun x ↦ x = 0
w✝¹ : G₀ˣ
w✝ : H₀ˣ
⊢ Commute ((inl G₀ H₀) ↑w✝¹) ((inr G₀ H₀) ↑w✝)
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✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
f : G →* S
i : ι
hi : f (v i) ≠ 1
hi' : v i⁻¹ = (v i)⁻¹
hj : f (v i) < 1
⊢ i⁻¹ ∈ {i | 1 < f (v i)} ∧ v i⁻¹ = (v i)⁻¹

Tactic:
by simpa [hi']

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

Goal state before:
pp: case inr.inr
ι : 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
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
this :
  ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_1 : LinearOrder S]
    [inst_2 : InvolutiveInv ι] [inst_3 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι),
    (∀ i ∈ s, 1 < f (v i)) →
      ∀ (i : ι),
        v i ≠ 1 →
          v i⁻¹ = (v i)⁻¹ → v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s) → v i ∈ closure (v '' s) → f (v i) ≠ 1
hi : v i ∉ closure (v '' s)
hi' : (v i)⁻¹ ∈ closure (v '' s)
⊢ f (v i) ≠ 1

Tactic:
simpa [hv_inv] using this v f s hf i⁻¹ (by simpa [hv_inv]) (by simp [hv_inv])
      (by left; simpa [hv_inv]) (by simpa [hv_inv])

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (⦋n + 1 + 1⦌.len + 1)
⊢ (Hom.toOrderHom (σ i.castSucc ≫ σ j)) k = (Hom.toOrderHom (σ j.succ ≫ σ i)) k

Tactic:
dsimp [σ]

Goal state after:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (⦋n + 1 + 1⦌.len + 1)
⊢ j.predAbove (i.castSucc.predAbove k) = i.predAbove (j.succ.predAbove k)
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
⊢ ↑((ConcreteCategory.hom (σ₀Iter i hi)) j) = 0

Tactic:
obtain rfl | hj := hj.eq_or_lt
  · rw [σ₀Iter_coe_eq_of_ge .., tsub_self]
  · exact σ₀Iter_coe_eq_of_lt ..

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case succ
j : ℕ
hj :
  ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : m + j = n),
    j < ↑i → ↑i = ↑i' + j → δ i ≫ σ₀Iter j ⋯ = σ₀Iter j ⋯ ≫ δ i'
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : m + (j + 1) = n
hi' : j + 1 < ↑i
hi'' : ↑i = ↑i' + (j + 1)
⊢ σ₀Iter j ⋯ ≫ δ i'.succ ≫ σ 0 = σ₀Iter j ⋯ ≫ σ 0 ≫ δ i'

Tactic:
dsimp% δ_comp_σ_of_gt (i := i') (j := 0)
        (by rw [Fin.lt_def]; dsimp; lia)

Goal state after:
case succ
j : ℕ
hj :
  ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : m + j = n),
    j < ↑i → ↑i = ↑i' + j → δ i ≫ σ₀Iter j ⋯ = σ₀Iter j ⋯ ≫ δ i'
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : m + (j + 1) = n
hi' : j + 1 < ↑i
hi'' : ↑i = ↑i' + (j + 1)
⊢ σ₀Iter j ⋯ ≫ σ 0 ≫ δ i' = σ₀Iter j ⋯ ≫ σ 0 ≫ δ i'
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
⊢ ∀ {X' X : Augmented C} {Y : Arrow C} (f : X' ⟶ X) (g : X ⟶ augmentedCechNerve.obj Y),
    (cechNerveEquiv X' Y).symm (f ≫ g) = Augmented.toArrow.map f ≫ (cechNerveEquiv X Y).symm g

Tactic:
by dsimp [cechNerveEquiv]; cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
i j : WidePullbackShape ι
f : i ⟶ j
⊢ (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).map f ≫
      Option.casesOn j (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none)) fun i ↦
        limit.π (Discrete.functor fun x ↦ X) { as := i }) =
    (Option.casesOn i (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none)) fun i ↦
        limit.π (Discrete.functor fun x ↦ X) { as := i }) ≫
      (wideCospan ι X).map f

Tactic:
cases f
            · cases i
              all_goals simp
            · simp only [Functor.const_obj_obj, Functor.const_obj_map, terminal.comp_from]
              subsingleton

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

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
⊢ range (A.ι ≫ f) ≤ A.image f

Tactic:
by rw [image_eq_range]

Goal state after:
Module: Mathlib.Order.Fin.Finset

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a b : α
hab : a < b
x : α
hbc : b < x
x✝ : ↥{a, b, x}
hx : x ∈ {a, b, x}
⊢ ∃ a_1, ![⟨a, ⋯⟩, ⟨b, ⋯⟩, ⟨x, ⋯⟩] a_1 = ⟨x, hx⟩

Tactic:
· exact ⟨2, rfl⟩

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

Goal state before:
pp: case mp
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
this : Function.Injective ⇑(Hom.toOrderHom (objEquiv ↑x))
a b : Fin (d + 1)
⊢ ↑x a ≤ ↑x b → a ≤ b

pp: case mpr
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
this : Function.Injective ⇑(Hom.toOrderHom (objEquiv ↑x))
a b : Fin (d + 1)
⊢ a ≤ b → ↑x a ≤ ↑x b

Tactic:
· rw [← not_lt, ← not_lt]
      intro h h'
      apply h
      obtain h'' | h'' := (monotone_apply x.val h'.le).lt_or_eq
      · assumption
      · simp only [this h'', lt_self_iff_false] at h'

Goal state after:
case mpr
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
this : Function.Injective ⇑(Hom.toOrderHom (objEquiv ↑x))
a b : Fin (d + 1)
⊢ a ≤ b → ↑x a ≤ ↑x b