mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case refine_2.inl
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
m : ℕ
h1 : n ≤ m
⊢ (fun m ↦
          if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
          else x ^ p ^ (n - m))
        (m + 1) ^
      p =
    (fun m ↦
        if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
        else x ^ p ^ (n - m))
      m

pp: case refine_2.inr.inl
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
m : ℕ
h1 : n = m + 1
⊢ (fun m ↦
          if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
          else x ^ p ^ (n - m))
        (m + 1) ^
      p =
    (fun m ↦
        if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
        else x ^ p ^ (n - m))
      m

pp: case refine_2.inr.inr
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
m : ℕ
h1 : ¬n ≤ m + 1
⊢ (fun m ↦
          if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
          else x ^ p ^ (n - m))
        (m + 1) ^
      p =
    (fun m ↦
        if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
        else x ^ p ^ (n - m))
      m

Tactic:
· have h1' : n ≤ m + 1 := by lia
      simp only [h1', ↓reduceDIte, h1, Nat.leRec_succ, ← frobenius_def]
      exact Classical.choose_spec (h _)

Goal state after:
case refine_2.inr.inl
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
m : ℕ
h1 : n = m + 1
⊢ (fun m ↦
          if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
          else x ^ p ^ (n - m))
        (m + 1) ^
      p =
    (fun m ↦
        if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
        else x ^ p ^ (n - m))
      m

case refine_2.inr.inr
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
m : ℕ
h1 : ¬n ≤ m + 1
⊢ (fun m ↦
          if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
          else x ^ p ^ (n - m))
        (m + 1) ^
      p =
    (fun m ↦
        if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
        else x ^ p ^ (n - m))
      m
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: R✝ : Type u_1
inst✝⁶ : CommSemiring R✝
p : ℕ
hp : Fact (Nat.Prime p)
inst✝⁵ : CharP R✝ p
R : Type u₁
inst✝⁴ : CommSemiring R
inst✝³ : CharP R p
inst✝² : PerfectRing R p
S : Type u₂
inst✝¹ : CommSemiring S
inst✝ : CharP S p
f : R →+* Perfection S p
r : R
n : ℕ
⊢ (coeff S p n) ((⇑(frobenius (Perfection S p) p))^[n] (f ((⇑(frobeniusEquiv R p).symm)^[n] r))) = (coeff S p n) (f r)

Tactic:
← RingHom.map_iterate_frobenius,

Goal state after:
R✝ : Type u_1
inst✝⁶ : CommSemiring R✝
p : ℕ
hp : Fact (Nat.Prime p)
inst✝⁵ : CharP R✝ p
R : Type u₁
inst✝⁴ : CommSemiring R
inst✝³ : CharP R p
inst✝² : PerfectRing R p
S : Type u₂
inst✝¹ : CommSemiring S
inst✝ : CharP S p
f : R →+* Perfection S p
r : R
n : ℕ
⊢ (coeff S p n) (f ((⇑(frobenius R p))^[n] ((⇑(frobeniusEquiv R p).symm)^[n] r))) = (coeff S p n) (f r)
Module: Mathlib.RingTheory.WittVector.Teichmuller

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ (teichmuller p) 0 = 0

Tactic:
ext ⟨⟩ <;> · rw [zero_coeff]; rfl

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

Goal state before:
pp: case pn
n : ℕ
⊢ (hermite n).degree ≤ ↑n

Tactic:
degree_le_iff_coeff_zero,

Goal state after:
case pn
n : ℕ
⊢ ∀ (m : ℕ), ↑n < ↑m → (hermite n).coeff m = 0
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: case succ
F : Type u_1
inst✝ : Field F
p q : F[X]
d : ℕ
a✝ :
  (match d with
    | 0 => 0
    | d.succ => ∑ i ∈ (p + q).support, (p + q).coeff i • preHilbertPoly F d i) =
    (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i) +
      match d with
      | 0 => 0
      | d.succ => ∑ i ∈ q.support, q.coeff i • preHilbertPoly F d i
⊢ ∑ i ∈ (p + q).support, (p + q).coeff i • preHilbertPoly F d i =
    ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i + ∑ i ∈ q.support, q.coeff i • preHilbertPoly F d i

Tactic:
← sum_def _ fun _ r => r • _

Goal state after:
case succ
F : Type u_1
inst✝ : Field F
p q : F[X]
d : ℕ
a✝ :
  (match d with
    | 0 => 0
    | d.succ => ∑ i ∈ (p + q).support, (p + q).coeff i • preHilbertPoly F d i) =
    (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i) +
      match d with
      | 0 => 0
      | d.succ => ∑ i ∈ q.support, q.coeff i • preHilbertPoly F d i
⊢ ((p + q).sum fun x r ↦ r • preHilbertPoly F d x) =
    ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i + ∑ i ∈ q.support, q.coeff i • preHilbertPoly F d i
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
hx : x = 0
⊢ ∃ i y, i = y + y⁻¹ ∧ ¬y = 0

Tactic:
exact ⟨_, 1, rfl, one_ne_zero⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c x1 x2 : R
ha : a ≠ 0
hvieta : b = -a * (x1 + x2) ∧ c = a * x1 * x2
⊢ (C a * X ^ 2 + C b * X + C c).roots = {x1, x2}

Tactic:
suffices C a * X ^ 2 + C b * X + C c = C a * (X - C x1) * (X - C x2) by
      have h1 : C a * (X - C x1) ≠ 0 := mul_ne_zero (by simpa) (Polynomial.X_sub_C_ne_zero _)
      have h2 : C a * (X - C x1) * (X - C x2) ≠ 0 := mul_ne_zero h1 (Polynomial.X_sub_C_ne_zero _)
      simp [this, Polynomial.roots_mul h2, Polynomial.roots_mul h1]
    simp [hvieta.1, hvieta.2]
    ring

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

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
f : R[X]
inst✝¹ : DecidableEq ↑(f.rootSet S)
hf : (map (algebraMap R S) f).Splits
p : Ideal S
inst✝ : p.IsPrime
hp : (f.rootSet S).ncard ≤ (↑(Multiset.toFinset 0)).ncard + 1
g : G
hg : g ∈ Ideal.inertia G p
hfp : map (algebraMap R (S ⧸ p)) f = 0
⊢ (MulAction.toPermHom G ↑(f.rootSet S)) g = 1 ∨ ((MulAction.toPermHom G ↑(f.rootSet S)) g).IsSwap

Tactic:
Multiset.toFinset_zero,

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
f : R[X]
inst✝¹ : DecidableEq ↑(f.rootSet S)
hf : (map (algebraMap R S) f).Splits
p : Ideal S
inst✝ : p.IsPrime
hp : (f.rootSet S).ncard ≤ (↑∅).ncard + 1
g : G
hg : g ∈ Ideal.inertia G p
hfp : map (algebraMap R (S ⧸ p)) f = 0
⊢ (MulAction.toPermHom G ↑(f.rootSet S)) g = 1 ∨ ((MulAction.toPermHom G ↑(f.rootSet S)) g).IsSwap
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: n : ℕ
⊢ (coeff n) largeSchroderSeries = n.largeSchroder

Tactic:
by
  simp [largeSchroderSeries]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u
M : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Preorder ι
F : ι → Type u_4
inst✝¹ : (i : ι) → AddCommMonoid (F i)
inst✝ : (i : ι) → Module R (F i)
f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j
D : DirectedSystem F fun x x_1 h ↦ ⇑(f h)
i j k : ι
h : k ≤ j
h' : j ≤ i
t : M ⊗[R] F k
⊢ (LinearMap.lTensor M (f h')) ((LinearMap.lTensor M (f h)) t) = (LinearMap.lTensor M (f ⋯)) t

Tactic:
by
    rw [← comp_apply, ← lTensor_comp]
    apply DFunLike.congr_fun
    ext p n
    simp [D.map_map]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: n : ℕ
hn : 0 < n
this :
  ∑ x ∈ range n, (coeff x) (X * largeSchroderSeries) * (n - x).largeSchroder =
    ∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0
x : ℕ
hx : x ∈ Ico 1 n
hx' : 0 < x
⊢ (if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0) = (x - 1).largeSchroder * (n - x).largeSchroder

Tactic:
if_pos hx'

Goal state after:
n : ℕ
hn : 0 < n
this :
  ∑ x ∈ range n, (coeff x) (X * largeSchroderSeries) * (n - x).largeSchroder =
    ∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0
x : ℕ
hx : x ∈ Ico 1 n
hx' : 0 < x
⊢ (x - 1).largeSchroder * (n - x).largeSchroder = (x - 1).largeSchroder * (n - x).largeSchroder
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝¹² : CommSemiring R
M : Type u_1
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
S : Type v
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
f : M →ₚₗ[R] N
A : Type u
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommSemiring T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq : (rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (rTensor M ψ.rangeRestrict.toLinearMap) q
θ : (RingCon.ker ↑φ).Quotient →ₐ[R] (RingCon.ker ↑ψ).Quotient :=
  (↑(quotientKerEquivRangeₐ ψ).symm).comp (h'.comp ↑(quotientKerEquivRangeₐ φ))
ht : (h.comp φ.range.val).comp ↑(quotientKerEquivRangeₐ φ) = ψ.range.val.comp ((↑(quotientKerEquivRangeₐ ψ)).comp θ)
⊢ f.toFun' (RingCon.ker ↑ψ).Quotient
      ((rTensor M (↑(quotientKerEquivRangeₐ ψ).symm).toLinearMap)
        ((rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p)) =
    f.toFun' (RingCon.ker ↑ψ).Quotient ((rTensor M (mkₐ R (RingCon.ker ↑ψ)).toLinearMap) q)

Tactic:
hpq,

Goal state after:
R : Type u
inst✝¹² : CommSemiring R
M : Type u_1
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
S : Type v
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
f : M →ₚₗ[R] N
A : Type u
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommSemiring T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq : (rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (rTensor M ψ.rangeRestrict.toLinearMap) q
θ : (RingCon.ker ↑φ).Quotient →ₐ[R] (RingCon.ker ↑ψ).Quotient :=
  (↑(quotientKerEquivRangeₐ ψ).symm).comp (h'.comp ↑(quotientKerEquivRangeₐ φ))
ht : (h.comp φ.range.val).comp ↑(quotientKerEquivRangeₐ φ) = ψ.range.val.comp ((↑(quotientKerEquivRangeₐ ψ)).comp θ)
⊢ f.toFun' (RingCon.ker ↑ψ).Quotient
      ((rTensor M (↑(quotientKerEquivRangeₐ ψ).symm).toLinearMap) ((rTensor M ψ.rangeRestrict.toLinearMap) q)) =
    f.toFun' (RingCon.ker ↑ψ).Quotient ((rTensor M (mkₐ R (RingCon.ker ↑ψ)).toLinearMap) q)
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
i : ℕ
hi : i < ((map (Ideal.Quotient.mk I)) g).order.toNat
H : f - ↑r = g * q
⊢ (coeff i) (f - ↑r) ∈ I

Tactic:
H

Goal state after:
A : Type u_1
inst✝ : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
i : ℕ
hi : i < ((map (Ideal.Quotient.mk I)) g).order.toNat
H : f - ↑r = g * q
⊢ (coeff i) (g * q) ∈ I
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_5
inst✝³ : AddCommMonoid P
inst✝² : Module R P
f : M →ₚₗ[R] N
g : N →ₚₗ[R] P
S : Type u_7
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S ⟨s, p⟩ = t
hb : π R N S ⟨s, f.toFun' (MvPolynomial (Fin s.card) R) p⟩ = toFun S f t
⊢ toFun S (g.comp f) t = toFun S g (toFun S f t)

Tactic:
toFun_eq_rTensor_φ_toFun' _ hb,

Goal state after:
R : Type u
inst✝⁸ : CommSemiring R
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_5
inst✝³ : AddCommMonoid P
inst✝² : Module R P
f : M →ₚₗ[R] N
g : N →ₚₗ[R] P
S : Type u_7
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S ⟨s, p⟩ = t
hb : π R N S ⟨s, f.toFun' (MvPolynomial (Fin s.card) R) p⟩ = toFun S f t
⊢ toFun S (g.comp f) t =
    (rTensor P (φ R s).toLinearMap) (g.toFun' (MvPolynomial (Fin s.card) R) (f.toFun' (MvPolynomial (Fin s.card) R) p))
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsSimpleModule R ↥N
s : Set (Submodule R M)
hs : ∀ (m : ↑s), IsSemisimpleModule R ↥↑m
hN : N ≤ ⨆ a ∈ s, a
e : ↥N ≃ₗ[R] ↥(inclusion hN).range
this✝ : IsSimpleModule R ↥(inclusion hN).range
this : IsSemisimpleModule R ↥(⨆ i ∈ s, i)
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty (↥N ≃ₗ[R] ↥S)

Tactic:
obtain ⟨_, ⟨m, hm, rfl⟩, S, le, ⟨e'⟩⟩ := LinearMap.range (inclusion hN)
      |>.le_linearEquiv_of_sSup_eq_top (comap (⨆ i ∈ s, i).subtype '' s) <| by
    rw [sSup_image, biSup_comap_subtype_eq_top]

Goal state after:
R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsSimpleModule R ↥N
s : Set (Submodule R M)
hs : ∀ (m : ↑s), IsSemisimpleModule R ↥↑m
hN : N ≤ ⨆ a ∈ s, a
e : ↥N ≃ₗ[R] ↥(inclusion hN).range
this✝ : IsSimpleModule R ↥(inclusion hN).range
this : IsSemisimpleModule R ↥(⨆ i ∈ s, i)
m : Submodule R M
hm : m ∈ s
S : Submodule R ↥(⨆ a ∈ s, a)
le : S ≤ comap (⨆ i ∈ s, i).subtype m
e' : ↥(inclusion hN).range ≃ₗ[R] ↥S
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty (↥N ≃ₗ[R] ↥S)
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: case inr
R : Type u_2
M : Type u
N : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
S : Submodule R M
inst✝ : IsSimpleModule R ↥S
f : M →ₗ[R] N
eq : f ∘ₗ S.subtype = 0
⊢ (f ∘ₗ S.subtype).range ≤ isotypicComponent R N ↥S

Tactic:
· simp_rw [eq, LinearMap.range_zero, bot_le]

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
S : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup S
inst✝³ : Module R M
inst✝² : Module R S
inst✝¹ : IsSimpleModule R S
inst✝ : IsSemisimpleModule R M
m : Submodule R M
ne : m ≠ ⊥
⊢ m = isotypicComponent R M S → IsIsotypicOfType R (↥m) S ∧ m.IsFullyInvariant

Tactic:
by rintro rfl; exact ⟨.isotypicComponent R M S, .isotypicComponent R M S⟩

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Maximal.Topology

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x : MaximalSpectrum R
⊢ toPrimeSpectrum ⁻¹' {x.toPrimeSpectrum} = {x}

Tactic:
by
      simpa only [← image_singleton] using preimage_image_eq {x} toPrimeSpectrum_injective

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Moebius

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h✝ : Nontrivial α
ha : Squarefree a
hb : Squarefree b
⊢ moebius (a * b) = moebius a * moebius b

Tactic:
have hab : Squarefree (a * b) := squarefree_mul_iff.mpr ⟨h, ha, hb⟩

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h✝ : Nontrivial α
ha : Squarefree a
hb : Squarefree b
hab : Squarefree (a * b)
⊢ moebius (a * b) = moebius a * moebius b
Module: Mathlib.RingTheory.WittVector.Isocrystal

Goal state before:
pp: p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : Φ(p, k) x ≠ 0
⊢ ∃ a, a ≠ 0 ∧ Φ(p, k) x = a • x

Tactic:
rw [finrank_eq_one_iff_of_nonzero' x hx] at h_dim

Goal state after:
p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
this✝ : Nontrivial V
x : V
h_dim : ∀ (w : V), ∃ c, c • x = w
hx : x ≠ 0
this : Φ(p, k) x ≠ 0
⊢ ∃ a, a ≠ 0 ∧ Φ(p, k) x = a • x
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y : 𝕎 k
this : ↑p = 0
sum_zero_pow_mul_pow_p :
  ∀ (y : 𝕎 k), ∑ x ∈ range (n + 1 + 1), 0 ^ x * y.coeff x ^ p ^ (n + 1 - x) = y.coeff 0 ^ p ^ (n + 1)
⊢ (x * y).coeff (n + 1) - y.coeff (n + 1) * ∑ x_1 ∈ range (n + 1 + 1), 0 ^ x_1 * x.coeff x_1 ^ p ^ (n + 1 - x_1) -
      x.coeff (n + 1) * ∑ x ∈ range (n + 1 + 1), 0 ^ x * y.coeff x ^ p ^ (n + 1 - x) =
    (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)

Tactic:
congr <;> apply sum_zero_pow_mul_pow_p

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : ℵ₀ < cof α
a : α
f : ↑s → α → α
hf : ∀ (x : ↑s) (x_1 : α), f x x_1 ∈ ↑x ∧ x_1 ≤ f x x_1
g : ℕ → α := ⋯
hg : BddAbove (range g)
t : Set α
ht : t ∈ s
⊢ (range fun n ↦ f ⟨t, ht⟩ (g n)) ⊆ t

Tactic:
· grind

Goal state after:
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
⊢ ∃ f,
    ∀ (x y : 𝕎 k),
      (x * y).coeff (n + 1) =
        x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) + y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) +
          f (truncateFun (n + 1) x) (truncateFun (n + 1) y)

Tactic:
by
  obtain ⟨f, hf⟩ := nth_mul_coeff' p k n
  use f
  intro x y
  rw [hf x y]
  ring

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case refine_2.inl
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : b ≤ 1
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b o))

Tactic:
rw [CNF.of_le_one hb ho]

Goal state after:
case refine_2.inl
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : b ≤ 1
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst [(0, o)])
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case inr.inl
b : Ordinal.{u_1}
hb : b ≤ 1
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ (0, (single 0 o) 0) ∈ CNF b o

Tactic:
rw [CNF.of_le_one hb ho]

Goal state after:
case inr.inl
b : Ordinal.{u_1}
hb : b ≤ 1
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ (0, (single 0 o) 0) ∈ [(0, o)]
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case inr.inr
b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
ho : o ≠ 0
ha : a ≠ 0
⊢ a ∉ map Prod.fst (CNF b o)

Tactic:
rw [CNF.of_le_one hb ho]

Goal state after:
case inr.inr
b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
ho : o ≠ 0
ha : a ≠ 0
⊢ a ∉ map Prod.fst [(0, o)]
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case inl
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
⊢ (e, x) ∈ (e, x) :: CNF b y

Tactic:
exact mem_cons_self

Goal state after:
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: case refine_1
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
h : IsOpen[inst✝³] {a}
ha : IsSuccLimit a
⊢ False

Tactic:
obtain ⟨l, u, h₁, h₂⟩ := mem_nhds_iff_exists_Ioo_subset' (by simpa using ha.not_isMin)
      (by simpa only [not_isMax_iff] using not_isMax a) |>.mp (h.mem_nhds (mem_singleton a))
    refine ha.isSuccPrelimit l ?_
    rw [← succ_eq_iff_covBy]
    simp only [mem_Ioo, subset_singleton_iff] at h₁ h₂
    exact h₂ _ ⟨lt_succ l, h₁.1.succ_le.trans_lt h₁.2⟩

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o : ONote
b₁ b₂ : Ordinal.{0}
bb : b₁ ≤ b₂
h : o.NFBelow b₁
⊢ o.NFBelow b₂

Tactic:
by
  induction h with
  | zero => exact zero
  | oadd' h₁ h₂ h₃ _ _ => constructor; exacts [h₁, h₂, lt_of_lt_of_le h₃ bb]

Goal state after:
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: n : ℕ
f : (Fin n → ZFSet.{u}) → ZFSet.{u}
inst✝ : Definable n f
xs ys : Fin n → PSet.{u}
h : ∀ (i : Fin n), xs i ≈ ys i
⊢ (f fun x ↦ ZFSet.mk (xs x)) = f fun x ↦ ZFSet.mk (ys x)

Tactic:
exact congrArg _ (funext fun i ↦ Quotient.sound (h i))

Goal state after:
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y z : ZFSet.{u_1}
⊢ {y, z} = {x} ↔ x = y ∧ x = z

Tactic:
pair_eq_singleton_iff

Goal state after:
x y z : ZFSet.{u_1}
⊢ y = x ∧ z = x ↔ x = y ∧ x = z
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x x' y y' : ZFSet.{u_1}
⊢ x.pair y = x'.pair y' → x = x' ∧ y = y'

Tactic:
H

Goal state after:
x x' y y' : ZFSet.{u_1}
H : x.pair y = x'.pair y'
⊢ x = x' ∧ y = y'
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.eq
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this✝¹ : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this✝ : e.NF
this : e'.NF
he : e.cmp e' = Ordering.eq
ee : e = e'
⊢ ω ^ e.repr * (↑↑n + ↑↑n') + a'.repr = ω ^ e.repr * ↑↑n + (ω ^ e'.repr * ↑↑n' + a'.repr)

Tactic:
rw [ee, ← add_assoc, ← mul_add]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case inr.inr
o x : Ordinal.{u}
h : x.invVeblen₁ < o
⊢ ω ^ x ∈ range (veblen o) ↔ o ≤ x.invVeblen₁

Tactic:
· apply iff_of_false _ h.not_ge
    rintro ⟨z, hz⟩
    have hz' := hz
    rw [← veblen_veblen_of_lt h, hz', veblen_opow_eq_opow_iff] at hz
    exact (lt_veblen_invVeblen₁ x).ne' hz

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case pos
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h' : (a₁.sub a₂).NFBelow e₁.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
en : n₁ = n₂
⊢ (match Ordering.eq with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match 0 with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).NFBelow
    b

Tactic:
simp only [en, ↓reduceIte]

Goal state after:
case pos
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h' : (a₁.sub a₂).NFBelow e₁.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
en : n₁ = n₂
⊢ (a₁.sub a₂).NFBelow b
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h' : (a₁.sub a₂).NFBelow e₁.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
en : ¬n₁ = n₂
⊢ (match Ordering.eq with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match 0 with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).NFBelow
    b

Tactic:
simp only [en, ↓reduceIte]

Goal state after:
case neg
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h' : (a₁.sub a₂).NFBelow e₁.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
en : ¬n₁ = n₂
⊢ NFBelow 0 b