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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝ : CommRing R
α : Type u_2
x : α → 𝕎 R
a : α
S' : Finset α
ha : a ∉ S'
h : ∀ (n : ℕ), Subsingleton ↑{r | r ∈ insert a S' ∧ (x r).coeff n ≠ 0}
n : ℕ
this : ∀ (n : ℕ), Subsingleton ↑{r | r ∈ S' ∧ (x r).coeff n ≠ 0}
hind : ∀ (n : ℕ), (∑ s ∈ S', x s).coeff n = ∑ s ∈ S', (x s).coeff n
m : ℕ
hma : (x a).coeff m ≠ 0
hmS' : ∑ s ∈ S', (x s).coeff m ≠ 0
⊢ False

Tactic:
have := Finset.sum_eq_zero.mt hmS'

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝ : CommRing R
α : Type u_2
x : α → 𝕎 R
a : α
S' : Finset α
ha : a ∉ S'
h : ∀ (n : ℕ), Subsingleton ↑{r | r ∈ insert a S' ∧ (x r).coeff n ≠ 0}
n : ℕ
this✝ : ∀ (n : ℕ), Subsingleton ↑{r | r ∈ S' ∧ (x r).coeff n ≠ 0}
hind : ∀ (n : ℕ), (∑ s ∈ S', x s).coeff n = ∑ s ∈ S', (x s).coeff n
m : ℕ
hma : (x a).coeff m ≠ 0
hmS' : ∑ s ∈ S', (x s).coeff m ≠ 0
this : ¬∀ x_1 ∈ S', (x x_1).coeff m = 0
⊢ False
Module: Mathlib.RingTheory.WittVector.TeichmullerSeries

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
n : ℕ
x : R
⊢ ((teichmuller p) x * ↑p ^ n).coeff n = x ^ p ^ n

Tactic:
simpa using WittVector.mul_pow_charP_coeff_succ (teichmuller p x) (m := 0)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ dickson 2 0 0 = X ^ 0

Tactic:
by
    simp only [dickson_zero, pow_zero]
    norm_num

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

Goal state before:
pp: case pos
n k : ℕ
h : Even (n + k)
⊢ (hermite n).coeff k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(n.choose k)

pp: case neg
n k : ℕ
h : ¬Even (n + k)
⊢ (hermite n).coeff k = 0

Tactic:
· exact coeff_hermite_of_even_add h

Goal state after:
case neg
n k : ℕ
h : ¬Even (n + k)
⊢ (hermite n).coeff k = 0
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = (X - C 1) ^ rootMultiplicity 1 p * q
hq2 : ¬X - C 1 ∣ q
⊢ (p.hilbertPoly d).natDegree = d - rootMultiplicity 1 p - 1

Tactic:
have heq : p = q * (-1) ^ p.rootMultiplicity 1 * (1 - X) ^ p.rootMultiplicity 1 := by
    simp only [mul_assoc, ← mul_pow, neg_mul, one_mul, neg_sub]
    exact hq1.trans (mul_comm _ _)

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = (X - C 1) ^ rootMultiplicity 1 p * q
hq2 : ¬X - C 1 ∣ q
heq : p = q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p
⊢ (p.hilbertPoly d).natDegree = d - rootMultiplicity 1 p - 1
Module: Mathlib.RingTheory.PowerSeries.Restricted

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

Tactic:
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.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
r a b : R
f✝ g✝ f g h : M →ₚₗ[R] N
⊢ f + g + h = f + (g + h)

Tactic:
ext; simp only [add_def, add_assoc]

Goal state after:
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
r a b : R
f✝ g f : M →ₚₗ[R] N
⊢ 0 + f = f

Tactic:
by ext; simp only [add_def, zero_add, zero_def]

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: case inr.refine_1
z : ℤ
hz : z ≠ 0
p : ℕ
x✝ : Prime ↑p ∧ 0 ≤ ↑p ∧ ↑p ∣ z
pp : Nat.Prime p
dp : ↑p ∣ z
⊢ ∃ a ∈ z.natAbs.primeFactors, Nat.castEmbedding.toFun a = ↑p

Tactic:
rw [Int.natCast_dvd] at dp

Goal state after:
case inr.refine_1
z : ℤ
hz : z ≠ 0
p : ℕ
x✝ : Prime ↑p ∧ 0 ≤ ↑p ∧ ↑p ∣ z
pp : Nat.Prime p
dp : p ∣ z.natAbs
⊢ ∃ a ∈ z.natAbs.primeFactors, Nat.castEmbedding.toFun a = ↑p
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
⊢ Free R M

Tactic:
let f := b'.symm.toLinearMap.comp (Finsupp.mapRange.linearMap (Submodule.mkQ (Ideal.span {x})))

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}))
⊢ Free R M
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case inr.degree_lt
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
inst✝ : IsAdicComplete I A
hI : I ≠ ⊤
⊢ (H.mod f).degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat

Tactic:
exact degree_trunc_lt _ _

Goal state after:
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
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ (rTensor M A.val.toLinearMap).range
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (rTensor M (φ R gen).toLinearMap) p = t
⊢ s ∈ A ⊔ Algebra.adjoin R ↑{s}

Tactic:
apply Algebra.subset_adjoin

Goal state after:
R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ (rTensor M A.val.toLinearMap).range
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (rTensor M (φ R gen).toLinearMap) p = t
⊢ s ∈ ↑A ⊔ ↑(Algebra.adjoin R ↑{s})
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
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 := Finset.image (⇑h) s
⊢ ∀ (x : ↥(φ R s).range), (h.comp (φ R s).range.val) x ∈ (φ R s').range

Tactic:
rintro ⟨x, hx⟩
    simp only [range_φ] at hx ⊢
    simp only [AlgHom.coe_comp, Subalgebra.coe_val, Function.comp_apply, Finset.coe_image,
      Algebra.adjoin_image, s']
    exact ⟨x, hx, rfl⟩

Goal state after:
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
f : M →ₚₗ[R] N
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] (⇑(TensorProduct.lid R N) ∘ toFun R f ∘ ⇑(TensorProduct.lid R M).symm) x = toFun S f (1 ⊗ₜ[R] x)

Tactic:
convert! f.isCompat_apply (Algebra.ofId R S) (1 ⊗ₜ[R] x)

Goal state after:
case e'_2
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
f : M →ₚₗ[R] N
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] (⇑(TensorProduct.lid R N) ∘ toFun R f ∘ ⇑(TensorProduct.lid R M).symm) x =
    (rTensor N (Algebra.ofId R S).toLinearMap) (toFun R f (1 ⊗ₜ[R] x))

case e'_3
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
f : M →ₚₗ[R] N
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] x = (rTensor M (Algebra.ofId R S).toLinearMap) (1 ⊗ₜ[R] x)
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case pos
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
f g : A⟦X⟧
inst✝ : IsPrecomplete (IsLocalRing.maximalIdeal A) A
hg : (map (IsLocalRing.residue A)) g ≠ 0
⊢ (IsWeierstrassDivisorAt.mod ⋯ f).degree < ↑((map (IsLocalRing.residue A)) g).order.toNat

Tactic:
exact degree_trunc_lt _ _

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
g' : A⟦X⟧
f' : A[X]
h' : A⟦X⟧
H' : g'.IsWeierstrassFactorizationAt f' h' I
⊢ g * g' = ↑(f * f') * (h * h')

Tactic:
rw [H.eq_mul, H'.eq_mul, Polynomial.coe_mul]

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
g' : A⟦X⟧
f' : A[X]
h' : A⟦X⟧
H' : g'.IsWeierstrassFactorizationAt f' h' I
⊢ ↑f * h * (↑f' * h') = ↑f * ↑f' * (h * h')
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
S c : Submodule R M
hc : c ∈ isotypicComponents R M
inst✝ : IsSimpleModule R ↥S
le : S ≤ c
⊢ c = isotypicComponent R M ↥S

Tactic:
obtain ⟨S', _, rfl⟩ := hc
  have ⟨e⟩ := isIsotypicOfType_submodule_iff.mp (.isotypicComponent R M S') _ le
  exact e.symm.isotypicComponent_eq

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
l : List ι
f : ι → R
hl : ∀ x ∈ l, f x ∈ I
⊢ (List.map f l).sum ∈ I

Tactic:
mem_iff,

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
l : List ι
f : ι → R
hl : ∀ x ∈ l, f x ∈ I
⊢ I.ringCon (List.map f l).sum 0
Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Multiset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ (Multiset.map f s).sum ∈ I

Tactic:
mem_iff,

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Multiset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ I.ringCon (Multiset.map f s).sum 0
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
⊢ s.sum f ∈ I

Tactic:
mem_iff,

Goal state after:
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) 0
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
        ↑p ^ (n + 1) * X (0, n + 1) *
          ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      ↑p ^ (n + 1) * X (1, n + 1) *
        ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
    remainder p n

Tactic:
enter [1, 1, 2, 2]

Goal state after:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))
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
⊢ IsClub (⋂₀ s)

Tactic:
cases isEmpty_or_nonempty α; · simp
  obtain hα | hα := hα.lt_or_gt
  · exact .sInter_of_cof_le_one (cof_lt_aleph0_iff.1 hα) hs
  refine ⟨.sInter fun x hx ↦ (hs x hx).dirSupClosed, fun a ↦ ?_⟩
  choose f hf using fun x : s ↦ (hs _ x.2).isCofinal
  let g : ℕ → α := Nat.rec a fun _ IH ↦ sSup (.range (f · IH))
  have hg : BddAbove (.range g) := by
    refine .of_not_isCofinal fun hg ↦ (cof_le hg).not_gt (hα.trans_le' ?_)
    simpa using mk_range_le_lift (f := g)
  refine ⟨_, fun t ht ↦ ?_, le_csSup hg ⟨0, rfl⟩⟩
  apply (hs t ht).isLUB_mem (t := .range fun n ↦ f ⟨t, ht⟩ (g n)) _ (range_nonempty _)
  · refine ⟨?_, fun b hb ↦ csSup_le' ?_⟩ <;> rintro _ ⟨n, rfl⟩
    · apply (le_csSup (.of_not_isCofinal _) _).trans (le_csSup hg ⟨n + 1, rfl⟩)
      · exact fun hg' ↦ (cof_le hg').not_gt (mk_range_le.trans_lt hsα)
      · use ⟨t, ht⟩
    · exact (hf ⟨t, ht⟩ _).2.trans <| hb ⟨_, rfl⟩
  · grind

