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

Goal state before:
pp: K : Type u_1
g : GenContFract K
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? (n' + 1) = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt (n' + 1)
s_nth_eq : g.s.get? (n' + 1) = some { a := a, b := b }
pa pb : K
s_n'th_eq : g.s.get? n' = some { a := pa, b := pb }
g' : GenContFract K := g.squashGCF (n' + 1)
pred_conts : Pair K := g.contsAux (n' + 1)
succ_n'th_contsAux_eq : pred_conts = g.contsAux (n' + 1)
ppred_conts : Pair K := g.contsAux n'
n'th_contsAux_eq : ppred_conts = g.contsAux n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := g'.contsAux (n' + 1)
succ_n'th_contsAux_eq' : pred_conts' = g'.contsAux (n' + 1)
ppred_conts' : Pair K := g'.contsAux n'
n'th_contsAux_eq' : ppred_conts' = g'.contsAux n'
pA' : K := pred_conts'.a
pB' : K := pred_conts'.b
ppA' : K := ppred_conts'.a
ppB' : K := ppred_conts'.b
this✝¹ : g'.convs (n' + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')
this✝ : g.convs (n' + 2) = (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB)
this :
  ((pb + a / b) * pA + pa * ppA) / ((pb + a / b) * pB + pa * ppB) =
    (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB)
⊢ (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB) =
    ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')

Tactic:
by
        obtain ⟨eq1, eq2, eq3, eq4⟩ : pA' = pA ∧ pB' = pB ∧ ppA' = ppA ∧ ppB' = ppB := by
          simp [*, g', pA, pB, ppA, ppB, pA', pB', ppA', ppB',
            (contsAux_eq_contsAux_squashGCF_of_le <| le_refl <| n' + 1).symm,
            (contsAux_eq_contsAux_squashGCF_of_le n'.le_succ).symm]
        symm
        simpa only [eq1, eq2, eq3, eq4, mul_div_cancel_right₀ _ b_ne_zero]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case succ.inl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
n : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b) → g.convs n = g.convs' n
g : GenContFract K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n + 1 → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF n
terminatedAt_n : g.TerminatedAt n
g'_eq_g : g' = g
⊢ g.convs (n + 1) = g'.convs' n

Tactic:
convs_stable_of_terminated n.le_succ terminatedAt_n,

Goal state after:
case succ.inl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
n : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b) → g.convs n = g.convs' n
g : GenContFract K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n + 1 → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF n
terminatedAt_n : g.TerminatedAt n
g'_eq_g : g' = g
⊢ g.convs n = g'.convs' n
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: case inr.a
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
n : ℕ
hn : 3 < n
⊢ 3 < ↑n

Tactic:
simpa using hn

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

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : ↑(fib (n + 1)) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
this✝ : 1 / den' ≤ 1 / den
this : |(-1) ^ n / den'| = 1 / den'
⊢ |(-1) ^ n / den'| ≤ 1 / den

Tactic:
rwa [this]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case refine_4
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ 0 * e' = 0

Tactic:
zero_mul

Goal state after:
case refine_4
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this✝ : (e₁ - e₂) ^ 3 = e₁ - e₂
n : ℕ
hn : (e₁ - e₂) ^ n = 0
this : e₁ - e₂ = 0
⊢ e₁ = e₂

Tactic:
sub_eq_zero

Goal state after:
R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this✝ : (e₁ - e₂) ^ 3 = e₁ - e₂
n : ℕ
hn : (e₁ - e₂) ^ n = 0
this : e₁ = e₂
⊢ e₁ = e₂
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
this : ∀ (s : Finset I), (∏ i ∈ s, (1 - e i)) * x = x
⊢ 0 * x = 0

Tactic:
zero_mul

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
this : ∀ (s : Finset I), (∏ i ∈ s, (1 - e i)) * x = x
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
w✝ x✝² y✝ z✝ : R
h₁ : ∀ (i j : n), c (single i j w✝) (single i j x✝²)
h₂ : ∀ (i j : n), c (single i j y✝) (single i j z✝)
x✝¹ x✝ : n
⊢ c (single x✝¹ x✝ (w✝ + y✝)) (single x✝¹ x✝ (x✝² + z✝))

Tactic:
simpa [single_add] using c.add (h₁ _ _) (h₂ _ _)

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

Goal state before:
pp: K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
a b : K
hb : b ≠ 0
⊢ (f - b⁻¹ • a • 1).ker = (b • (f - b⁻¹ • a • 1)).ker

Tactic:
by rw [LinearMap.ker_smul _ b hb]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case refine_1.some.some
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
I : Type u_3
inst✝ : Fintype I
f : R →+* S
e₀ : R
he₀ : IsIdempotentElem e₀
hfe₀ : RingHom.ker f = Ideal.span {e₀}
e : I → S
he : CompleteOrthogonalIdempotents e
e' : I → R
he' : ∀ (i : I), f (e' i) = e i
k✝ : I → R
hk✝ : ∀ (i : I), e' i * e' i - e' i = e₀ * k✝ i
i j : I
h : some i ≠ some j
k : R
hk : e' i * e' j = e₀ * k
⊢ 0 * k = 0

Tactic:
zero_mul

Goal state after:
case refine_1.some.some
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
I : Type u_3
inst✝ : Fintype I
f : R →+* S
e₀ : R
he₀ : IsIdempotentElem e₀
hfe₀ : RingHom.ker f = Ideal.span {e₀}
e : I → S
he : CompleteOrthogonalIdempotents e
e' : I → R
he' : ∀ (i : I), f (e' i) = e i
k✝ : I → R
hk✝ : ∀ (i : I), e' i * e' i - e' i = e₀ * k✝ i
i j : I
h : some i ≠ some j
k : R
hk : e' i * e' j = e₀ * k
⊢ 0 = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
a✝ : e * r = r
⊢ r * e = r

Tactic:
rwa [← hc.comm]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : NonUnitalSemiring R
⊢ 0 * e = 0

Tactic:
zero_mul

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e✝ : R
I : Type u_2
inst✝¹ : Fintype I
e : I → R
inst✝ : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : (i : I) → ⋯.Corner
i j : I
a✝ : j ∈ Finset.univ
ne : j ≠ i
r' : R
eq : (fun x ↦ e j * x * e j) r' = ↑(r j)
⊢ 0 * r' * e j * e i = 0

Tactic:
zero_mul

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
μ₁ μ₂ : 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 : μ₁ - μ₂ = 0
hf₁₂ : f₂ - f₁ = (algebraMap R (End R ↥p)) (μ₁ - μ₂)
⊢ False

Tactic:
sub_eq_zero

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.Algebra.Exact.Sequence

Goal state before:
pp: k : Type u_1
inst✝¹⁸ : DivisionRing k
V₀ : Type u₀
inst✝¹⁷ : AddCommGroup V₀
inst✝¹⁶ : Module k V₀
inst✝¹⁵ : FiniteDimensional k V₀
V₁ : Type u₁
inst✝¹⁴ : AddCommGroup V₁
inst✝¹³ : Module k V₁
inst✝¹² : FiniteDimensional k V₁
V₂ : Type u₂
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : FiniteDimensional k V₂
V₃ : Type u₃
inst✝⁸ : AddCommGroup V₃
inst✝⁷ : Module k V₃
inst✝⁶ : FiniteDimensional k V₃
V₄ : Type u₄
inst✝⁵ : AddCommGroup V₄
inst✝⁴ : Module k V₄
inst✝³ : FiniteDimensional k V₄
V₅ : Type u₅
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₄
W₀ : Type (max u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₀} V₀
W₁ : Type (max u₁ u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₁} V₁
W₂ : Type (max u₂ u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₂} V₂
W₃ : Type (max u₃ u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₃} V₃
W₄ : Type (max u₄ u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₄} V₄
W₅ : Type (max u₅ u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₅} V₅
⊢ ↑(finrank k V₀) - ↑(finrank k V₁) + ↑(finrank k V₂) - ↑(finrank k V₃) + ↑(finrank k V₄) - ↑(finrank k V₅) = 0

Tactic:
let g₀ : W₀ →ₗ[k] W₁ := ULift.moduleEquiv.symm.toLinearMap ∘ₗ f₀ ∘ₗ ULift.moduleEquiv.toLinearMap

Goal state after:
k : Type u_1
inst✝¹⁸ : DivisionRing k
V₀ : Type u₀
inst✝¹⁷ : AddCommGroup V₀
inst✝¹⁶ : Module k V₀
inst✝¹⁵ : FiniteDimensional k V₀
V₁ : Type u₁
inst✝¹⁴ : AddCommGroup V₁
inst✝¹³ : Module k V₁
inst✝¹² : FiniteDimensional k V₁
V₂ : Type u₂
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : FiniteDimensional k V₂
V₃ : Type u₃
inst✝⁸ : AddCommGroup V₃
inst✝⁷ : Module k V₃
inst✝⁶ : FiniteDimensional k V₃
V₄ : Type u₄
inst✝⁵ : AddCommGroup V₄
inst✝⁴ : Module k V₄
inst✝³ : FiniteDimensional k V₄
V₅ : Type u₅
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₄
W₀ : Type (max u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₀} V₀
W₁ : Type (max u₁ u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₁} V₁
W₂ : Type (max u₂ u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₂} V₂
W₃ : Type (max u₃ u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₃} V₃
W₄ : Type (max u₄ u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₄} V₄
W₅ : Type (max u₅ u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₅} V₅
g₀ : W₀ →ₗ[k] W₁ := ↑ULift.moduleEquiv.symm ∘ₗ f₀ ∘ₗ ↑ULift.moduleEquiv
⊢ ↑(finrank k V₀) - ↑(finrank k V₁) + ↑(finrank k V₂) - ↑(finrank k V₃) + ↑(finrank k V₄) - ↑(finrank k V₅) = 0
Module: Mathlib.Algebra.FreeAlgebra.Cardinality

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
X : Type v
inst✝¹ : Nonempty X
inst✝ : Nontrivial R
hX : #(FreeMonoid X) = max #X ℵ₀
⊢ max (Cardinal.lift.{v, u} #R) (max (Cardinal.lift.{u, v} #X) ℵ₀) =
    max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀

Tactic:
sup_assoc

Goal state after:
R : Type u
inst✝² : CommSemiring R
X : Type v
inst✝¹ : Nonempty X
inst✝ : Nontrivial R
hX : #(FreeMonoid X) = max #X ℵ₀
⊢ max (Cardinal.lift.{v, u} #R) (max (Cardinal.lift.{u, v} #X) ℵ₀) =
    max (Cardinal.lift.{v, u} #R) (max (Cardinal.lift.{u, v} #X) ℵ₀)
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
inj : Function.Injective ⇑(algebraMap R A)
cl : ∀ {x : A}, IsIntegral R x → ∃ y, (algebraMap R A) y = x
⊢ IsIntegrallyClosedIn R A

Tactic:
refine ⟨inj, by simp_all, ?_⟩

Goal state after:
case mpr
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
inj : Function.Injective ⇑(algebraMap R A)
cl : ∀ {x : A}, IsIntegral R x → ∃ y, (algebraMap R A) y = x
x✝ : A
⊢ (∃ y, (algebraMap R A) y = x✝) → IsIntegral R x✝
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
⊢ (p.scaleRoots x).IsWeaklyEisensteinAt P

Tactic:
refine ⟨fun i => ?_⟩
  rw [coeff_scaleRoots]
  rw [natDegree_scaleRoots, ← tsub_pos_iff_lt] at i
  exact Ideal.mul_mem_left _ _ (Ideal.pow_mem_of_mem P hP _ i)

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ : R
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
⊢ Module.rank R ℍ[R,c₁,c₂,c₃] = 4

Tactic:
rank_eq_card_basis (basisOneIJK c₁ c₂ c₃),

Goal state after:
R : Type u_3
c₁ c₂ c₃ : R
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
⊢ ↑(Fintype.card (Fin 4)) = 4
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case hs
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 : ℕ × ℕ
⊢ s.coeff x.2 ∈ P

Tactic:
· rw [mem_ker, ← coeff_map, hs, coeff_zero]

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
⊢ f %ₘ q = r * s %ₘ q

Tactic:
rw [h_eq, hg, hh]

Goal state after:
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
⊢ (C g.leadingCoeff * q ^ m + r) * (C h.leadingCoeff * q ^ n + s) %ₘ q = r * s %ₘ q
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
c₁ c₂ c₃ : R
inst✝ : Infinite R
⊢ #ℍ[R,c₁,c₂,c₃] = #R

Tactic:
by
  rw [mk_quaternionAlgebra, pow_four]

Goal state after:
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
⊢ Δ_[1]^[P.natDegree] (fun x ↦ eval x P) x = (P.leadingCoeff • ↑P.natDegree !) x

Tactic:
simp_rw [P.eval_eq_sum_range, ← sum_apply _ _ (fun i x ↦ P.coeff i * x ^ i),
    fwdDiff_iter_finsetSum, ← smul_eq_mul, ← Pi.smul_def, fwdDiff_iter_const_smul, Pi.smul_apply]

Goal state after:
R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
⊢ (∑ x ∈ range (P.natDegree + 1), P.coeff x • Δ_[1]^[P.natDegree] fun i ↦ i ^ x) x = P.leadingCoeff • ↑P.natDegree ! x
Module: Mathlib.Algebra.GroupWithZero.Action.Center

Goal state before:
pp: case inl
G₀ : Type u_1
inst✝ : GroupWithZero G₀
u : ↥(center G₀ˣ)
⊢ 0 * ↑↑u = 0

Tactic:
zero_mul

Goal state after:
case inl
G₀ : Type u_1
inst✝ : GroupWithZero G₀
u : ↥(center G₀ˣ)
⊢ 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
x : f.ValueGroup₀
u : Bˣ
hu : u ∈ f.valueGroup
⊢ ∃ a, (restrict₀ f) a = some ⟨u, hu⟩

Tactic:
change u ∈ (valueGroup f : Set Bˣ) at hu
    rw [← valueMonoid_eq_valueGroup'] at hu
    obtain ⟨v, hv⟩ := hu
    use v
    simp [restrict₀_apply, hv, Units.ne_zero, WithZero.coe]

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
⊢ { f // ((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj X).d 1 0 ≫ f = 0 }

Tactic:
refine ⟨X.hom.app (op ⦋0⦌), ?_⟩

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
⊢ ((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj X).d 1 0 ≫ X.hom.app (op ⦋0⦌) = 0
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

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

Tactic:
by
  refine ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)
  ext
  rw [dsimp% ConcreteCategory.comp_apply (δ 0) (δ₀Iter i), coe_δ,
    δ₀Iter_apply .., δ₀Iter_apply ..]
  dsimp
  lia

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 : n + j = m),
    ↑i' = ↑i + j → δ₀Iter j h ≫ δ i' = δ i ≫ δ₀Iter j ⋯
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : n + (j + 1) = m
hi'' : ↑i' = ↑i + (j + 1)
⊢ δ 0 ≫ δ₀Iter j ⋯ ≫ δ i' = δ i ≫ δ₀Iter (j + 1) ⋯

Tactic:
δ₀Iter_succ' ..,

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
n : ℕ
⊢ F.map (H.h (Fin.last n)) ≫ (((whiskering C D).obj F).obj Y).δ (Fin.last (n + 1)) =
    (((whiskering C D).obj F).map f).app (op ⦋n⦌)

Tactic:
by
    simpa [SimplicialObject.δ] using!
      congrArg (fun k => F.map k) (H.h_last_comp_δ_last n)

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

Goal state before:
pp: case left
X✝¹ Y✝ : SSet
f : X✝¹ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
X✝ : SimplexCategoryᵒᵖ
⊢ Function.Injective ⇑(ConcreteCategory.hom (f.app X✝))

Tactic:
rw [← mono_iff_injective]
      infer_instance

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

Goal state before:
pp: case inr
X : SSet
x y : X.N
h : x < y
h' : x.dim = y.dim
⊢ x.dim < y.dim

Tactic:
obtain ⟨f, _, hf⟩ := le_iff_exists_mono.1 h.le
    obtain ⟨d, ⟨x, hx⟩, rfl⟩ := x.mk_surjective
    obtain ⟨d', ⟨y, hy⟩, rfl⟩ := y.mk_surjective
    obtain rfl : d = d' := h'
    obtain rfl := SimplexCategory.eq_id_of_mono f
    obtain rfl : y = x := by simpa using hf
    simp at h

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

Goal state before:
pp: n d : ℕ
s : Fin (d + 1) ↪o Fin (n + 1)
⊢ objEquiv.symm (Hom.mk s.toOrderHom) ∈ Δ[n].nonDegenerate d

Tactic:
by
    simpa [mem_nonDegenerate_iff_strictMono] using! s.strictMono

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
⊢ IsIso (toOfSimplex x) ↔ Mono (yonedaEquiv.symm x)

Tactic:
constructor
  · intro
    rw [← toOfSimplex_ι]
    infer_instance
  · intro h
    have := mono_of_mono_fac (toOfSimplex_ι x)
    apply isIso_of_mono_of_epi

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case succ
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : Augmented C
ed : X.ExtraDegeneracy
i : ℕ
⊢ (AlternatingFaceMapComplex.ε.app X ≫
          ((AlternatingFaceMapComplex.obj (drop.obj X)).fromSingle₀Equiv (point.obj X)).symm ed.s').f
      (i + 1) =
    (((dNext (i + 1)) fun i ↦ Pi.single (i + 1) (-ed.s i)) + (prevD (i + 1)) fun i ↦ Pi.single (i + 1) (-ed.s i)) +
      (𝟙 (AlternatingFaceMapComplex.obj (drop.obj X))).f (i + 1)

Tactic:
rw [Homotopy.prevD_chainComplex, Homotopy.dNext_succ_chainComplex]
          simp [Fin.sum_univ_succ (n := i + 2), s_comp_δ₀, Preadditive.sum_comp,
            Preadditive.comp_sum,
            s_comp_δ, pow_succ]

Goal state after: