mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : Semiring R
inst✝² : ValuativeRel R
inst✝¹ : IsDiscrete R
inst✝ : IsNontrivial R
a : ValueGroupWithZero R
ha : ¬a = 0
⊢ (uniformizer R)⁻¹ ≤ a ↔ 1 < a

Tactic:
replace ha : 0 < a := bot_lt_iff_ne_bot.mpr ha

Goal state after:
case neg
R : Type u_1
inst✝³ : Semiring R
inst✝² : ValuativeRel R
inst✝¹ : IsDiscrete R
inst✝ : IsNontrivial R
a : ValueGroupWithZero R
ha : 0 < a
⊢ (uniformizer R)⁻¹ ≤ a ↔ 1 < a
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: K✝ : Type u_1
inst✝⁴ : Field K✝
inst✝³ : UniformSpace K✝
L : Type u_2
inst✝² : Field L
inst✝¹ : UniformSpace L
inst✝ : CompletableTopField L
K : Subfield L
F : Filter ↥K
F_cau : Cauchy F
inf_F : 𝓝 0 ⊓ F = ⊥
i : ↥K →+* L := K.subtype
⊢ Cauchy (map (fun x ↦ x⁻¹) F)

Tactic:
have hi : IsUniformInducing i := isUniformEmbedding_subtype_val.isUniformInducing

Goal state after:
K✝ : Type u_1
inst✝⁴ : Field K✝
inst✝³ : UniformSpace K✝
L : Type u_2
inst✝² : Field L
inst✝¹ : UniformSpace L
inst✝ : CompletableTopField L
K : Subfield L
F : Filter ↥K
F_cau : Cauchy F
inf_F : 𝓝 0 ⊓ F = ⊥
i : ↥K →+* L := K.subtype
hi : IsUniformInducing ⇑i
⊢ Cauchy (map (fun x ↦ x⁻¹) F)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W'.negAddY P Q * (P z * Q z) ^ 3 = (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 3

Tactic:
negAddY_eq',

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ (P y * Q z ^ 3 - Q y * P z ^ 3) * (W'.addX P Q * (P z * Q z) ^ 2 - P x * Q z ^ 2 * addZ P Q ^ 2) +
      P y * Q z ^ 3 * addZ P Q ^ 3 =
    (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 3
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : v ↑r ≠ 0
vr : Γˣ := Units.mk0 (v ↑r) hr₀
hvr_def : vr = Units.mk0 (v ↑r) hr₀
m : ℤ
hm : Units.mk0 (v ↑π.val) ⋯ ^ m = vr
hm' : v ↑π.val ^ m = v ↑r
hm₀ : 0 ≤ m
n : ℕ
hn : m = ↑n
⊢ ∃ n u, ↑r = ↑(π.val ^ n) * ↑↑u

Tactic:
use n

Goal state after:
case h
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : v ↑r ≠ 0
vr : Γˣ := ⋯
hvr_def : vr = Units.mk0 (v ↑r) hr₀
m : ℤ
hm : Units.mk0 (v ↑π.val) ⋯ ^ m = vr
hm' : v ↑π.val ^ m = v ↑r
hm₀ : 0 ≤ m
n : ℕ
hn : m = ↑n
⊢ ∃ u, ↑r = ↑(π.val ^ n) * ↑↑u
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.addXYZ P Q = addU P Q • ![1, 1, 0]

Tactic:
simp [addXYZ, addX_of_X_eq hP hQ hPz hQz hx, addY_of_X_eq hP hQ hPz hQz hx, addZ_of_X_eq hx,
    smul_fin3]

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

Goal state before:
pp: R✝ : Type u_1
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst✝ : Ring R
v : Valuation R Γ₀
a b : (ofClass Valued.v).ValueGroup₀
⊢ (WithZero.map' ↑(valueGroupEquiv v)) a ≤ (WithZero.map' ↑(valueGroupEquiv v)) b ↔ a ≤ b

Tactic:
match a, b with
    | 0, 0 => simp
    | 0, .coe _ => simp
    | .coe _, 0 => simp
    | .coe a, .coe b => simp

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_2
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
g : G
⊢ ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ Nonempty (G ≃*o Multiplicative ℤ)

Tactic:
let e : G ≃o Additive G := OrderIso.refl G

Goal state after:
G : Type u_2
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
⊢ ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ Nonempty (G ≃*o Multiplicative ℤ)
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ φ = (mk fun p ↦ (coeff (p + 1)) φ) * X + C (constantCoeff φ)

Tactic:
ext (_ | n)
  · simp
  · simp only [coeff_succ_mul_X, coeff_mk, map_add, coeff_C, n.succ_ne_zero,
      if_false, add_zero]

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
m : σ →₀ ℕ
⊢ (coeff m) ((map f) ((monomial n) a)) = (coeff m) ((monomial n) (f a))

Tactic:
simp [coeff_monomial, apply_ite f]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : Semiring R
S₁ : Type u_5
S₂ : Type u_6
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : S₁ →+* S₂
p : MvPowerSeries σ R
⊢ (map g) ((map f) p) = (map (g.comp f)) p

Tactic:
by
  ext n
  simp

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

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

Tactic:
ext n
  simp_rw [coeff_rescale]
  rw [mul_pow, mul_comm _ (b ^ n), mul_assoc]

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
r : R
hr : r ≠ 0
hv : v.asIdeal = Ideal.span {r}
⊢ exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors)) = exp (-1)

Tactic:
← hv,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r ≠ 0
hv : v.asIdeal = Ideal.span {r}
⊢ exp (-↑((Associates.mk v.asIdeal).count (Associates.mk v.asIdeal).factors)) = exp (-1)
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case inr
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
x : K
hv : (valuation K v) x ≤ 1
n : R
d : ↥v.asIdeal.primeCompl
hnd : x * (algebraMap R K) n = (algebraMap R K) ↑d
⊢ v.intValuation ↑d ≤ (valuation K v) x * v.intValuation n

Tactic:
← valuation_of_algebraMap (K := K),

Goal state after:
case inr
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
x : K
hv : (valuation K v) x ≤ 1
n : R
d : ↥v.asIdeal.primeCompl
hnd : x * (algebraMap R K) n = (algebraMap R K) ↑d
⊢ (valuation K v) ↑↑d ≤ (valuation K v) x * v.intValuation n
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case inr
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
x : K
hv : (valuation K v) x ≤ 1
n : R
d : ↥v.asIdeal.primeCompl
hnd : x * (algebraMap R K) n = (algebraMap R K) ↑d
⊢ (valuation K v) ↑↑d ≤ (valuation K v) x * v.intValuation n

Tactic:
← valuation_of_algebraMap (K := K),

Goal state after:
case inr
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
x : K
hv : (valuation K v) x ≤ 1
n : R
d : ↥v.asIdeal.primeCompl
hnd : x * (algebraMap R K) n = (algebraMap R K) ↑d
⊢ (valuation K v) ↑↑d ≤ (valuation K v) x * (valuation K v) ↑n
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case left
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
n : ℕ
H : ↑n < weightedOrder w g
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff d) f ≠ 0
hd : (weight w) d = n
⊢ (coeff d) (f + g) ≠ 0

Tactic:
← hd

Goal state after:
case left
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
H : ↑((weight w) d) < weightedOrder w g
hd' : (coeff d) f ≠ 0
hd : (weight w) d = n
⊢ (coeff d) (f + g) ≠ 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
a b : R
hv : v.intValuation b ≤ v.intValuation a
γ : Multiplicative ℤ
ha : ¬a = 0
hvaz : v.intValuation a ≠ 0
hγz : ↑γ ≠ 0
n : ℕ
hna : exp (-↑n) < v.intValuation a
hnγ : exp (-↑n) < ↑γ
hvn : emultiplicity v.asIdeal (Ideal.span {a}) ≤ ↑n
⊢ ∃ a_1, v.intValuation (b - a_1 * a) ≤ exp (-↑n)

Tactic:
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]

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
a b : R
hv : v.intValuation b ≤ v.intValuation a
γ : Multiplicative ℤ
ha : ¬a = 0
hvaz : v.intValuation a ≠ 0
hγz : ↑γ ≠ 0
n : ℕ
hna : exp (-↑n) < v.intValuation a
hnγ : exp (-↑n) < ↑γ
hvn : emultiplicity v.asIdeal (Ideal.span {a}) ≤ ↑n
hb : b ∈ v.asIdeal ^ multiplicity v.asIdeal (Ideal.span {a})
⊢ ∃ a_1, v.intValuation (b - a_1 * a) ≤ exp (-↑n)
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case h
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
x : K
hv : (valuation K v) x ≤ 1
γ : (WithZero (Multiplicative ℤ))ˣ
n d : R
hd✝ : d ∈ v.asIdeal.primeCompl
hd : v.intValuation d = 1
hnd : x * (algebraMap R K) ↑⟨d, hd✝⟩ = (algebraMap R K) n
hd' : v.intValuation n ≤ v.intValuation d
a : R
hval : v.intValuation (n - a * d) < ↑γ
⊢ (valuation K v) ((algebraMap R K) a - x) = v.intValuation (n - a * d)