Goal state after:
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
⊢ (coeff b o) 0 = (single 0 o) 0

pp: case inr.inr
b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
ho : o ≠ 0
ha : a ≠ 0
⊢ (coeff b o) a = (single 0 o) a

Tactic:
· apply coeff_of_mem_CNF
      rw [CNF.of_le_one hb ho]
      simp

Goal state after:
case inr.inr
b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
ho : o ≠ 0
ha : a ≠ 0
⊢ (coeff b o) a = (single 0 o) a
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: case neg
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
s : Set α
ha : ∃ b, b < a
⊢ (∃ᶠ (y : α) in 𝓝 a, y ≠ a ∧ y ∈ s) ↔ (∃ b, b < a) ∧ ∀ b < a, (s ∩ Ioo b a).Nonempty

Tactic:
simp_rw [(hasBasis_nhds_Ioc_of_exists_lt ha).frequently_iff, Set.Nonempty, mem_inter_iff]

Goal state after:
case neg
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
s : Set α
ha : ∃ b, b < a
⊢ (∀ i < a, ∃ x ∈ Ioc i a, x ≠ a ∧ x ∈ s) ↔ (∃ b, b < a) ∧ ∀ b < a, ∃ x ∈ s, x ∈ Ioo b a
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x : PSet.{u_1}
⊢ (mk x).Nonempty ↔ x.Nonempty

Tactic:
refine ⟨?_, fun ⟨a, h⟩ => ⟨mk a, h⟩⟩

Goal state after:
x : PSet.{u_1}
⊢ (mk x).Nonempty → x.Nonempty
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o₁ o₂ : Ordinal.{u}
h : o₁ < o₂
⊢ veblenWith f o₁ 0 < veblenWith f o₂ 0

Tactic:
← veblenWith_veblenWith_of_lt hf h,

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o₁ o₂ : Ordinal.{u}
h : o₁ < o₂
⊢ veblenWith f o₁ 0 < veblenWith f o₁ (veblenWith f o₂ 0)
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ (match cmp o₁ o₂ with
      | Ordering.eq => cmp a b
      | Ordering.lt => cmp a (veblenWith f o₂ b)
      | Ordering.gt => cmp (veblenWith f o₁ a) b) =
      Ordering.lt ↔
    o₁ = o₂ ∧ a < b ∨ o₁ < o₂ ∧ a < veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a < b

Tactic:
aesop (add simp lt_asymm)

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ (match cmp o₁ o₂ with
      | Ordering.eq => cmp a b
      | Ordering.lt => cmp a (veblenWith f o₂ b)
      | Ordering.gt => cmp (veblenWith f o₁ a) b) =
      Ordering.eq ↔
    o₁ = o₂ ∧ a = b ∨ o₁ < o₂ ∧ a = veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a = b

Tactic:
aesop (add simp lt_asymm)

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

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

Tactic:
have ee := @cmp_compares _ _ h₁.fst h₂.fst

Goal state after:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
ee : (e₁.cmp e₂).Compares e₁ e₂
⊢ (match e₁.cmp e₂ with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match ↑n₁ - ↑n₂ with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).repr =
    (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: x y : Class.{u}
h : Set.Nonempty x
⊢ y ∈ ⋂₀ x ↔ ∀ z ∈ x, y ∈ z

Tactic:
by
  refine ⟨fun hy z => mem_of_mem_sInter hy, fun H => ?_⟩
  simp_rw [mem_def, sInter_apply]
  obtain ⟨z, hz⟩ := h
  obtain ⟨y, rfl, _⟩ := H z (coe_mem.2 hz)
  refine ⟨y, rfl, fun w hxw => ?_⟩
  simpa only [coe_mem, coe_apply] using H w (coe_mem.2 hxw)

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

Goal state before:
pp: e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
⊢ (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).NFBelow (e₁.repr + b₂)

Tactic:
by_cases e0 : e₂ = 0 <;> simp only [e0, oadd_mul, ↓reduceIte]

Goal state after:
case pos
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : e₂ = 0
⊢ (e₁.oadd (n₁ * n₂) a₁).NFBelow (e₁.repr + b₂)

case neg
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : ¬e₂ = 0
⊢ ((e₁ + e₂).oadd n₂ (e₁.oadd n₁ a₁ * a₂)).NFBelow (e₁.repr + b₂)
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: case limit
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ (V_ o).card = preBeth o

Tactic:
preBeth_limit ho.isSuccPrelimit,

Goal state after:
case limit
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ (V_ o).card = ⨆ a, preBeth ↑a
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝¹ : e.NF
this✝ : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + ↑m'
this : ¬e.repr = repr 0
⊢ ω ^ e.repr = ω ^ 1 * ω ^ (e.repr - 1)

Tactic:
rw [← opow_add, Ordinal.add_sub_cancel_of_le (one_le_iff_ne_zero.2 this)]

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r : R
h : r = 0
⊢ r • 1 = 0

Tactic:
by
  simp [h]

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r s : R
h : r = s
⊢ r • 1 = s • 1

Tactic:
by
  simp [h]

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: A : Type u_2
sA : CommSemiring A
c a b : A
h : a = b
⊢ c * a = c * b

Tactic:
by
  simp [h]

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

Goal state before:
pp: o e : ONote
n : ℕ+
a : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (e.oadd n a, m)
⊢ a.repr + ↑m < ω ^ e.repr

Tactic:
obtain ⟨h₁, h₂⟩ := nf_repr_split h

Goal state after:
o e : ONote
n : ℕ+
a : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (e.oadd n a, m)
h₁ : (e.oadd n a).NF
h₂ : o.repr = (e.oadd n a).repr + ↑m
⊢ a.repr + ↑m < ω ^ e.repr
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
t : ℝ
h1 : 0 < f t
h2 : (f ^ exp') t = 0
⊢ ¬(f ^ exp') t = 0

Tactic:
exact (Real.rpow_pos_of_pos h1 _).ne.symm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
s : Stream' (Option α)
hs : ∀ U ∈ nhds s, (U ∩ {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}).Nonempty
n : ℕ
hn : s n = none
t : Stream' (Option α)
hts : dist t s < (1 / 2) ^ (n + 1)
ht : t ∈ {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}
⊢ s (n + 1) = none

Tactic:
← PiNat.apply_eq_of_dist_lt hts (by simp)

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
s : Stream' (Option α)
hs : ∀ U ∈ nhds s, (U ∩ {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}).Nonempty
n : ℕ
t : Stream' (Option α)
hn : t n = none
hts : dist t s < (1 / 2) ^ (n + 1)
ht : t ∈ {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}
⊢ s (n + 1) = none
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
x y : α
s t : Stream'.Seq α
h : x ≠ y
⊢ dist (Seq.cons x s) (Seq.cons y t) = 1

Tactic:
apply dist_eq_one_of_head
  simpa

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α :=
  fun f b ↦
    match F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
hT : LipschitzWith 2⁻¹ T
f : β → Stream'.Seq α
hf : Function.IsFixedPt T f
b : β
⊢ match F b with
  | none =>
    (match F b with
      | none => nil
      | some (a, c, b') => Seq.cons a (op c (f b'))) =
      nil
  | some (a, c, b') =>
    (match F b with
      | none => nil
      | some (a, c, b') => Seq.cons a (op c (f b'))) =
      Seq.cons a
        (op c
          (match F b' with
          | none => nil
          | some (a, c, b') => Seq.cons a (op c (f b'))))

Tactic:
cases hb : F b with
  | none =>
    simp
  | some v =>
    obtain ⟨a, c, b'⟩ := v
    simp only [cons_eq_cons, true_and]
    congr
    change f b' = T f b'
    rw [hf]

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

Goal state before:
pp: α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
h : ∀ (s t : Stream'.Seq α), dist (op s) (op t) ≤ dist s t
x y : Stream'.Seq α
⊢ dist (op (Seq.cons hd x)).tail (op (Seq.cons hd y)).tail ≤ dist x y

Tactic:
specialize h (.cons hd x) (.cons hd y)

Goal state after:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
x y : Stream'.Seq α
h : dist (op (Seq.cons hd x)) (op (Seq.cons hd y)) ≤ dist (Seq.cons hd x) (Seq.cons hd y)
⊢ dist (op (Seq.cons hd x)).tail (op (Seq.cons hd y)).tail ≤ dist x y
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic

Goal state before:
pp: basis : Basis
c : ℝ
⊢ (const basis c).toFun = fun x ↦ c

Tactic:
by
  match basis with
  | [] => simp [const, ofReal, toReal]
  | List.cons _ _ => simp [const]

Goal state after: