mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: case mpr
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
⊢ (∃ i, {b | b - a ∈ B i} ⊆ s) → ∃ i ∈ hB.toRingFilterBasis.toAddGroupFilterBasis, (fun y ↦ a + y) '' i ⊆ s

Tactic:
rintro ⟨i, hi⟩

Goal state after:
case mpr
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : {b | b - a ∈ B i} ⊆ s
⊢ ∃ i ∈ hB.toRingFilterBasis.toAddGroupFilterBasis, (fun y ↦ a + y) '' i ⊆ s
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case pos
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.addMap ⟦P⟧ ⟦Q⟧ =
    ⟦![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1]⟧

Tactic:
rw [addMap_eq, add_of_Y_ne' hP hQ hPz hQz hx <| not_and.mp hxy hx,
      smul_eq _ <| isUnit_dblZ_of_Y_ne' hP hQ hPz hx <| not_and.mp hxy hx]

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

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z x✝¹ : R
y✝¹ : ↥(posSubmonoid R)
x✝ : R
y✝ : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk x✝¹ y✝¹ * ValueGroupWithZero.mk x✝ y✝ =
    ValueGroupWithZero.mk x✝ y✝ * ValueGroupWithZero.mk x✝¹ y✝¹

Tactic:
apply ValuativeRel.ValueGroupWithZero.sound <;>
    · simp only [Submonoid.coe_mul]
      nth_grw 2 [veq_mul_comm]
      nth_grw 6 [veq_mul_comm]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
W : Jacobian F
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
⊢ (W.map f).add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W.add P Q

Tactic:
by_cases h : P ≈ Q
  · rw [add_of_equiv <| (comp_equiv_comp f hP hQ).mpr h, add_of_equiv h, map_dblXYZ]
  · rw [add_of_not_equiv <| h.comp (comp_equiv_comp f hP hQ).mp, add_of_not_equiv h, map_addXYZ]

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: R K : Type u
inst✝² : Ring R
inst✝¹ : DivisionRing K
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
this : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
⊢ ∀ (s : Set R), s ∈ 𝓝 0 ↔ ∃ γ, {x | v.restrict x < ↑γ} ⊆ s

Tactic:
intro s

Goal state after:
R K : Type u
inst✝² : Ring R
inst✝¹ : DivisionRing K
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
this : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
s : Set R
⊢ s ∈ 𝓝 0 ↔ ∃ γ, {x | v.restrict x < ↑γ} ⊆ s
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: case e'_5
R : Type u_1
inst✝⁵ : Ring R
inst✝⁴ : ValuativeRel R
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
_u : UniformSpace R
inst✝² : IsUniformAddGroup R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
x✝ : (ofClass v).ValueGroup₀ˣ
⊢ {p | v.restrict (p.2 - p.1) < ↑x✝} = (fun p ↦ p.2 + -p.1) ⁻¹' ↑(v.ltAddSubgroup ((Units.map ↑embedding) x✝))

Tactic:
simp [restrict_lt_iff_lt_embedding, sub_eq_add_neg]

Goal state after:
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: case neg
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : IsTopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ (↑x).hatInv = ↑x⁻¹

Tactic:
exact hatInv_extends h

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = span {x}
y : R
hy : Submodule.colon I ↑(span {a}) = span {y}
i : R
hi : i ∈ I
hisup : i ∈ span {x}
hasup : a ∈ span {x}
⊢ i ∈ span {x * y}

Tactic:
mem_span_singleton'

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = span {x}
y : R
hy : Submodule.colon I ↑(span {a}) = span {y}
i : R
hi : i ∈ I
hisup : ∃ a, a * x = i
hasup : ∃ a_1, a_1 * x = a
⊢ i ∈ span {x * y}
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case neg
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsDiscreteValuationRing A
x : A
hx : ¬x = 0
⊢ (maximalIdeal A).intValuation x = (ENat.recTopCoe 0 (fun x ↦ ↑(ofAdd ↑x)) ((addVal A) x))⁻¹

Tactic:
obtain ⟨ϖ, hϖ⟩ := exists_irreducible A

Goal state after:
case neg
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsDiscreteValuationRing A
x : A
hx : ¬x = 0
ϖ : A
hϖ : Irreducible ϖ
⊢ (maximalIdeal A).intValuation x = (ENat.recTopCoe 0 (fun x ↦ ↑(ofAdd ↑x)) ((addVal A) x))⁻¹
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : x = 1
⊢ ↥(closure {x}) ≃*o ↥(closure {y})

Tactic:
refine ⟨⟨⟨fun _ ↦ ⟨1, by simp [hxy.mp hx]⟩, fun _ ↦ ⟨1, by simp [hx]⟩, ?_, ?_⟩, ?_⟩, ?_⟩
    · intro ⟨a, ha⟩
      simpa [hx, closure_singleton_one, eq_comm] using ha
    · intro ⟨a, ha⟩
      simpa [hxy.mp hx, closure_singleton_one, eq_comm] using ha
    · intros
      simp
    · intro ⟨a, ha⟩ ⟨b, hb⟩
      simp only [hx, closure_singleton_one, mem_bot] at ha hb
      simp [ha, hb]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case mpr
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
f : G ≃+o ℤ
this : LocallyFiniteOrder G
⊢ {x | 0 ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2

Tactic:
exact BddBelow.wellFoundedOn_lt ⟨0, by simp [mem_lowerBounds]⟩

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
S : Type u_3
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
n : σ →₀ ℕ
a : R
⊢ (map f) ((monomial n) a) = (monomial n) (f a)

Tactic:
ext m
  simp [coeff_monomial, apply_ite f]

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
hab : extensionValuation.restrict ↑⋯.choose = extensionValuation.restrict ↑⋯.choose
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
hx : v x = embedding a
hy : v y = embedding b
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
ha0 : a = 0
⊢ embedding a = embedding b

pp: case neg
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
hab : extensionValuation.restrict ↑⋯.choose = extensionValuation.restrict ↑⋯.choose
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
hx : v x = embedding a
hy : v y = embedding b
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
ha0 : ¬a = 0
⊢ embedding a = embedding b

Tactic:
· have h0 : extension ((algebraMap K (hat K)) x) = 0 := by
        simpa [ha0, extension_eq_zero_iff, map_eq_zero] using hx
      simp [h0, reduceDIte, extension_eq_zero_iff, map_eq_zero,
        left_eq_dite_iff, WithZero.zero_ne_coe, imp_false, not_not] at this
      simp [ha0, ← hy, this]

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
hab : extensionValuation.restrict ↑⋯.choose = extensionValuation.restrict ↑⋯.choose
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
hx : v x = embedding a
hy : v y = embedding b
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
ha0 : ¬a = 0
⊢ embedding a = embedding b
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
d : σ →₀ ℕ
h✝ : ¬d = 0
⊢ 0 = ↑(#∅)

Tactic:
· simp only [card_empty, Nat.cast_zero]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
a b : R
hv : v.intValuation b ≤ v.intValuation a
γ : Multiplicative ℤ
⊢ ∃ y, v.intValuation (b - y * a) < ↑γ

Tactic:
by_cases ha: a = 0
  · subst ha
    rw [map_zero, le_zero_iff] at hv
    exact ⟨0, by simp [hv]⟩
  · have hvaz := intValuation_ne_zero v a ha
    have hγz : WithZero.coe γ ≠ 0 := WithZero.coe_ne_zero
    -- Otherwise, find `n : ℕ` such that `exp (-n) < γ` and `exp(-n) < v a`.
    obtain ⟨n, hna, hnγ⟩ := exists_exp_neg_natCast_lt_and_lt hvaz hγz
    apply Exists.imp (fun _ h ↦ lt_of_le_of_lt h hnγ)
    -- `v b ≤ v a`, so `b ∈ v.asIdeal ^ -log (v a)`.
    -- From `irreducible_pow_sup_of_ge` we know that
    -- `v.asIdeal ^ -log (v a) = v.asIdeal ^ n ⊔ Ideal.span {a}`.
    -- So, `∃ z ∈ v.asIdeal ^ n, ∃ (y: R), b = z + y * a`. This gives `z` and `y` such that
    -- `b - y * a = z` and `v z ≤ exp (-n)`, as required.
    have hvn : emultiplicity v.asIdeal (Ideal.span {a}) ≤ n := by
      grw [← exp_le_intValuation_iff_emultiplicity_le, hna]
    have hb : b ∈ v.asIdeal ^ multiplicity v.asIdeal (Ideal.span {a}) := by
      rwa [← intValuation_le_pow_iff_mem, ← v.intValuation_eq_exp_neg_multiplicity ha]
    have hnz : Ideal.span {a} ≠ ⊥ := by rwa [ne_eq, Ideal.span_singleton_eq_bot]
    simpa [← Ideal.irreducible_pow_sup_of_ge hnz v.irreducible n hvn, Submodule.mem_sup,
      ← eq_sub_iff_add_eq, ← intValuation_le_pow_iff_mem, Ideal.mem_span_singleton'] using hb

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ (ofClass (valuation K v)).valueGroup = (ofClass Valued.v).valueGroup

Tactic:
simp [valuation, valueGroup, valueMonoid, ← (toCompletion_surjective K v).range_comp]; rfl

Goal state after:
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℕ∞
⊢ Tendsto f l (𝓝 ⊤) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, ↑n < f a

Tactic:
simp_rw [nhds_top_order, lt_top_iff_ne_top, tendsto_iInf, tendsto_principal, ENat.forall_ne_top,
    mem_Ioi]

Goal state after:
Module: Mathlib.Topology.Algebra.TopologicallyNilpotent

Goal state before:
pp: R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : Ring R
inst✝ : IsLinearTopology R R
a b : R
ha : IsTopologicallyNilpotent a
hb : IsTopologicallyNilpotent b
h : Commute a b
⊢ ∀ (ib : Ideal R), ↑ib ∈ 𝓝 0 → ∃ ia, ∀ x ∈ Set.Ici ia, (a + b) ^ x ∈ ↑ib

Tactic:
intro I

Goal state after:
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : Ring R
inst✝ : IsLinearTopology R R
a b : R
ha : IsTopologicallyNilpotent a
hb : IsTopologicallyNilpotent b
h : Commute a b
I : Ideal R
⊢ ↑I ∈ 𝓝 0 → ∃ ia, ∀ x ∈ Set.Ici ia, (a + b) ^ x ∈ ↑I
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case refine_2.refine_2
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
s : Set (adicCompletion K v)
x✝ : ∃ γ, {x | (valuation K v).restrict x < ↑γ} ⊆ s
γ : (ofClass (valuation K v)).ValueGroup₀ˣ
hγ : {x | (valuation K v).restrict x < ↑γ} ⊆ s
x : adicCompletion K v
hx : x ∈ toCompletion ⁻¹' {y | Valued.v.restrict y < ↑((Units.mapEquiv (valueGroupOrderIso K v).toMulEquiv) γ)}
⊢ (valuation K v).restrict x < ↑γ

Tactic:
← map_lt_map_iff (valueGroupOrderIso K v),

Goal state after:
case refine_2.refine_2
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
s : Set (adicCompletion K v)
x✝ : ∃ γ, {x | (valuation K v).restrict x < ↑γ} ⊆ s
γ : (ofClass (valuation K v)).ValueGroup₀ˣ
hγ : {x | (valuation K v).restrict x < ↑γ} ⊆ s
x : adicCompletion K v
hx : x ∈ toCompletion ⁻¹' {y | Valued.v.restrict y < ↑((Units.mapEquiv (valueGroupOrderIso K v).toMulEquiv) γ)}
⊢ (valueGroupOrderIso K v) ((valuation K v).restrict x) < (valueGroupOrderIso K v) ↑γ
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
p : ℕ
hf : f.IsHomogeneous p
d : σ →₀ ℕ
hd : degree d ≠ p
⊢ (coeff d) f = 0

Tactic:
by
  apply IsWeightedHomogeneous.coeff_eq_zero hf
  rwa [degree_eq_weight_one] at hd

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: case inr
σ : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : CommSemiring R
ι : Type u_5
f : ι → MvPowerSeries σ R
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
w : σ → ℕ
hempty : Nonempty ι
d : σ →₀ ℕ
h : ∀ (n : ℕ), ∃ a, ∀ (b : ι), a ≤ b → ↑n < weightedOrder w (f b)
i : ι
hi : ∀ (b : ι), i ≤ b → ↑((Finsupp.weight w) d) < weightedOrder w (f b)
⊢ ∀ (s : Finset ι), (coeff d) (∏ i ∈ s, f i) ≠ 0 → ↑s ⊆ Set.Iio i

Tactic:
intro s

Goal state after:
case inr
σ : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : CommSemiring R
ι : Type u_5
f : ι → MvPowerSeries σ R
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
w : σ → ℕ
hempty : Nonempty ι
d : σ →₀ ℕ
h : ∀ (n : ℕ), ∃ a, ∀ (b : ι), a ≤ b → ↑n < weightedOrder w (f b)
i : ι
hi : ∀ (b : ι), i ≤ b → ↑((Finsupp.weight w) d) < weightedOrder w (f b)
s : Finset ι
⊢ (coeff d) (∏ i ∈ s, f i) ≠ 0 → ↑s ⊆ Set.Iio i
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ φ.order = MvPowerSeries.order φ

Tactic:
by
  refine eq_of_le_of_ge ?_ ?_
  · refine MvPowerSeries.le_order fun d hd => by
      have : coeff ↑(Finsupp.degree d) φ = 0 := coeff_of_lt_order _ hd
      have eq_aux : d.degree = d () := Finset.sum_eq_single _ (by simp) (by simp)
      exact (PowerSeries.coeff_def rfl (R := R)) ▸ (eq_aux ▸ this)
  · refine le_order φ (MvPowerSeries.order φ) fun i hi => by
      rw [← Finsupp.degree_single () i] at hi
      exact MvPowerSeries.coeff_of_lt_order hi

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

Goal state before:
pp: case neg.left
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : ↑i = ↑n
⊢ (coeff i) ((monomial n) a) ≠ 0

Tactic:
simp only [Nat.cast_inj] at hi
      rwa [hi, coeff_monomial_same]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
⊢ ((trunc n) (↑((trunc n) f) * g)).coeff m = ((trunc n) (f * g)).coeff m

Tactic:
rw [coeff_trunc, coeff_trunc]

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
⊢ (if m < n then (coeff m) (↑((trunc n) f) * g) else 0) = if m < n then (coeff m) (f * g) else 0
Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace M
inst✝ : IsLinearTopology R M
ι : Type u_4
f : Filter ι
a : ι → R
m : ι → M
ha : ∀ (i : Submodule R M), ↑i ∈ 𝓝 0 → ∀ᶠ (x : ι) in f, m x ∈ ↑i
⊢ ∀ (i : Submodule R M), ↑i ∈ 𝓝 0 → ∀ᶠ (x : ι) in f, (a • m) x ∈ ↑i

Tactic:
intro I

Goal state after:
R : Type u_1
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace M
inst✝ : IsLinearTopology R M
ι : Type u_4
f : Filter ι
a : ι → R
m : ι → M
ha : ∀ (i : Submodule R M), ↑i ∈ 𝓝 0 → ∀ᶠ (x : ι) in f, m x ∈ ↑i
I : Submodule R M
⊢ ↑I ∈ 𝓝 0 → ∀ᶠ (x : ι) in f, (a • m) x ∈ ↑I
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R⟦X⟧
n : ℕ
⊢ (trunc n) ((map f) p) = Polynomial.map f ((trunc n) p)

Tactic:
ext m; simp [coeff_trunc, apply_ite f]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : CommSemiring R
ι : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ a, ∀ (b : ι), a ≤ b → ↑n < (f b).order
i : ι
hi : ∀ (b : ι), i ≤ b → ↑n < (f b).order
⊢ ∀ (s : Finset ι), (coeff n) (∏ i ∈ s, f i) ≠ 0 → ↑s ⊆ Set.Iio i

Tactic:
intro s

Goal state after:
case inr
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : CommSemiring R
ι : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ a, ∀ (b : ι), a ≤ b → ↑n < (f b).order
i : ι
hi : ∀ (b : ι), i ≤ b → ↑n < (f b).order
s : Finset ι
⊢ (coeff n) (∏ i ∈ s, f i) ≠ 0 → ↑s ⊆ Set.Iio i
Module: Mathlib.RingTheory.MvPowerSeries.Evaluation

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : UniformSpace R
S : Type u_3
inst✝⁴ : CommRing S
inst✝³ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝² : IsUniformAddGroup R
inst✝¹ : IsUniformAddGroup S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁵.toTopologicalSpace, inst✝³.toTopologicalSpace] ⇑φ
ha : HasEval a
⊢ ∀ (i : Ideal S), ↑i ∈ 𝓝 0 → ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, (eval₂Hom φ a) x ∈ ↑i

Tactic:
intro I

Goal state after:
σ : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : UniformSpace R
S : Type u_3
inst✝⁴ : CommRing S
inst✝³ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝² : IsUniformAddGroup R
inst✝¹ : IsUniformAddGroup S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁵.toTopologicalSpace, inst✝³.toTopologicalSpace] ⇑φ
ha : HasEval a
I : Ideal S
⊢ ↑I ∈ 𝓝 0 → ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, (eval₂Hom φ a) x ∈ ↑I
Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsLinearTopology R R
f : MvPowerSeries σ R
hf : IsTopologicallyNilpotent (constantCoeff f)
d : σ →₀ ℕ
I : Ideal R
hI : ↑I ∈ 𝓝 0
⊢ ∀ᶠ (x : ℕ) in atTop, (coeff d) (f ^ x) ∈ ↑I

Tactic:
replace hf := hf.eventually_mem hI

Goal state after:
σ : Type u_1
R : Type u_3
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsLinearTopology R R
f : MvPowerSeries σ R
d : σ →₀ ℕ
I : Ideal R
hI : ↑I ∈ 𝓝 0
hf : ∀ᶠ (x : ℕ) in atTop, constantCoeff f ^ x ∈ ↑I
⊢ ∀ᶠ (x : ℕ) in atTop, (coeff d) (f ^ x) ∈ ↑I
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
a : σ → MvPowerSeries τ S
x : σ → ℕ
inst✝ : Finite τ
ha : HasSubst a
d : τ →₀ ℕ
i : σ
⊢ i ∈ {s | (coeff d) ↑((MvPowerSeries.truncTotal (x s)) (a s)) ≠ 0} → i ∈ {s | (coeff d) (a s) ≠ 0}

Tactic:
by contrapose; simp +contextual [coeff_truncTotal_eq_ite]

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
q n : ℕ
hq : 1 < q
⊢ { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) 1) 0, map_zero' := ⋯ } n = 1 n

Tactic:
by_cases hn : ∃ k, q ^ k = n

Goal state after:
case pos
R : Type u_1
inst✝ : CommSemiring R
q n : ℕ
hq : 1 < q
hn : ∃ k, q ^ k = n
⊢ { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) 1) 0, map_zero' := ⋯ } n = 1 n

case neg
R : Type u_1
inst✝ : CommSemiring R
q n : ℕ
hq : 1 < q
hn : ¬∃ k, q ^ k = n
⊢ { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) 1) 0, map_zero' := ⋯ } n = 1 n
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
x : R
n : ℕ
hq : 1 < q
⊢ Function.extend (fun x ↦ q ^ x) (fun x_1 ↦ (PowerSeries.coeff x_1) (x • 1)) 0 n = (x • 1) n

Tactic:
by_cases hn : ∃ k, q ^ k = n

Goal state after:
case pos
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
x : R
n : ℕ
hq : 1 < q
hn : ∃ k, q ^ k = n
⊢ Function.extend (fun x ↦ q ^ x) (fun x_1 ↦ (PowerSeries.coeff x_1) (x • 1)) 0 n = (x • 1) n

case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
x : R
n : ℕ
hq : 1 < q
hn : ¬∃ k, q ^ k = n
⊢ Function.extend (fun x ↦ q ^ x) (fun x_1 ↦ (PowerSeries.coeff x_1) (x • 1)) 0 n = (x • 1) n
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case h₂
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : f =O[atTop] fun n ↦ ↑n ^ (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖↑x_1 ^ (x - 1)‖
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ‖f b‖ ≤ C * ‖↑b ^ (x - 1)‖
C' : ℝ := max C ((insert 0 (image (fun n ↦ ‖f n‖ / ↑n ^ (x - 1)) (range m))).max' ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀✝ : n ≠ 0
hn : m ≤ n
hn₀ : 0 ≤ ↑n
⊢ |↑n| ^ (x - 1) ≤ ↑n ^ (x - 1)

Tactic:
abs_of_nonneg hn₀

Goal state after:
case h₂
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : f =O[atTop] fun n ↦ ↑n ^ (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖↑x_1 ^ (x - 1)‖
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ‖f b‖ ≤ C * ‖↑b ^ (x - 1)‖
C' : ℝ := max C ((insert 0 (image (fun n ↦ ‖f n‖ / ↑n ^ (x - 1)) (range m))).max' ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀✝ : n ≠ 0
hn : m ≤ n
hn₀ : 0 ≤ ↑n
⊢ ↑n ^ (x - 1) ≤ ↑n ^ (x - 1)
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ≥0
hc : 1 < ‖c‖
h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0
this : NontriviallyNormedField 𝕜 := { toNormedField := inst✝², non_trivial := ⋯ }
hr : 0 < r
hx : ‖x‖ ≠ 0
a : 𝕜
ha₀ : a ≠ 0
har : ‖a • x‖ < ↑r
hainv : ‖a‖⁻¹ ≤ (↑r)⁻¹ * ‖c‖ * ‖x‖
⊢ ↑‖a‖₊⁻¹ ≤ ↑(‖c‖₊ * ‖x‖₊ / r)

Tactic:
rwa [ENNReal.coe_le_coe, div_eq_inv_mul, ← mul_assoc]

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
this : Invertible ((coeff 1) P.substInv)
Q : R⟦X⟧ := P.substInv.substInv
hQ : HasSubst Q
eq_aux : subst Q P.substInv = X
⊢ Q = subst Q X

Tactic:
subst_X hQ

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
this : Invertible ((coeff 1) P.substInv)
Q : R⟦X⟧ := P.substInv.substInv
hQ : HasSubst Q
eq_aux : subst Q P.substInv = X
⊢ Q = Q
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: case refine_1
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
ιE : Sort u_7
ιF : Sort u_8
pE : ιE → Prop
pF : ιF → Prop
sE : ιE → Set E
sF : ιF → Set F
hE : (𝓝 0).HasBasis pE sE
hF : (𝓝 0).HasBasis pF sF
s t : Set E
hsub : s ⊆ t
V : Set F
hV₀ : V ∈ 𝓝 0
hV : ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 s (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 V (g x)
⊢ ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 t (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 V (g x)

Tactic:
exact ⟨V, hV₀, fun ε hε ↦ (hV ε hε).mono fun x ↦ le_trans <| egauge_anti _ hsub _⟩

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
c : F
⊢ derivWithin (fun x ↦ c) s = 0

Tactic:
by
  ext; simp [derivWithin]

Goal state after: