mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: case h
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ofClass Valued.v).ValueGroup₀ˣ
r s : WithVal v
hr₀ : 0 < Valued.v r
hs₀ : 0 < Valued.v s
hr : Valued.v.restrict r / Valued.v.restrict s = ↑γ
h' : w.restrict.IsEquiv v.restrict
x : R
hx : Valued.v.restrict (x * s.ofVal) < Valued.v.restrict r.ofVal
⊢ Valued.v.restrict (toVal v x) < ↑γ

pp: case h
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ofClass Valued.v).ValueGroup₀ˣ
r s : WithVal v
hr₀ : 0 < Valued.v r
hs₀ : 0 < Valued.v s
hr : Valued.v.restrict r / Valued.v.restrict s = ↑γ
h' : w.restrict.IsEquiv v.restrict
x : R
hx : Valued.v.restrict x < Valued.v.restrict r.ofVal / Valued.v.restrict s.ofVal
⊢ 0 < Valued.v.restrict s.ofVal

Tactic:
restrict_lt_iff,

Goal state after:
case h
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ofClass Valued.v).ValueGroup₀ˣ
r s : WithVal v
hr₀ : 0 < Valued.v r
hs₀ : 0 < Valued.v s
hr : Valued.v.restrict r / Valued.v.restrict s = ↑γ
h' : w.restrict.IsEquiv v.restrict
x : R
hx : Valued.v (x * s.ofVal) < Valued.v r.ofVal
⊢ Valued.v.restrict (toVal v x) < ↑γ

case h
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ofClass Valued.v).ValueGroup₀ˣ
r s : WithVal v
hr₀ : 0 < Valued.v r
hs₀ : 0 < Valued.v s
hr : Valued.v.restrict r / Valued.v.restrict s = ↑γ
h' : w.restrict.IsEquiv v.restrict
x : R
hx : Valued.v.restrict x < Valued.v.restrict r.ofVal / Valued.v.restrict s.ofVal
⊢ 0 < Valued.v.restrict s.ofVal
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: case h
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ofClass Valued.v).ValueGroup₀ˣ
r s : WithVal v
hr₀ : 0 < Valued.v r
hs₀ : 0 < Valued.v s
hr : Valued.v.restrict r / Valued.v.restrict s = ↑γ
h' : w.restrict.IsEquiv v.restrict
x : R
hx : v x * v s.ofVal < v r.ofVal
⊢ Valued.v.restrict (toVal v x) < ↑γ

Tactic:
rw [← hr, lt_div_iff₀ ((restrict_pos_iff Valued.v s).mpr hs₀), ← map_mul, ← lt_def,
      ← h.orderRingIso_apply]
    simp only [orderRingIso_apply, toVal_mul, lt_def, ofVal_mul, restrict_lt_iff]
    rw [map_mul]
    exact hx

Goal state after:
Module: Mathlib.Order.Interval.Finset.DenselyOrdered

Goal state before:
pp: X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
⊢ DenselyOrdered ↑s ↔ s.Subsingleton

Tactic:
refine ⟨fun H ↦ ?_, fun h ↦ h.denselyOrdered⟩

Goal state after:
X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered ↑s
⊢ s.Subsingleton
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
x : K
x_ne : x ≠ 0
s : Set K
s_in : s ∈ 𝓝 x⁻¹
⊢ s ∈ map Inv.inv (𝓝 x)

Tactic:
obtain ⟨γ, hs⟩ := Valued.mem_nhds.mp s_in; clear s_in
      rw [mem_map, Valued.mem_nhds]
      let γ' := Units.mk0 ((ValueGroup₀.restrict₀ _) x) (v.restrict.ne_zero_iff.mpr x_ne)
      use min (γ * (γ' * γ')) γ'
      intro y y_in
      apply hs
      simp only [mem_ofPred_eq, Units.min_val, Units.val_mul] at y_in
      exact Valuation.inversion_estimate _ x_ne y_in

Goal state after:
Module: Mathlib.Order.Interval.Finset.DenselyOrdered

Goal state before:
pp: case refine_2
X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered ↑s
x : X
hx : ↑x ∈ s
y : X
hy : ↑y ∈ s
hxy : x < y
this : ⟨↑x, hx⟩ < ⟨↑y, hy⟩
z : { x // x ∈ s }
hz : ↑x < ↑z
hz' : ↑z < ↑y
⊢ x < (↑z).unbot ⋯

Tactic:
rw [← WithBot.coe_lt_coe]
    simp [hz.trans_le]

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

Goal state before:
pp: case h.right
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
H₀ : ∀ x ∈ M₀, ↑γ₀ ≤ v.restrict x
γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
H₁ : ∀ x ∈ M₁, ∀ y ∈ M₁, v.restrict (y - x) < ↑(min (γ * γ₀ * γ₀) γ₀)
x : K
x_in₀ : x ∈ M₀
x_in₁ : x ∈ M₁
y : K
left✝ : y ∈ M₀
y_in₁ : y ∈ M₁
⊢ v.restrict (y⁻¹ - x⁻¹) < ↑γ

Tactic:
specialize H₁ x x_in₁ y y_in₁

Goal state after:
case h.right
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
H₀ : ∀ x ∈ M₀, ↑γ₀ ≤ v.restrict x
γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
x : K
x_in₀ : x ∈ M₀
x_in₁ : x ∈ M₁
y : K
H₁ : v.restrict (y - x) < ↑(min (γ * γ₀ * γ₀) γ₀)
left✝ : y ∈ M₀
y_in₁ : y ∈ M₁
⊢ v.restrict (y⁻¹ - x⁻¹) < ↑γ
Module: Mathlib.Order.Northcott

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
h' : β → γ
inst✝² : LE γ
inst✝¹ : Northcott h'
inst✝ : Filter.TendstoCofinite h
c : γ
⊢ {a | (h' ∘ h) a ≤ c}.Finite

Tactic:
refine Set.Finite.of_finite_fibers h ?_ fun x _ ↦
      (Filter.TendstoCofinite.finite_preimage_singleton h x).inter_of_right _

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
h' : β → γ
inst✝² : LE γ
inst✝¹ : Northcott h'
inst✝ : Filter.TendstoCofinite h
c : γ
⊢ (h '' {a | (h' ∘ h) a ≤ c}).Finite
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x + y})).factors)) ≤
    max (v.intValuationDef x) (v.intValuationDef y)

Tactic:
v.intValuationDef_if_neg hx,

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x + y})).factors)) ≤
    max (exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors))) (v.intValuationDef y)
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ (mk fun n ↦ a ^ n * (coeff n) 1) = 1

Tactic:
ext1

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a : R
n✝ : ℕ
⊢ (coeff n✝) (mk fun n ↦ a ^ n * (coeff n) 1) = (coeff n✝) 1
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
a b : R
n : ℕ
⊢ (coeff n) ((rescale b) ((rescale a) f)) = (coeff n) ((rescale (a * b)) f)

Tactic:
coeff_rescale

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
a b : R
n : ℕ
⊢ b ^ n * (a ^ n * (coeff n) f) = (a * b) ^ n * (coeff n) f
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r ≠ 0
⊢ v.intValuation r = exp (-↑(multiplicity v.asIdeal (Ideal.span {r})))

Tactic:
by
  have hsr : Ideal.span {r} ≠ 0 := Submodule.span_singleton_eq_bot.mp.mt hr
  have hfm : FiniteMultiplicity v.asIdeal (Ideal.span {r}) :=
    FiniteMultiplicity.of_prime_left v.prime hsr
  rw [v.intValuation_if_neg hr, exp_inj, neg_inj, Int.natCast_inj, ← ENat.natCast_inj,
    ← FiniteMultiplicity.emultiplicity_eq_multiplicity hfm,
    UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors (irreducible v) hsr,
    normalize_eq, Ideal.count_associates_factors_eq hsr v.isPrime v.ne_bot]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}
⊢ (∃ i, True ∧ {x | extensionValuation x < ↑((Units.map ↑embedding) i)} ⊆ s) ↔
    ∃ γ, {x | extensionValuation.restrict x < ↑γ} ⊆ s

Tactic:
simp only [extensionValuation_toFun, Units.coe_map, MonoidHom.coe_coe, true_and]

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}
⊢ (∃ i, {x | embedding (extension x) < embedding ↑i} ⊆ s) ↔ ∃ γ, {x | extensionValuation.restrict x < ↑γ} ⊆ s
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: A : Type u_2
inst✝ : CommRing A
⊢ -C 1 * X = -X

Tactic:
map_one,

Goal state after:
A : Type u_2
inst✝ : CommRing A
⊢ -1 * X = -X
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case e'_4
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff (k i)) f = constantCoeff f
hs'' : ∀ i ∈ s, k i = 0
⊢ degree (∑ x ∈ range n \ s, k x) = ∑ x ∈ range n \ s, degree (k x)

Tactic:
simp only [degree_eq_weight_one, map_sum]

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

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

Tactic:
ENat.forall_ne_top,

Goal state after:
α : Type u_1
l : Filter α
f : α → ℕ∞
⊢ (∀ (x : ℕ), ∀ᶠ (a : α) in l, f a ∈ Ioi ↑x) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, ↑n < f a
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
g : (ofClass (valuation K v)).ValueGroup₀
⊢ embedding ((valueGroupOrderIso K v) g) = embedding g

Tactic:
by
  match g with
  | 0 => simp [valueGroupOrderIso]
  | .coe a => simp [coe_valueGroupOrderIso_coe, embedding_apply, coe_valueGroupEquiv]

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
S : Type u_3
inst✝⁸ : Field K
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
v : HeightOneSpectrum R
inst✝⁴ : Algebra S K
S₀ : Type u_4
inst✝³ : CommSemiring S₀
inst✝² : Algebra S₀ S
inst✝¹ : Algebra S₀ K
inst✝ : IsScalarTower S₀ S K
x : S₀
⊢ ((algebraMap S₀ (adicCompletion K v)) x).toCompletion =
    ((algebraMap S (adicCompletion K v)) ((algebraMap S₀ S) x)).toCompletion

Tactic:
algebraMap_adicCompletion_toCompletion,

Goal state after:
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
inst✝⁴ : Algebra S K
S₀ : Type u_4
inst✝³ : CommSemiring S₀
inst✝² : Algebra S₀ S
inst✝¹ : Algebra S₀ K
inst✝ : IsScalarTower S₀ S K
x : S₀
⊢ (algebraMap S₀ (valuation K v).Completion) x =
    ((algebraMap S (adicCompletion K v)) ((algebraMap S₀ S) x)).toCompletion
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: 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
inst✝⁴ : Algebra S K
S₀ : Type u_4
inst✝³ : CommSemiring S₀
inst✝² : Algebra S₀ S
inst✝¹ : Algebra S₀ K
inst✝ : IsScalarTower S₀ S K
x : S₀
⊢ (algebraMap S₀ (valuation K v).Completion) x =
    ((algebraMap S (adicCompletion K v)) ((algebraMap S₀ S) x)).toCompletion

Tactic:
algebraMap_adicCompletion_toCompletion,

Goal state after:
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
inst✝⁴ : Algebra S K
S₀ : Type u_4
inst✝³ : CommSemiring S₀
inst✝² : Algebra S₀ S
inst✝¹ : Algebra S₀ K
inst✝ : IsScalarTower S₀ S K
x : S₀
⊢ (algebraMap S₀ (valuation K v).Completion) x = (algebraMap S (valuation K v).Completion) ((algebraMap S₀ S) x)
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
⊢ eval₂ G s 0 = ∑ i ∈ range 0, G ((coeff i) f) * s ^ i

Tactic:
range_zero,

Goal state after:
case zero
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
⊢ eval₂ G s 0 = ∑ i ∈ ∅, G ((coeff i) f) * s ^ i
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
ih : n • φ.order ≤ (φ ^ n).order
⊢ (n + 1) • φ.order ≤ (φ ^ (n + 1)).order

Tactic:
add_smul,

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
ih : n • φ.order ≤ (φ ^ n).order
⊢ n • φ.order + 1 • φ.order ≤ (φ ^ (n + 1)).order
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.toNat + 1) * ψ
this : (coeff n) φ = (coeff n) (ψ * X ^ (φ.order.toNat + 1))
h✝ : ¬1 = 0
⊢ ↑n < ↑(φ.order.toNat + 1)

Tactic:
· rw [← hn, ENat.natCast_lt_natCast]
          simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ (X ^ n).order = ↑n

Tactic:
rw [X_pow_eq, order_monomial_of_ne_zero]
  exact one_ne_zero

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

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
a : S
inst✝¹⁰ : UniformSpace R
inst✝⁹ : UniformSpace S
inst✝⁸ : IsUniformAddGroup R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : IsUniformAddGroup S
inst✝⁵ : T2Space S
inst✝⁴ : CompleteSpace S
inst✝³ : IsTopologicalRing S
inst✝² : IsLinearTopology S S
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ha : HasEval a
p : Polynomial R
⊢ (aeval ha) ↑p = (Polynomial.aeval a) p

Tactic:
by
  rw [coe_aeval, Polynomial.aeval_def, eval₂_coe]

Goal state after:
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
a : σ → S
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : IsUniformAddGroup R
inst✝⁶ : IsUniformAddGroup S
inst✝⁵ : CompleteSpace S
inst✝⁴ : T2Space S
inst✝³ : IsTopologicalRing S
inst✝² : IsLinearTopology S S
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ha : HasEval a
⊢ ⇑(aeval ha) = eval₂ (algebraMap R S) a

Tactic:
simp only [aeval, AlgHom.coe_mk, coe_eval₂Hom]

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : σ → MvPowerSeries τ S
p : MvPolynomial σ R
⊢ subst a ↑p = (MvPolynomial.aeval a) p

Tactic:
by
  let : UniformSpace R := ⊥
  let : UniformSpace S := ⊥
  rw [subst_eq_eval₂, eval₂_coe, MvPolynomial.aeval_def]

Goal state after:
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ Uncountable ℝ

Tactic:
by
  rw [← aleph0_lt_mk_iff, mk_real]
  exact aleph0_lt_continuum

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
τ : Type u_4
S : Type u_5
inst✝ : CommRing S
a : σ → MvPowerSeries τ R
ha : HasSubst a
h : R →+* S
f : MvPowerSeries σ R
⊢ (map h) (subst a f) = subst (fun i ↦ (map h) (a i)) ((map h) f)

Tactic:
ext n
  have {r : R} : h r = h.toAddMonoidHom r := rfl
  rw [coeff_subst (ha.map h), coeff_map, coeff_subst ha, this, AddMonoidHom.map_finsum _
    (coeff_subst_finite ha _ _), finsum_congr]
  intro d
  simp [smul_eq_mul, RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.coe_coe, map_mul,
    ← coeff_map, Finsupp.prod]

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

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
τ : Type u_3
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : MvPowerSeries τ S
ha : HasSubst a
f g : R⟦X⟧
⊢ subst a (f * g) = subst a f * subst a g

Tactic:
rw [← coe_substAlgHom ha, map_mul]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
i : ℕ
hn : k ∣ i
⊢ ((ofPowerSeries (q ^ k)) f) (q ^ i) = (algebraMap R R) ((PowerSeries.coeff (i / k)) f)

Tactic:
obtain ⟨j, rfl⟩ := hn
        rw [pow_mul, ofPowerSeries_apply_pow (one_lt_pow' hq hk)]
        simp [hk]

Goal state after:
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
x : E
a : 𝕜
y : E
hy : y ∈ s
hxy : (fun x ↦ a • x) y = c • x
hc : c ≠ 0
⊢ egauge 𝕜 s x ≤ ↑(‖a‖₊ / ‖c‖₊)

Tactic:
div_eq_inv_mul,

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
x : E
a : 𝕜
y : E
hy : y ∈ s
hxy : (fun x ↦ a • x) y = c • x
hc : c ≠ 0
⊢ egauge 𝕜 s x ≤ ↑(‖c‖₊⁻¹ * ‖a‖₊)
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
a : σ → R
f : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (coeff n) ((rescale a) f) = (coeff n) (subst (a • X) f)

Tactic:
coeff_rescale

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
a : σ → R
f : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (n.prod fun s m ↦ a s ^ m) * (coeff n) f = (coeff n) (subst (a • X) f)
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:
div_eq_inv_mul,

Goal state after:
𝕜 : 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‖₊⁻¹ ≤ r⁻¹ * (‖c‖₊ * ‖x‖₊)
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ (MvPowerSeries.coeff e) (subst X₀ f * subst X₁ f) = (coeff (e 0)) f * (coeff (e 1)) f

Tactic:
rw [MvPowerSeries.coeff_mul, Finset.sum_eq_single (single 0 (e 0), single 1 (e 1)) ?_ ?_]
  · grind [coeff_subst_single]
  · intro b hb hb'
    by_contra hmul_ne_zero
    rcases ne_zero_and_ne_zero_of_mul hmul_ne_zero with ⟨h0, h1⟩
    simp only [Fin.isValue, coeff_subst_single, ne_eq, ite_eq_right_iff,
      not_forall, exists_prop] at h0 h1
    apply hb'
    rw [Prod.ext_iff, ← mem_antidiagonal.mp hb, h0.1, h1.1]
    simp
  · intro he
    have he' : single 0 (e 0) + single 1 (e 1) = e := by
      ext i
      fin_cases i <;> simp
    exact absurd (mem_antidiagonal.mpr he') he

Goal state after:
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : 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
f₁ f₂ : α → E
g₁ g₂ : α → F
l : Filter α
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ f₁ =o[𝕜; l] g₁ ↔ f₂ =o[𝕜; l] g₂

Tactic:
simp only [isLittleOTVS_iff_tendsto_div]
  peel with U hU V hV
  exact tendsto_congr' (hf.comp₂ (egauge _ _ · / egauge _ _ ·) hg)

Goal state after:
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : Module 𝕜 F
inst✝² : AddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
k : α → G
hfg : f =O[𝕜; l] g
hgk : g =o[𝕜; l] k
U : Set E
hU₀ : U ∈ 𝓝 0
V : Set F
hV₀ : V ∈ 𝓝 0
hV : (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ egauge 𝕜 V (g x)
W : Set G
hW₀ : W ∈ 𝓝 0
hW : ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 V (g x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 W (k x)
ε : ℝ≥0
hε : ε ≠ 0
⊢ (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 W (k x)

Tactic:
filter_upwards [hV, hW ε hε] with x hx₁ hx₂ using hx₁.trans hx₂

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
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : ¬AccPt x (𝓟 s)
⊢ (fderivWithin 𝕜 f s x) 1 = 0

Tactic:
fderivWithin_zero_of_not_accPt h,

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : ¬AccPt x (𝓟 s)
⊢ 0 1 = 0
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜 E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : ContinuousAdd E
inst✝⁶ : ContinuousSMul 𝕜 E
F : Type u_3
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : TopologicalSpace F
inst✝² : ContinuousAdd F
inst✝¹ : ContinuousSMul 𝕜 F
f : E → F
f' f₁' : E →L[𝕜] F
x : E
inst✝ : T2Space F
h₀ : HasFDerivAtFilter f f' (𝓝 x ×ˢ pure x)
h₁ : HasFDerivAtFilter f f₁' (𝓝 x ×ˢ pure x)
⊢ f' = f₁'

Tactic:
← nhdsWithin_univ

Goal state after:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜 E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : ContinuousAdd E
inst✝⁶ : ContinuousSMul 𝕜 E
F : Type u_3
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : TopologicalSpace F
inst✝² : ContinuousAdd F
inst✝¹ : ContinuousSMul 𝕜 F
f : E → F
f' f₁' : E →L[𝕜] F
x : E
inst✝ : T2Space F
h₀ : HasFDerivAtFilter f f' (𝓝[univ] x ×ˢ pure x)
h₁ : HasFDerivAtFilter f f₁' (𝓝[univ] x ×ˢ pure x)
⊢ f' = f₁'
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x₀ : E
n : ℕ
h : f =O[𝓝 x₀] fun x ↦ ‖x - x₀‖ ^ n
hn : 1 < n
⊢ HasFDerivAt f 0 x₀

Tactic:
← nhdsWithin_univ

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x₀ : E
n : ℕ
h : f =O[𝓝[univ] x₀] fun x ↦ ‖x - x₀‖ ^ n
hn : 1 < n
⊢ HasFDerivAt f 0 x₀