Tactic:
← valuation_of_algebraMap (K := K),

Goal state after:
case h
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
x : K
hv : (valuation K v) x ≤ 1
γ : (WithZero (Multiplicative ℤ))ˣ
n d : R
hd✝ : d ∈ v.asIdeal.primeCompl
hd : v.intValuation d = 1
hnd : x * (algebraMap R K) ↑⟨d, hd✝⟩ = (algebraMap R K) n
hd' : v.intValuation n ≤ v.intValuation d
a : R
hval : v.intValuation (n - a * d) < ↑γ
⊢ (valuation K v) ((algebraMap R K) a - x) = (valuation K v) ↑(n - a * d)
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
⊢ f ≠ 0 ↔ ∃ n d, (coeff d) f ≠ 0 ∧ degree d = n

Tactic:
by
  simp_rw [degree_eq_weight_one]
  exact ne_zero_iff_exists_coeff_ne_zero_and_weight (fun _ => 1)

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : CommSemiring R
f : MvPowerSeries σ R
hf : constantCoeff f = 0
⊢ Tendsto (fun n ↦ f ^ n) atTop (𝓝 0)

Tactic:
apply isTopologicallyNilpotent_of_constantCoeff_isNilpotent
  rw [hf]
  exact IsNilpotent.zero

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
r : R
x : ↥(adicCompletionIntegers K v)
⊢ { toFun := fun r ↦ ⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) r)) }, ⋯⟩,
          map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
        r *
      x =
    x *
      { toFun := fun r ↦ ⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) r)) }, ⋯⟩,
          map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
        r

Tactic:
by
    rw [mul_comm]

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

Goal state before:
pp: case pos
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
a : adicCompletion K v
ha : a ∈ adicCompletionIntegers K v
⊢ ∃ b ∈ R⁰, a * ↑b ∈ adicCompletionIntegers K v

Tactic:
use 1
    simp [ha]

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
φ : 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
hI : ↑I ∈ 𝓝 0
n✝ : σ → ℕ := fun s ↦ sInf {n | a s ^ n.succ ∈ I}
s : σ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → a s ^ b ∈ ↑I
⊢ {n | a s ^ n.succ ∈ I}.Nonempty

Tactic:
use n

Goal state after:
case h
σ : 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
hI : ↑I ∈ 𝓝 0
n✝ : σ → ℕ := ⋯
s : σ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → a s ^ b ∈ ↑I
⊢ n ∈ {n | a s ^ n.succ ∈ I}
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
ha : HasSubst a
ha' : ∀ (i : σ), constantCoeff (a i) = 0
f : MvPowerSeries σ R
hf : constantCoeff f = 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ ∃ i, d i ≠ 0

Tactic:
by_contra! hc
        exact hd <| Finsupp.ext hc

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

Goal state before:
pp: case a
⊢ ℵ₀ ^ ℵ₀ = 𝔠

Tactic:
aleph0_power_aleph0

Goal state after:
case a
⊢ 𝔠 = 𝔠
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
n : ℕ
⊢ ‖term f s' n‖ ≤ ‖term f s n‖

Tactic:
simp only [norm_term_eq]
  split
  · next => rfl
  · next hn => gcongr; exact Nat.one_le_cast.mpr <| Nat.one_le_iff_ne_zero.mpr hn

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

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
I : Set ι
hI : I.Finite
U : (i : ι) → Set (E i)
hU : ∀ i ∈ I, Balanced 𝕜 (U i)
x : (i : ι) → E i
hI₀ : I = univ ∨ (∃ i ∈ I, x i ≠ 0) ∨ (𝓝[≠] 0).NeBot
r : ℝ≥0∞
hr : ⨆ i ∈ I, egauge 𝕜 (U i) (x i) < r
c : ι → 𝕜
hc : ∀ i ∈ I, x i ∈ c i • U i
hcr : ∀ i ∈ I, ‖c i‖ₑ < r
hr₀ : 0 < r
⊢ ∃ c₀, (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r

Tactic:
rcases I.eq_empty_or_nonempty with rfl | hIne

Goal state after:
case inl
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
U : (i : ι) → Set (E i)
x : (i : ι) → E i
r : ℝ≥0∞
c : ι → 𝕜
hr₀ : 0 < r
hI : ∅.Finite
hU : ∀ i ∈ ∅, Balanced 𝕜 (U i)
hI₀ : ∅ = univ ∨ (∃ i ∈ ∅, x i ≠ 0) ∨ (𝓝[≠] 0).NeBot
hr : ⨆ i ∈ ∅, egauge 𝕜 (U i) (x i) < r
hc : ∀ i ∈ ∅, x i ∈ c i • U i
hcr : ∀ i ∈ ∅, ‖c i‖ₑ < r
⊢ ∃ c₀, (c₀ ≠ 0 ∨ ∅ = univ) ∧ (∀ i ∈ ∅, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r

case inr
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
I : Set ι
hI : I.Finite
U : (i : ι) → Set (E i)
hU : ∀ i ∈ I, Balanced 𝕜 (U i)
x : (i : ι) → E i
hI₀ : I = univ ∨ (∃ i ∈ I, x i ≠ 0) ∨ (𝓝[≠] 0).NeBot
r : ℝ≥0∞
hr : ⨆ i ∈ I, egauge 𝕜 (U i) (x i) < r
c : ι → 𝕜
hc : ∀ i ∈ I, x i ∈ c i • U i
hcr : ∀ i ∈ I, ‖c i‖ₑ < r
hr₀ : 0 < r
hIne : I.Nonempty
⊢ ∃ c₀, (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r
Module: Mathlib.Analysis.Calculus.TangentCone.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : SMul 𝕜 E
inst✝ : TopologicalSpace E
s : Set E
x : E
ι : Sort u_3
p : ι → Prop
U : ι → Set E
h : (𝓝 0).HasBasis p U
y : E
⊢ y ∈ tangentConeAt 𝕜 s x ↔ y ∈ ⋂ i, ⋂ (_ : p i), closure[inst✝] (univ • (U i ∩ (fun x_2 ↦ x + x_2) ⁻¹' s))

Tactic:
simp only [tangentConeAt_def, mem_ofPred_eq, mem_iInter₂, ← map₂_smul, ← map_prod_eq_map₂,
    ((nhdsWithin_hasBasis h _).top_prod.map _).clusterPt_iff_forall_mem_closure, image_prod,
    image2_smul]

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 : 𝕜
h : ¬DifferentiableAt 𝕜 f x
⊢ deriv f x = 0

Tactic:
unfold deriv
  rw [fderiv_zero_of_not_differentiableAt h]
  simp

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

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : DifferentiableWithinAt ℝ f (Ioi x) x
A : HasDerivWithinAt f (derivWithin f (Ioi x) x) (Ici x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x

Tactic:
have B := (differentiableWithinAt_Ioi_iff_Ici.1 H).hasDerivWithinAt

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : DifferentiableWithinAt ℝ f (Ioi x) x
A : HasDerivWithinAt f (derivWithin f (Ioi x) x) (Ici x) x
B : HasDerivWithinAt f (derivWithin f (Ici x) x) (Ici x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x
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
x : E
s : Set E
inst✝² : ContinuousAdd E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : T2Space E
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderiv 𝕜 id x = ContinuousLinearMap.id 𝕜 E

Tactic:
exact fderiv_id

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
l : Filter α
f : α → E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
x : E
h : Tendsto (fun x_1 ↦ f x_1 - x) l (𝓝 0)
U : Set E
hU₀ : U ∈ 𝓝 0
hUb : Balanced 𝕜 U
r : ℝ≥0
hr₀ : 0 < r
hr₁ : r ≤ 1
hr : ↑r ≤ (egauge 𝕜 U x)⁻¹
⊢ ∃ j, 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (id U + id U) (f x) ≤ egauge 𝕜 (ball 0 j) 1

Tactic:
use r, by positivity

Goal state after:
case right
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
l : Filter α
f : α → E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
x : E
h : Tendsto (fun x_1 ↦ f x_1 - x) l (𝓝 0)
U : Set E
hU₀ : U ∈ 𝓝 0
hUb : Balanced 𝕜 U
r : ℝ≥0
hr₀ : 0 < r
hr₁ : r ≤ 1
hr : ↑r ≤ (egauge 𝕜 U x)⁻¹
⊢ ∀ᶠ (x : α) in l, egauge 𝕜 (id U + id U) (f x) ≤ egauge 𝕜 (ball 0 ↑r) 1
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:

Tactic:
egauge 𝕜 (ball 0 r) (f x) ≤ ‖c‖ₑ * ‖f x‖ₑ / r :=
        egauge_ball_le_of_one_lt_norm hc <| .inl hr₀.ne'
      _ ≤ ‖c‖ₑ * (C * ‖g x‖ₑ) / r := by
        gcongr
        simp only [enorm_eq_nnnorm, ← coe_nnnorm] at hx ⊢
        exact mod_cast hx
      _ = ‖g x‖ₑ / (r / (C * ‖c‖₊) : ℝ≥0) := by
        simp_all [pos_iff_ne_zero, ENNReal.div_eq_inv_mul, ENNReal.mul_inv]
        ac_rfl
      _ ≤ _ := div_le_egauge_ball _ _ _

Goal state after:
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: case a
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
C : ℝ
⊢ ∃ i', ⨆ (_ : ∀ (n : ℕ), ‖p (n + 1)‖ * ↑r ^ n ≤ C), ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ i'), ↑r

Tactic:
use ‖p 0‖ ⊔ (C * r)

Goal state after:
case h
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
C : ℝ
⊢ ⨆ (_ : ∀ (n : ℕ), ‖p (n + 1)‖ * ↑r ^ n ≤ C), ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ max ‖p 0‖ (C * ↑r)), ↑r
Module: Mathlib.Analysis.Analytic.OfScalars

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : Ring E
inst✝² : Algebra 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalRing E
c : ℕ → 𝕜
x : E
n : ℕ
⊢ ((ofScalars E c n) fun x_1 ↦ x) = c n • x ^ n

Tactic:
by
  simp [ofScalars]

Goal state after:
Module: Mathlib.Analysis.Analytic.OfScalars

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : Ring E
inst✝² : Algebra 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalRing E
c : ℕ → 𝕜
x : E
⊢ (fun n ↦ (ofScalars E c n) fun x_1 ↦ x) = fun n ↦ c n • x ^ n

Tactic:
by
  simp [ofScalars]

Goal state after:
Module: Mathlib.Analysis.Analytic.OfScalars

Goal state before:
pp: case neg.refine_1.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r)
r' : ℝ≥0
hr' : r' * r < 1
hrz : ¬r' = 0
⊢ ∀ᶠ (n : ℕ) in atTop, ‖‖c n‖ * ↑r' ^ n‖ ≠ 0

pp: case neg.refine_1.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r)
r' : ℝ≥0
hr' : r' * r < 1
hrz : ¬r' = 0
⊢ Tendsto (fun n ↦ ‖‖‖c (n + 1)‖ * ↑r' ^ (n + 1)‖‖ / ‖‖‖c n‖ * ↑r' ^ n‖‖) atTop (𝓝 ↑(r' * r))

Tactic:
· refine (hc.eventually_ne (NNReal.coe_ne_zero.mpr hr)).mp (Eventually.of_forall ?_)
      simp_all

Goal state after:
case neg.refine_1.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r)
r' : ℝ≥0
hr' : r' * r < 1
hrz : ¬r' = 0
⊢ Tendsto (fun n ↦ ‖‖‖c (n + 1)‖ * ↑r' ^ (n + 1)‖‖ / ‖‖‖c n‖ * ↑r' ^ n‖‖) atTop (𝓝 ↑(r' * r))
Module: Mathlib.Analysis.Analytic.OfScalars

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n ↦ ‖c n‖ / ‖c n.succ‖) atTop (𝓝 ↑r)
⊢ (ofScalars E c).radius = ↑r

Tactic:
suffices Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 r⁻¹) by
    convert! ofScalars_radius_eq_inv_of_tendsto E c (inv_ne_zero hr) this
    simp
  convert hc.inv₀ (NNReal.coe_ne_zero.mpr hr)
  simp

Goal state after:
Module: Mathlib.Analysis.Analytic.OfScalars

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
hc : ∀ᶠ (x : ℕ) in atTop, ‖‖ofScalars E c x‖ * ↑r ^ x‖ = 0
n : ℕ
hc' : ‖‖ofScalars E c n‖ * ↑r ^ n‖ = 0
⊢ 0 = ‖c n.succ‖ / ‖c n‖

Tactic:
rw [ofScalars_norm, norm_mul, norm_norm, mul_eq_zero] at hc'

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
hc : ∀ᶠ (x : ℕ) in atTop, ‖‖ofScalars E c x‖ * ↑r ^ x‖ = 0
n : ℕ
hc' : ‖c n‖ = 0 ∨ ‖↑r ^ n‖ = 0
⊢ 0 = ‖c n.succ‖ / ‖c n‖
Module: Mathlib.Analysis.Analytic.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f pf x r
v : Fin 0 → E
⊢ (pf 0) v = f x

Tactic:
by
  rw [← hasFPowerSeriesWithinOnBall_univ] at hf
  exact hf.coeff_zero v

Goal state after: