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

Goal state before:
pp: case neg.refine_2
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
hn : 1 < n
h : Irreducible (map (Int.castRingHom ℚ) (X ^ n - X - 1))
⊢ Irreducible (X ^ n - X - 1)

Tactic:
Polynomial.map_sub,

Goal state after:
case neg.refine_2
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
hn : 1 < n
h : Irreducible (map (Int.castRingHom ℚ) (X ^ n - X) - map (Int.castRingHom ℚ) 1)
⊢ Irreducible (X ^ n - X - 1)
Module: Mathlib.RingTheory.Polynomial.Selmer

Goal state before:
pp: case neg.refine_2
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
hn : 1 < n
h : Irreducible (map (Int.castRingHom ℚ) (X ^ n - X) - map (Int.castRingHom ℚ) 1)
⊢ Irreducible (X ^ n - X - 1)

Tactic:
Polynomial.map_sub,

Goal state after:
case neg.refine_2
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
hn : 1 < n
h : Irreducible (map (Int.castRingHom ℚ) (X ^ n) - map (Int.castRingHom ℚ) X - map (Int.castRingHom ℚ) 1)
⊢ Irreducible (X ^ n - X - 1)
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 ≤ (f.rootSet (S ⧸ p)).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:
rw [rootSet_def f (S ⧸ p), aroots_def, hfp, roots_zero, Multiset.toFinset_zero,
      Finset.coe_empty, Set.ncard_empty, zero_add, Set.ncard_le_one_iff_subsingleton,
      ← Set.subsingleton_coe] at hp

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 : Subsingleton ↑(f.rootSet S)
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: ⊢ largeSchroderSeries = 1 + X * largeSchroderSeries + X * largeSchroderSeries ^ 2

Tactic:
ext n
  by_cases hn : n = 0
  · aesop
  · have hn' : 0 < n := by omega
    simp only [coeff_largeSchroderSeries, map_add, coeff_one, hn, ↓reduceIte, zero_add]
    rw [coeff_X_mul_largeSchroderSeriesSeries_sq _ hn', coeff_X_mul_largeSchroderSeries _ hn',
      show n = n - 1 + 1 by omega, largeSchroder_succ (n - 1)]
    simp only [add_tsub_cancel_right, Nat.add_left_cancel_iff]
    rw [Iic_eq_Icc, Nat.bot_eq_zero, ← range_succ_eq_Icc_zero]

Goal state after:
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
f : A⟦X⟧
k i : ℕ
q : A⟦X⟧ := ⋯
s : A⟦X⟧ := ⋯
n : ℕ := ⋯
hi : i ≥ n
hq : ∀ {i : ℕ}, i ≥ n → (coeff i) s ∈ I ^ k
s₀ : A[X] := ⋯
s₁ : A⟦X⟧ := ⋯
hs : s = X ^ n * s₁ + ↑s₀
q' : A⟦X⟧ := ⋯
⊢ f - g * q' = s + g * (q - q')

pp: A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
q : A⟦X⟧ := ⋯
s : A⟦X⟧ := ⋯
n : ℕ := ⋯
hi : i ≥ n
hq : ∀ {i : ℕ}, i ≥ n → (coeff i) s ∈ I ^ k
s₀ : A[X] := ⋯
s₁ : A⟦X⟧ := ⋯
hs : s = X ^ n * s₁ + ↑s₀
q' : A⟦X⟧ := ⋯
⊢ s + g * (q - q') = ↑s₀ - ↑((trunc n) g) * s₁ * ↑⋯.unit⁻¹

Tactic:
· simp_rw [s]; ring

Goal state after:
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
q : A⟦X⟧ := ⋯
s : A⟦X⟧ := ⋯
n : ℕ := ⋯
hi : i ≥ n
hq : ∀ {i : ℕ}, i ≥ n → (coeff i) s ∈ I ^ k
s₀ : A[X] := ⋯
s₁ : A⟦X⟧ := ⋯
hs : s = X ^ n * s₁ + ↑s₀
q' : A⟦X⟧ := ⋯
⊢ s + g * (q - q') = ↑s₀ - ↑((trunc n) g) * s₁ * ↑⋯.unit⁻¹
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
f : A⟦X⟧
k i✝ i : ℕ
⊢ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) (f - g * H.seq f k) ∈ I ^ k

Tactic:
exact H.coeff_seq_mem f k (by simp)

Goal state after:
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
f : A⟦X⟧
inst✝ : IsPrecomplete I A
i : ℕ
⊢ (coeff i) (H.div f) = ↑(H.divCoeff f i)

Tactic:
by
  simp [div]

Goal state after:
Module: Mathlib.RingTheory.RegularLocalRing.Defs

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
R' : Type u_2
inst✝ : CommRing R'
e : R ≃+* R'
this✝ : IsLocalRing R'
this : IsNoetherianRing R'
⊢ IsRegularLocalRing R'

Tactic:
isRegularLocalRing_iff,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
R' : Type u_2
inst✝ : CommRing R'
e : R ≃+* R'
this✝ : IsLocalRing R'
this : IsNoetherianRing R'
⊢ ↑(Submodule.spanFinrank (maximalIdeal R')) = ringKrullDim R'
Module: Mathlib.RingTheory.RegularLocalRing.Defs

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ IsRegularLocalRing R ↔ ↑(Module.finrank (ResidueField R) (CotangentSpace R)) = ringKrullDim R

Tactic:
isRegularLocalRing_iff,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ ↑(Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R ↔
    ↑(Module.finrank (ResidueField R) (CotangentSpace R)) = ringKrullDim R
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: case hpq
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
T : Type w
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S ⟨s, p⟩ = t
s' : Finset T := ⋯
h' : ↥(φ R s).range →ₐ[R] ↥(φ R s').range := ⋯
j : Fin s.card → Fin s'.card := ⋯
eq_h_comp : (φ R s').comp (rename j) = h.comp (φ R s)
p' : MvPolynomial (Fin s'.card) R ⊗[R] M := ⋯
ha' : π R M T ⟨s', p'⟩ = (rTensor M h.toLinearMap) t
⊢ (rTensor M (h'.comp (φ R s).rangeRestrict).toLinearMap) p = (rTensor M (φ R s').rangeRestrict.toLinearMap) p'

Tactic:
· simp only [p', ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap]
    congr
    ext n
    simp only [AlgHom.coe_comp, Function.comp_apply, coe_codRestrict,
      Subalgebra.coe_val, rename_X, h', j]
    simp only [φ, aeval_X, Equiv.symm_apply_apply]

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

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
f g : A⟦X⟧
hg : (map (IsLocalRing.residue A)) g ≠ 0
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
⊢ f.IsWeierstrassDivision g (f /ʷ g) (f %ʷ g)

Tactic:
by
  simp_rw [weierstrassDiv, weierstrassMod, dif_pos hg]
  exact (IsWeierstrassDivisor.of_map_ne_zero hg).isWeierstrassDivisionAt_div_mod f

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

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
hI : I ≠ ⊤
⊢ constantCoeff h ∉ I

Tactic:
contrapose hI

Goal state after:
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
hI : constantCoeff h ∈ I
⊢ I = ⊤
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
⊢ IsRegularLocalRing (Localization.AtPrime p)

Tactic:
apply IsRegularLocalRing.of_spanFinrank_maximalIdeal_le
  let q := (maximalIdeal R).map C
  have qle : q ≤ p := by simpa [q, ← max] using map_comap_le
  have reg := (isRegularLocalRing_iff R).mp ‹_›
  have fg' := (maximalIdeal R).fg_of_isNoetherianRing
  have fg := Submodule.FG.finite_generators fg'
  have ht : (maximalIdeal R).height ≤ q.height := le_of_eq (height_map_C (maximalIdeal R)).symm
  by_cases eq : p = q
  · have ht1 : (maximalIdeal R).height ≤ p.height := by simpa [eq]
    have : Ideal.span ((algebraMap R (Localization.AtPrime p)) '' (maximalIdeal R).generators) =
      maximalIdeal (Localization.AtPrime p) := by
      rw [IsScalarTower.algebraMap_eq R R[X] (Localization.AtPrime p), RingHom.coe_comp,
        Set.image_comp, ← Ideal.map_span, ← Ideal.map_span]
      simp only [Ideal.span, (maximalIdeal R).span_generators, algebraMap_eq, q, ← eq,
        Localization.AtPrime.map_eq_maximalIdeal]
    simp only [← maximalIdeal_height_eq_ringKrullDim, ← IsLocalization.height_under p.primeCompl,
      IsLocalization.AtPrime.under_maximalIdeal _ p, ge_iff_le]
    apply le_trans _ (WithBot.coe_le_coe.mpr ht1)
    simp only [maximalIdeal_height_eq_ringKrullDim, ← reg, Nat.cast_le, ← this,
      ← Submodule.FG.generators_ncard fg']
    exact (Submodule.spanFinrank_span_le_ncard_of_finite (fg.image _)).trans (Set.ncard_image_le fg)
  · have lt : q < p := lt_of_le_of_ne qle (Ne.symm eq)
    have : (comap C p).IsMaximal := by simpa [max] using maximalIdeal.isMaximal R
    obtain ⟨y, _, hy⟩ := Polynomial.exists_monic_span_sup_map_eq R p this (by simpa [max])
    have peq : p = Ideal.span (((algebraMap R R[X]) '' (maximalIdeal R).generators) ∪ {y}) := by
      simp only [Set.union_comm, Ideal.span_union, ← Ideal.map_span, algebraMap_eq, sup_comm]
      nth_rw 1 [hy, max, ← (maximalIdeal R).span_generators]
    simp only [← Localization.AtPrime.map_eq_maximalIdeal, peq, Ideal.map_span]
    rw [← maximalIdeal_height_eq_ringKrullDim, ← IsLocalization.height_under p.primeCompl,
      IsLocalization.AtPrime.under_maximalIdeal _ p]
    apply le_trans _ (WithBot.coe_le_coe.mpr (Ideal.height_add_one_le_of_lt_of_isPrime lt))
    apply le_trans _ (WithBot.coe_le_coe.mpr (add_le_add_left ht 1))
    rw [WithBot.coe_add, maximalIdeal_height_eq_ringKrullDim, WithBot.coe_one, ← reg,
      ← Nat.cast_one, ← Nat.cast_add, Nat.cast_le]
    have fin := (fg.image (algebraMap R R[X])).union (Set.finite_singleton y)
    apply le_trans (Submodule.spanFinrank_span_le_ncard_of_finite (fin.image _))
    apply le_trans (Set.ncard_image_le fin) (le_trans (Set.ncard_union_le _ _) _)
    rw [Set.ncard_singleton, add_le_add_iff_right, ← Submodule.FG.generators_ncard fg']
    exact Set.ncard_image_le fg

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, x ^ n ∈ f.range
hker : RingHom.ker f ≤ nilradical R
q q' : PrimeSpectrum S
hqq' : comap f q = comap f q'
x : S
n : ℕ
hn : n > 0
y : R
hy : f y = x ^ n
⊢ x ^ n ∈ q.asIdeal ↔ x ^ n ∈ q'.asIdeal

Tactic:
← hy

Goal state after:
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, x ^ n ∈ f.range
hker : RingHom.ker f ≤ nilradical R
q q' : PrimeSpectrum S
hqq' : comap f q = comap f q'
x : S
n : ℕ
hn : n > 0
y : R
hy : f y = x ^ n
⊢ f y ∈ q.asIdeal ↔ f y ∈ q'.asIdeal
Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing

Goal state before:
pp: p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a b : 𝕎 k
hab : ↑p = 0
h : a * b = 0
⊢ False

Tactic:
exact p_nonzero p k hab

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

Goal state before:
pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (⇑verschiebung ∘ ⇑frobenius)^[m] b
this : (⇑verschiebung ∘ ⇑frobenius)^[m] b = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)
⊢ a = ↑p ^ m * b

Tactic:
← mul_left_iterate (p : 𝕎 k) m

Goal state after:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (⇑verschiebung ∘ ⇑frobenius)^[m] b
this : (⇑verschiebung ∘ ⇑frobenius)^[m] b = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)
⊢ a = (fun x ↦ ↑p * x)^[m] b
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : solution p a₁ a₂ = 0
this : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
⊢ False

Tactic:
rw [h, zero_pow] at this

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : solution p a₁ a₂ = 0
this : 0 = a₂.coeff 0 / a₁.coeff 0
⊢ False

p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : solution p a₁ a₂ = 0
this : 0 ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
⊢ p - 1 ≠ 0
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hq' : q'.coeff 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
b : 𝕎 k := frobeniusRotation p hr' hq'
key : frobenius b * r' = q' * b
hq'' : (algebraMap (𝕎 k) (FractionRing (𝕎 k))) q' ≠ 0
⊢ φ ((algebraMap (𝕎 k) (FractionRing (𝕎 k))) b) * Localization.mk (↑p ^ m * r') ⟨↑p ^ n * q', hq⟩ =
    ↑p ^ ↑m / ↑p ^ ↑n * (algebraMap (𝕎 k) (FractionRing (𝕎 k))) b

Tactic:
simp [field, FractionRing.p_nonzero p k]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hq' : q'.coeff 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
b : 𝕎 k := frobeniusRotation p hr' hq'
key : frobenius b * r' = q' * b
hq'' : (algebraMap (𝕎 k) (FractionRing (𝕎 k))) q' ≠ 0
⊢ (algebraMap (𝕎 k) (Localization (nonZeroDivisors (𝕎 k)))) (frobenius b) * (algebraMap (𝕎 k) (FractionRing (𝕎 k))) r' =
    (algebraMap (𝕎 k) (FractionRing (𝕎 k))) q' * (algebraMap (𝕎 k) (FractionRing (𝕎 k))) b
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (polyOfInterest p n).vars =
    (↑p ^ (n + 1) *
        (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1) -
            X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) -
          X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)))).vars

Tactic:
by
  have : (p : 𝕄) ^ (n + 1) = C ((p : ℤ) ^ (n + 1)) := by norm_cast
  rw [polyOfInterest, this, vars_C_mul]
  apply pow_ne_zero
  exact mod_cast hp.out.ne_zero

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

Goal state before:
pp: case inr.inr.refine_2
α : 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 : ℕ → α := fun t ↦ Nat.rec a (fun x IH ↦ sSup (range fun x ↦ f x IH)) t
hg : BddAbove (range g)
t : Set α
ht : t ∈ s
b : α
hb : b ∈ upperBounds (range fun n ↦ f ⟨t, ht⟩ (g n))
n : ℕ
⊢ g n ≤ b

Tactic:
· exact (hf ⟨t, ht⟩ _).2.trans <| hb ⟨_, rfl⟩

Goal state after:
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
h : [] ∉ T
⊢ T = ⊥

Tactic:
by ext x; simpa using fun h' ↦ h <| mem_of_prefix x.nil_prefix h'

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case cons.inl
α : Type u_1
a : Lists α
l0 l₂ : Lists' α true
a'✝ : Lists α
m : a'✝ ∈ l₂.toList
s : l0.Subset l₂
e : a ~ a'✝
⊢ a ∈ l₂

pp: case cons.inr
α : Type u_1
a : Lists α
l0 l₂ : Lists' α true
a✝ a'✝ : Lists α
e : a✝ ~ a'✝
m : a'✝ ∈ l₂.toList
s : l0.Subset l₂
h : a ∈ l0.toList
⊢ a ∈ l₂

Tactic:
· exact ⟨_, m, e⟩

Goal state after:
case cons.inr
α : Type u_1
a : Lists α
l0 l₂ : Lists' α true
a✝ a'✝ : Lists α
e : a✝ ~ a'✝
m : a'✝ ∈ l₂.toList
s : l0.Subset l₂
h : a ∈ l0.toList
⊢ a ∈ l₂
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ ∀ a ∈ { entries := map Prod.toSigma (CNF b o), nodupKeys := ⋯ }.entries, decide (a.snd ≠ 0) = true

Tactic:
· simp_rw [mem_map]
    rintro _ ⟨a, ⟨ha, rfl⟩⟩
    simpa using (snd_pos ha).ne'

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
s : Set α
h : ¬IsMin a ∧ ∀ b < a, (s ∩ Ioo b a).Nonempty
⊢ ¬IsMin a ∧ ∀ (b : α), ¬b ⋖ a

Tactic:
Set.Nonempty

Goal state after:
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
s : Set α
h : ¬IsMin a ∧ ∀ b < a, ∃ x, x ∈ s ∩ Ioo b a
⊢ ¬IsMin a ∧ ∀ (b : α), ¬b ⋖ a
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: ⊢ DecidableRel TopBelow

Tactic:
by
  intro b o
  cases o <;> delta TopBelow <;> infer_instance

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
⊢ veblenWith f (o + 1) = deriv (veblenWith f o)

Tactic:
rw [deriv_eq_enumOrd (isNormal_veblenWith hf o),
    veblenWith_of_ne_zero f (add_pos_of_right zero_lt_one _).ne', derivFamily_eq_enumOrd]
  · apply congr_arg
    ext a
    rw [mem_iInter]
    use fun ha ↦ ha ⟨o, lt_succ o⟩
    rintro (ha : _ = _) ⟨b, hb : b < _⟩
    obtain rfl | hb := lt_succ_iff_eq_or_lt.1 hb
    · rw [Function.mem_fixedPoints_iff, ha]
    · rw [← ha]
      exact veblenWith_veblenWith_of_lt hf hb _
  · exact fun o ↦ isNormal_veblenWith hf o.1

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ω ^ deriv (fun a ↦ ω ^ a) o = deriv (fun a ↦ ω ^ a) o

Tactic:
deriv_fp (isNormal_opow one_lt_omega0)

Goal state after:
o : Ordinal.{u_1}
⊢ deriv (fun x ↦ ω ^ x) o = deriv (fun a ↦ ω ^ a) o
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o : Ordinal.{u}
⊢ o < ε_ 0 ↔ ∃ n, o < (fun a ↦ ω ^ a)^[n] 0

Tactic:
by
  rw [epsilon_zero_eq_nfp, lt_nfp_iff]

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ↑o.toZFSet = toZFSet '' Iio o

Tactic:
by
  ext
  simp [mem_toZFSet_iff]

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

Goal state before:
pp: f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
⊢ Tendsto (fun x ↦ (f ^ exp) x / (f ^ exp') x) atTop (𝓝 0)

pp: f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
⊢ ∀ᶠ (x : ℝ) in atTop, (f ^ exp') x = 0 → (f ^ exp) x = 0

Tactic:
· have : (fun t ↦ f t ^ exp / f t ^ exp') =ᶠ[atTop] fun t ↦ (f t) ^ (exp - exp') :=
      (h.eventually_gt_atTop 0).mono (fun _ h ↦ by simp [← Real.rpow_sub h])
    apply Tendsto.congr' this.symm
    conv =>
      arg 1
      rw [show (fun t ↦ f t ^ (exp - exp')) = ((fun t ↦ t ^ (-(exp' - exp))) ∘ f) by ext; simp]
    exact (tendsto_rpow_neg_atTop (by linarith)).comp h

Goal state after:
f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
⊢ ∀ᶠ (x : ℝ) in atTop, (f ^ exp') x = 0 → (f ^ exp) x = 0
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case succ.refine_2.e_a.succ
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
n✝ : ℕ
h : a'.repr + ↑(n✝ + 1) < ω ^ a0.repr
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑(n✝ + 1)) (k + 1) (n✝ + 1)).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑(n✝ + 1)) k (n✝ + 1)).repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑(n✝ + 1)) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑(n✝ + 1)) + R
Rl : R < ω ^ (a0.repr * succ ↑k)
⊢ ω0 ^ ↑k * α' * ↑(n✝ + 1) + R = (ω0 ^ ↑k * α' + R) * ↑(n✝ + 1)

Tactic:
rw [Nat.cast_add_one, ← succ_eq_add_one, add_mul_succ]

Goal state after:
case succ.refine_2.e_a.succ.ba
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
n✝ : ℕ
h : a'.repr + ↑(n✝ + 1) < ω ^ a0.repr
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑(n✝ + 1)) (k + 1) (n✝ + 1)).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑(n✝ + 1)) k (n✝ + 1)).repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑(n✝ + 1)) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑(n✝ + 1)) + R
Rl : R < ω ^ (a0.repr * succ ↑k)
⊢ R + ω0 ^ ↑k * α' = ω0 ^ ↑k * α'
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: basis : Basis
f : ℝ → ℝ
ex_tl : BasisExtension basis
h_basis : WellFormedBasis (insert f ex_tl).getBasis
⊢ List.Sublist ex_tl.getBasis (insert f ex_tl).getBasis

Tactic:
by simp [getBasis]

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

Goal state before:
pp: basis : Basis
n : ℕ
h : n < List.length basis
⊢ (monomial basis n).toFun = basis[n]

Tactic:
by
  let n' : Fin basis.length := ⟨n, h⟩
  conv_lhs => rw [show n = n'.val by simp [n']]
  convert! monomialRpow_toFun
  simp
  grind

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.cons
exps_hd : ℝ
exps_tl : List ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_allZero : exps_hd = 0 ∧ AllZero exps_tl
⊢ Tendsto (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop (𝓝 1)

Tactic:
have h_eq : UnitMonomial.toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) =
                  UnitMonomial.toFun exps_tl basis_tl := by
        ext x; simp [UnitMonomial.toFun, h_allZero.left]

Goal state after:
case cons.cons
exps_hd : ℝ
exps_tl : List ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_allZero : exps_hd = 0 ∧ AllZero exps_tl
h_eq : toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) = toFun exps_tl basis_tl
⊢ Tendsto (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop (𝓝 1)
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
pp: a : ℤ
n : ℕ
h : IsInt a (Int.negOfNat n)
⊢ n = 0 ↔ IsSquare a

Tactic:
refine ⟨fun h' ↦ by simp [h.1, h'], fun ⟨b, hb⟩ ↦ ?_⟩
  rw [h.1, Int.cast_negOfNat] at hb
  rcases eq_or_ne b 0 with rfl | hb₀
  · simp_all
  · refine absurd hb (ne_of_lt ?_)
    exact lt_of_le_of_lt (by simp) (mul_self_pos.mpr hb₀)

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

Goal state before:
pp: a : ℚ
n : ℕ
h : IsInt a (Int.negOfNat n)
⊢ n = 0 ↔ IsSquare a

Tactic:
refine ⟨fun h' ↦ by simp [h.1, h'], fun ⟨b, hb⟩ ↦ ?_⟩
  rw [h.1, Int.cast_negOfNat] at hb
  rcases eq_or_ne b 0 with rfl | hb₀
  · simp_all
  · refine absurd hb (ne_of_lt ?_)
    exact lt_of_le_of_lt (by simp) (mul_self_pos.mpr hb₀)

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℤ
s : Finset ℤ
hs : Icc m (n - 1) = s
⊢ Ico m n = s

Tactic:
by
  rw [← hs, Icc_sub_one_right_eq_Ico]

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case neg.cons.cons
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
xs_ih : val ∈ ys ↔ x ∈ xs
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : ⟨x, val⟩ ∈ map Prod.toSigma (xs.zip ys)
h₅ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₄ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) ys
h₂ : ∀ a' ∈ ys, y ≠ a'
h₆ : xs.length = ys.length
⊢ val ∈ ys

Tactic:
simp only [Prod.toSigma, List.mem_map, Prod.exists] at h₃
          rcases h₃ with ⟨a, b, h₃, h₄, h₅⟩
          apply (List.of_mem_zip h₃).2

Goal state after: