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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
h : IsLeftCancelMulZero R[X]
a b c : R
eq : (fun x ↦ a + x) b = (fun x ↦ a + x) c
a✝ : Nontrivial R
trinomial : R → R[X] := fun r ↦ a • X ^ 2 + r • X + C a
r : R
⊢ (X + C 1) * trinomial r = a • X ^ 3 + (a + r) • X ^ 2 + (a + r) • X + C a

Tactic:
simp only [trinomial, mul_add, add_mul, ← C_mul', C_1, one_mul, ← mul_assoc, X_mul_C, C_add]

Goal state after:
R : Type u_1
inst✝ : Semiring R
h : IsLeftCancelMulZero R[X]
a b c : R
eq : (fun x ↦ a + x) b = (fun x ↦ a + x) c
a✝ : Nontrivial R
trinomial : R → R[X] := fun r ↦ a • X ^ 2 + r • X + C a
r : R
⊢ C a * X * X ^ 2 + C a * X ^ 2 + (C r * X * X + C r * X) + (C a * X + C a) =
    C a * X ^ 3 + (C a * X ^ 2 + C r * X ^ 2) + (C a * X + C r * X) + C a
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: n : ℕ
⊢ (⇑derivative)^[n] (∑ m ∈ range (n + 1), n.choose m • (-1) ^ m * X ^ (n + m)) =
    ∑ x ∈ range (n + 1), ↑((n + x)! / x !) * C (↑(n.choose x) * (-1) ^ x) * X ^ x

Tactic:
rw [iterate_derivative_sum]

Goal state after:
n : ℕ
⊢ ∑ b ∈ range (n + 1), (⇑derivative)^[n] (n.choose b • (-1) ^ b * X ^ (n + b)) =
    ∑ x ∈ range (n + 1), ↑((n + x)! / x !) * C (↑(n.choose x) * (-1) ^ x) * X ^ x
Module: Mathlib.RingTheory.PowerSeries.CoeffMulMem

Goal state before:
pp: A : Type u_1
inst✝ : Semiring A
I : Ideal A
f g : A⟦X⟧
n : ℕ
hg : ∀ i ≤ n, (coeff i) g ∈ I
⊢ ∀ i ≤ n, (coeff i) (f * g) ∈ I

Tactic:
by
  simpa using coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal (I := ⊤) (f := f) n (by simp) hg

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

Goal state before:
pp: R : Type u
N : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : 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 : ι
t : F i ⊗[R] N
⊢ (LinearMap.rTensor N (f ⋯)) t = t

Tactic:
rw [← id_apply (R := R) t]
    apply DFunLike.congr_fun
    ext m n
    simp [D.map_self]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
m : ℕ
⊢ (MvPowerSeries.coeff (Finsupp.single () (p * m))) ((MvPowerSeries.expand p hp) φ) =
    (MvPowerSeries.coeff (Finsupp.single () m)) φ

Tactic:
← smul_eq_mul,

Goal state after:
R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
m : ℕ
⊢ (MvPowerSeries.coeff (Finsupp.single () (p • m))) ((MvPowerSeries.expand p hp) φ) =
    (MvPowerSeries.coeff (Finsupp.single () m)) φ
Module: Mathlib.RingTheory.PowerSeries.Restricted

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
c : ℝ
f : R⟦X⟧
⊢ (fun t ↦ ‖(MvPowerSeries.coeff t) f‖ * t.prod fun x x_1 ↦ c ^ x_1) =
    (fun n ↦ ‖(coeff n) f‖ * c ^ n) ∘ ⇑(Finsupp.uniqueEquiv ())

Tactic:
by
  funext t
  simp only [Function.comp_apply, Finsupp.uniqueEquiv_apply, PUnit.default_eq_unit,
    Finsupp.prod_pow, Finset.univ_unique, Finset.prod_singleton, coeff,
    show (Finsupp.single () (t ())) = t by grind]

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 : ι
t : M ⊗[R] F i
⊢ (LinearMap.lTensor M (f ⋯)) t = t

Tactic:
rw [← id_apply (R := R) t]
    apply DFunLike.congr_fun
    ext m n
    simp [D.map_self]

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

Goal state before:
pp: R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
u : M ⊗[R] N
⊢ ∃ P, P.FG ∧ u ∈ (rTensor N P.subtype).range

Tactic:
by
  let ⟨P, t, ht⟩ := Module.DirectLimit.exists_of ((Submodule.FG.rTensor.directLimit R M N).symm u)
  use P.val, P.property, t
  rw [← Submodule.FG.rTensor.directLimit_apply, ht, LinearEquiv.apply_symm_apply]

Goal state after:
Module: Mathlib.RingTheory.Regular.Free

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : R
mem : x ∈ ⊥.jacobson
reg : IsSMulRegular M x
free : Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
this : Module.Finite (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
I : Type u_2 := Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b : Basis (Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) (R ⧸ Ideal.span {x}) (QuotSMulTop x M) :=
  Free.chooseBasis (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b' : QuotSMulTop x M ≃ₗ[R] I →₀ R ⧸ Ideal.span {x} := LinearEquiv.restrictScalars R b.repr
f : (I →₀ R) →ₗ[R] QuotSMulTop x M := ↑b'.symm ∘ₗ Finsupp.mapRange.linearMap (Submodule.mkQ (Ideal.span {x}))
g : (I →₀ R) →ₗ[R] M
hg : (x • ⊤).mkQ ∘ₗ g = f
surjf : Function.Surjective ⇑f
lejac : Ideal.span {x} ≤ ⊥.jacobson
surjg : Function.Surjective ⇑g
⊢ (Finsupp.submodule fun x_1 ↦ Ideal.span {x} * ⊤) = x • ⊤

Tactic:
← smul_eq_mul,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : R
mem : x ∈ ⊥.jacobson
reg : IsSMulRegular M x
free : Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
this : Module.Finite (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
I : Type u_2 := Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b : Basis (Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) (R ⧸ Ideal.span {x}) (QuotSMulTop x M) :=
  Free.chooseBasis (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b' : QuotSMulTop x M ≃ₗ[R] I →₀ R ⧸ Ideal.span {x} := LinearEquiv.restrictScalars R b.repr
f : (I →₀ R) →ₗ[R] QuotSMulTop x M := ↑b'.symm ∘ₗ Finsupp.mapRange.linearMap (Submodule.mkQ (Ideal.span {x}))
g : (I →₀ R) →ₗ[R] M
hg : (x • ⊤).mkQ ∘ₗ g = f
surjf : Function.Surjective ⇑f
lejac : Ideal.span {x} ≤ ⊥.jacobson
surjg : Function.Surjective ⇑g
⊢ (Finsupp.submodule fun x_1 ↦ Ideal.span {x} • ⊤) = x • ⊤
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case inr
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq :
  ((X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat *
          mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) g) +
        ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g)) *
      q =
    ↑r
k : ℕ
ih : ∀ (i : ℕ), (coeff i) q ∈ I ^ k
i : ℕ
hi : ((map (Ideal.Quotient.mk I)) g).order.toNat ≤ i
⊢ r.coeff i ∈ I ^ (k + 1)

Tactic:
Polynomial.coeff_eq_zero_of_degree_lt (lt_of_lt_of_le hdeg (by simpa)),

Goal state after:
case inr
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq :
  ((X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat *
          mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) g) +
        ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g)) *
      q =
    ↑r
k : ℕ
ih : ∀ (i : ℕ), (coeff i) q ∈ I ^ k
i : ℕ
hi : ((map (Ideal.Quotient.mk I)) g).order.toNat ≤ i
⊢ 0 ∈ I ^ (k + 1)
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q q' : A⟦X⟧
r r' : A[X]
hr : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
hr' : r'.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq : g * q + ↑r = g * q' + ↑r'
⊢ g * (q - q') = ↑(r' - r)

Tactic:
rw [← eq_sub_iff_add_eq] at heq

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q q' : A⟦X⟧
r r' : A[X]
hr : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
hr' : r'.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq : g * q = g * q' + ↑r' - ↑r
⊢ g * (q - q') = ↑(r' - r)
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
a✝ : A
f✝ f'✝ : A⟦X⟧
inst✝ : IsAdicComplete I A
f f' : A⟦X⟧
hf : f ≈ f'
a : A⟦X⟧
ha : a * g = f - f'
⊢ H.mod f = H.mod f'

Tactic:
obtain ⟨hf1, hf2⟩ := H.isWeierstrassDivisionAt_div_mod f

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
a✝ : A
f✝ f'✝ : A⟦X⟧
inst✝ : IsAdicComplete I A
f f' : A⟦X⟧
hf : f ≈ f'
a : A⟦X⟧
ha : a * g = f - f'
hf1 : (H.mod f).degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
hf2 : f = g * H.div f + ↑(H.mod f)
⊢ H.mod f = H.mod f'
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
q : Ideal R[X] := Ideal.map C (maximalIdeal R)
qle : q ≤ p
reg : ↑(Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R
fg' : (maximalIdeal R).FG
fg : (Submodule.generators (maximalIdeal R)).Finite
ht : (maximalIdeal R).height ≤ q.height
eq : ¬p = q
lt : q < p
this : (comap C p).IsMaximal
y : R[X]
left✝ : y.Monic
hy : p = Ideal.map C (comap C p) ⊔ span {y}
peq : p = span (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y})
⊢ ↑(Submodule.spanFinrank
        (span
          (⇑(algebraMap R[X] (Localization.AtPrime p)) ''
            (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y})))) ≤
    ↑(maximalIdeal R).height + ↑1

Tactic:
maximalIdeal_height_eq_ringKrullDim,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
q : Ideal R[X] := Ideal.map C (maximalIdeal R)
qle : q ≤ p
reg : ↑(Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R
fg' : (maximalIdeal R).FG
fg : (Submodule.generators (maximalIdeal R)).Finite
ht : (maximalIdeal R).height ≤ q.height
eq : ¬p = q
lt : q < p
this : (comap C p).IsMaximal
y : R[X]
left✝ : y.Monic
hy : p = Ideal.map C (comap C p) ⊔ span {y}
peq : p = span (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y})
⊢ ↑(Submodule.spanFinrank
        (span
          (⇑(algebraMap R[X] (Localization.AtPrime p)) ''
            (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y})))) ≤
    ringKrullDim R + ↑1
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
rs : List R
reg : RingTheory.Sequence.IsRegular R rs
mem_max : ∀ x ∈ rs, x ∈ maximalIdeal R
⊢ Submodule.map (↑(Shrink.linearEquiv R R).symm) (Ideal.ofList rs * ⊤) = Ideal.ofList rs • ⊤

Tactic:
← smul_eq_mul,

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
rs : List R
reg : RingTheory.Sequence.IsRegular R rs
mem_max : ∀ x ∈ rs, x ∈ maximalIdeal R
⊢ Submodule.map (↑(Shrink.linearEquiv R R).symm) (Ideal.ofList rs • ⊤) = Ideal.ofList rs • ⊤
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : IsSimpleRing R
inst✝ : IsArtinianRing R
n : ℕ
hn : NeZero n
S : Submodule R R
hS : IsSimpleModule R ↥S
e : R ≃ₗ[R] Fin n → ↥S
⊢ ∃ n, ∃ (_ : NeZero n), ∃ I, ∃ (_ : IsSimpleModule R ↥I), Nonempty (R ≃+* Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ)

Tactic:
refine ⟨n, hn, S, hS, ⟨.trans (.opOp R) <| .trans (.op ?_) (.symm .mopMatrix)⟩⟩

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : IsSimpleRing R
inst✝ : IsArtinianRing R
n : ℕ
hn : NeZero n
S : Submodule R R
hS : IsSimpleModule R ↥S
e : R ≃ₗ[R] Fin n → ↥S
⊢ Rᵐᵒᵖ ≃+* Matrix (Fin n) (Fin n) (Module.End R ↥S)
Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ I.ringCon (s.sum f) (∑ _x ∈ ?m.23, 0)

pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ Type ?u.28

pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ Finset ?m.21

Tactic:
exact I.ringCon.finsetSum s hs

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: R Γ : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
inst✝¹ : IsDomain R
inst✝ : LinearOrderedCommGroupWithZero Γ
h : ValuativeRel R
hv : Valuation.Compatible 1
x✝¹ x✝ : R
⊢ 1 x✝¹ ≤ 1 x✝ ↔ if x✝ = 0 then x✝¹ = 0 else True

Tactic:
split_ifs <;>
  simp_all [Valuation.one_apply_of_ne_zero, Valuation.one_apply_le_one]

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
S : Type u_2
inst✝⁹ : CommRing S
R' : Type u_3
S' : Type u_4
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R' S'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
surjRS : Function.Surjective ⇑(algebraMap R S)
eqmap : RingHom.ker (algebraMap S S') = Ideal.map (algebraMap R S) (RingHom.ker (algebraMap R R'))
⊢ Ideal.comap (algebraMap R S) (RingHom.ker (algebraMap S S')) =
    RingHom.ker (algebraMap R R') ⊔ RingHom.ker (algebraMap R S)

Tactic:
simp [eqmap, Ideal.comap_map_of_surjective' _ surjRS]

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

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
⊢ ¬(↑p ^ i).coeff i = 0

Tactic:
WittVector.coeff_p_pow

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
⊢ ¬1 = 0
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ (Finsupp.single (0, x) (p ^ (n + 1 - x))).support ⊆ univ ×ˢ range (n + 1)

pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ ↑p ^ x ≠ 0

Tactic:
· apply Subset.trans Finsupp.support_single_subset
      simpa using mem_range.mp hx

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ ↑p ^ x ≠ 0
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ (Finsupp.single (1, x) (p ^ (n + 1 - x))).support ⊆ univ ×ˢ range (n + 1)

pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ ↑p ^ x ≠ 0

Tactic:
· apply Subset.trans Finsupp.support_single_subset
      simpa using mem_range.mp hx

Goal state after:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ ↑p ^ x ≠ 0
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: case e'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
n : ℕ
⊢ truncateFun (n + 1) (frobenius (mk p (frobeniusRotationCoeff p ha₁ ha₂))) = fun v ↦
    frobeniusRotationCoeff p ha₁ ha₂ ↑v ^ p

Tactic:
apply TruncatedWittVector.ext

Goal state after:
case e'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
n : ℕ
⊢ ∀ (i : Fin (n + 1)),
    TruncatedWittVector.coeff i (truncateFun (n + 1) (frobenius (mk p (frobeniusRotationCoeff p ha₁ ha₂)))) =
      TruncatedWittVector.coeff i fun v ↦ frobeniusRotationCoeff p ha₁ ha₂ ↑v ^ p
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: case mpr
s : Set Ordinal.{u}
⊢ (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s) → IsClosed s

Tactic:
← closure_subset_iff_isClosed

Goal state after:
case mpr
s : Set Ordinal.{u}
⊢ (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s) → closure s ⊆ s
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: α✝¹ : Type u_1
A✝¹ : α✝¹ → PSet.{u_1}
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
αβ : ∀ (a : α✝¹), ∃ b, (A✝¹ a).Equiv (A✝ b)
βα : ∀ (b : α✝), ∃ a, (A✝¹ a).Equiv (A✝ b)
x✝ : Ordinal.{u_1}
⊢ (x✝ ∈ Set.range fun a ↦ succ (A✝¹ a).rank) ↔ x✝ ∈ Set.range fun a ↦ succ (A✝ a).rank

Tactic:
constructor <;> simp only [Set.mem_range, forall_exists_index] <;> intro a h

Goal state after:
case mp
α✝¹ : Type u_1
A✝¹ : α✝¹ → PSet.{u_1}
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
αβ : ∀ (a : α✝¹), ∃ b, (A✝¹ a).Equiv (A✝ b)
βα : ∀ (b : α✝), ∃ a, (A✝¹ a).Equiv (A✝ b)
x✝ : Ordinal.{u_1}
a : α✝¹
h : succ (A✝¹ a).rank = x✝
⊢ ∃ y, succ (A✝ y).rank = x✝

case mpr
α✝¹ : Type u_1
A✝¹ : α✝¹ → PSet.{u_1}
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
αβ : ∀ (a : α✝¹), ∃ b, (A✝¹ a).Equiv (A✝ b)
βα : ∀ (b : α✝), ∃ a, (A✝¹ a).Equiv (A✝ b)
x✝ : Ordinal.{u_1}
a : α✝
h : succ (A✝ a).rank = x✝
⊢ ∃ y, succ (A✝¹ y).rank = x✝
Module: Mathlib.SetTheory.Ordinal.Notation

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

Tactic:
rw [Nat.sub_eq]
      simp only [h, Ordering.compares_eq] at this
      subst e₂
      cases (n₁ : ℕ) - n₂
      · by_cases en : n₁ = n₂ <;> simp only [en, ↓reduceIte]
        · exact h'.mono (le_of_lt h₁.lt)
        · exact NFBelow.zero
      · exact NFBelow.oadd h₁.fst h₁.snd h₁.lt

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

Goal state before:
pp: o : Ordinal.{u}
x : ZFSet.{u}
⊢ x ∈ V_ o ↔ ∃ a < o, x ⊆ V_ a

Tactic:
rw [vonNeumann]

Goal state after:
o : Ordinal.{u}
x : ZFSet.{u}
⊢ x ∈ ⋃ (a : ↑(Set.Iio o)), (V_ ↑a).powerset ↔ ∃ a < o, x ⊆ V_ a
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (V_ o).IsTransitive

Tactic:
rw [vonNeumann]

Goal state after:
o : Ordinal.{u_1}
⊢ (⋃ (a : ↑(Set.Iio o)), (V_ ↑a).powerset).IsTransitive
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: a b : Ordinal.{u}
h : a < b
⊢ V_ a ∈ V_ b

Tactic:
rw [vonNeumann]

Goal state after:
a b : Ordinal.{u}
h : a < b
⊢ V_ a ∈ ⋃ (a : ↑(Set.Iio b)), (V_ ↑a).powerset
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
x : PSet.{u_1}
⊢ x ∈ o.toPSet ↔ ∃ a < o, x.Equiv a.toPSet

Tactic:
toPSet,

Goal state after:
o : Ordinal.{u_1}
x : PSet.{u_1}
⊢ (x ∈ PSet.mk o.ToType fun a ↦ (↑a.toOrd).toPSet) ↔ ∃ a < o, x.Equiv a.toPSet
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.toPSet.rank = o

Tactic:
toPSet,

Goal state after:
o : Ordinal.{u_1}
⊢ (PSet.mk o.ToType fun a ↦ (↑a.toOrd).toPSet).rank = o
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
s : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
⊢ s.destruct =
    Option.map
      (fun x ↦
        match x with
        | (exp, coef, tl) => ((exp, coef), tl))
      (destruct s)

Tactic:
simp only [destruct, Option.map_map]

Goal state after:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
⊢ s.destruct =
    Option.map
      ((fun x ↦ ((x.1, x.2.1), x.2.2)) ∘ fun x ↦
        match x with
        | ((exp, coef), tl) => (exp, coef, tl))
      s.destruct
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: m : UnitMonomial
left right : Basis
⊢ (List.replicate (List.length left) 0 ++ m).toFun (left ++ right) = m.toFun right

Tactic:
induction left with
  | nil => rfl
  | cons left_hd left_tl ih => simp [List.replicate_succ, ih]

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Sort u_1
nil : (f : ℝ → ℝ) → motive (mk Multiseries.nil f)
cons :
  (exp : ℝ) →
    (coef : MultiseriesExpansion basis_tl) →
      (tl : Multiseries basis_hd basis_tl) → (f : ℝ → ℝ) → motive (mk (Multiseries.cons exp coef tl) f)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
⊢ motive ms

Tactic:
let ⟨s, f⟩ := ms
  cases s with
  | nil => apply nil
  | cons hd tl => apply cons

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case seq
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_coef : coef.Sorted
h_comp : tl.leadingExp < ↑exp
h_tl_coef : ∀ x ∈ (mk tl 0).seq, x.2.Sorted
h_tl_tl : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk tl 0).seq
⊢ (Multiseries.cons exp coef tl).Sorted

Tactic:
constructor
  · simp at h_tl_coef ⊢
    grind
  · cases tl
    · exact Seq.Pairwise_cons_nil
    · exact h_tl_tl.cons_cons_of_trans (by simpa [lt_iff_lt] using h_comp)

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

Goal state before:
pp: o : ONote
⊢ o.fastGrowing =
    match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → ℕ → ℕ) o.fundamentalSequence,
      ⋯ with
    | Sum.inl none, x => Nat.succ
    | Sum.inl (some a), x => fun i ↦ a.fastGrowing^[i] i
    | Sum.inr f, x => fun i ↦ (f i).fastGrowing i

Tactic:
rw [fastGrowing]

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

Goal state before:
pp: case lt
a : ONote
ha : a.NF
b : ONote
hb : b.NF
h : a.cmp b = Ordering.lt
this : Ordering.lt.Compares a b
⊢ Ordering.lt.Compares ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
try exact this

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

Goal state before:
pp: case eq
a : ONote
ha : a.NF
b : ONote
hb : b.NF
h : a.cmp b = Ordering.eq
this : Ordering.eq.Compares a b
⊢ Ordering.eq.Compares ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
try exact this

Goal state after:
case eq
a : ONote
ha : a.NF
b : ONote
hb : b.NF
h : a.cmp b = Ordering.eq
this : Ordering.eq.Compares a b
⊢ Ordering.eq.Compares ⟨a, ha⟩ ⟨b, hb⟩
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case gt
a : ONote
ha : a.NF
b : ONote
hb : b.NF
h : a.cmp b = Ordering.gt
this : Ordering.gt.Compares a b
⊢ Ordering.gt.Compares ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
try exact this

Goal state after:
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: q : ℚ
a b : ℕ
h : ∀ (p : ℚ), q ^ a ≠ p ^ b
hb : 0 < b
hq : 0 ≤ q
x : ℚ
hx : ↑x = ↑q ^ (↑a / ↑b)
⊢ ↑q ^ a = ↑x ^ b

Tactic:
hx,

Goal state after:
q : ℚ
a b : ℕ
h : ∀ (p : ℚ), q ^ a ≠ p ^ b
hb : 0 < b
hq : 0 ≤ q
x : ℚ
hx : ↑x = ↑q ^ (↑a / ↑b)
⊢ ↑q ^ a = (↑q ^ (↑a / ↑b)) ^ b
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
⊢ Function.Injective ⇑(ConcreteCategory.hom (eta G)) ↔ Group.ResiduallyFinite ↑G

Tactic:
injective_iff_map_eq_one,

Goal state after:
G : GrpCat
⊢ (∀ (a : ↑G), (ConcreteCategory.hom (eta G)) a = 1 → a = 1) ↔ Group.ResiduallyFinite ↑G