mathlib-initiative/mathlib-tactics huggingface dataset:
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
l : S
⊢ UniformContinuous fun x ↦ WithVal.toVal (valuation K v) ((algebraMap S K) l * x.ofVal)

Tactic:
exact (Ring.uniformContinuousConstSMul (WithVal <| v.valuation K)).uniformContinuous_const_smul _

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
d : σ →₀ ℕ
i : σ
hi : d = Finsupp.single i 1
⊢ ∀ᶠ (x' : σ) in cofinite, (if d = Finsupp.single x' 1 then 1 else 0) = 0

Tactic:
filter_upwards [eventually_cofinite_ne i] with j hj

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
d : σ →₀ ℕ
i : σ
hi : d = Finsupp.single i 1
j : σ
hj : j ≠ i
⊢ (if d = Finsupp.single j 1 then 1 else 0) = 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case neg
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:
rw [notMem_adicCompletionIntegers] at ha

Goal state after:
case neg
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 : 1 < Valued.v a
⊢ ∃ b ∈ R⁰, a * ↑b ∈ adicCompletionIntegers K v
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
m : ℕ
⊢ ((trunc (n + 1)) (C a)).coeff m = (Polynomial.C a).coeff m

Tactic:
coeff_trunc,

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
m : ℕ
⊢ (if m < n + 1 then (coeff m) (C a) else 0) = (Polynomial.C a).coeff m
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case left
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
i : ℕ
H : ↑i < ψ.order
hi : ↑i = φ.order
⊢ (coeff i) (φ + ψ) ≠ 0

Tactic:
rw [(coeff _).map_add, coeff_of_lt_order i H, add_zero]

Goal state after:
case left
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
i : ℕ
H : ↑i < ψ.order
hi : ↑i = φ.order
⊢ (coeff i) φ ≠ 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case right
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
⊢ ∀ (i : ℕ), ↑i < φ.order → (coeff i) (φ + ψ) = 0

Tactic:
· intro i hi
    rw [(coeff _).map_add, coeff_of_lt_order i hi, coeff_of_lt_order i (lt_trans hi H),
      zero_add]

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

Goal state before:
pp: case succ.e_a.e_6
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
n : ℕ
this : ((trunc (n + 1)) f).natDegree < n + 1
x✝ : ℕ
h : x✝ < n + 1
⊢ ((trunc (n + 1)) f).coeff x✝ = (coeff x✝) f

Tactic:
coeff_trunc,

Goal state after:
case succ.e_a.e_6
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
n : ℕ
this : ((trunc (n + 1)) f).natDegree < n + 1
x✝ : ℕ
h : x✝ < n + 1
⊢ (if x✝ < n + 1 then (coeff x✝) f else 0) = (coeff x✝) f
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n d : ℕ
⊢ ((trunc (n + 2)) X).coeff d = Polynomial.X.coeff d

Tactic:
coeff_trunc,

Goal state after:
R : Type u_1
inst✝ : Semiring R
n d : ℕ
⊢ (if d < n + 2 then (coeff d) X else 0) = Polynomial.X.coeff d
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
⊢ (trunc 1) p = Polynomial.C ((coeff 0) p)

Tactic:
ext i; simp +contextual [coeff_trunc, Polynomial.coeff_C]

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

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

Tactic:
coeff_trunc,

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : n ≤ m
d : ℕ
⊢ (if d < n then (coeff d) ↑((trunc m) f) else 0) = ((trunc n) f).coeff d
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : n ≤ m
d : ℕ
⊢ (if d < n then (coeff d) ↑((trunc m) f) else 0) = ((trunc n) f).coeff d

Tactic:
coeff_trunc,

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : n ≤ m
d : ℕ
⊢ (if d < n then (coeff d) ↑((trunc m) f) else 0) = if d < n then (coeff d) f else 0
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: case pos
R : Type u_2
inst✝ : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : n ≤ m
d : ℕ
h : d < n
⊢ ((trunc m) f).coeff d = (coeff d) f

Tactic:
coeff_trunc,

Goal state after:
case pos
R : Type u_2
inst✝ : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : n ≤ m
d : ℕ
h : d < n
⊢ (if d < m then (coeff d) f else 0) = (coeff d) f
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:
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) = ((trunc n) (f * g)).coeff m
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
x✝ : ℕ × ℕ
hab : x✝ ∈ antidiagonal m
ha : x✝.1 < n
⊢ ((trunc n) f).coeff x✝.1 * (coeff x✝.2) g = (coeff x✝.1) f * (coeff x✝.2) g

Tactic:
coeff_trunc,

Goal state after:
case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
x✝ : ℕ × ℕ
hab : x✝ ∈ antidiagonal m
ha : x✝.1 < n
⊢ (if x✝.1 < n then (coeff x✝.1) f else 0) * (coeff x✝.2) g = (coeff x✝.1) f * (coeff x✝.2) g
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
h : n < f.order.toNat
⊢ 0 = (coeff n) f

Tactic:
coeff_of_lt_order_toNat _ h

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
h : n < f.order.toNat
⊢ 0 = 0
Module: Mathlib.RingTheory.PowerSeries.Trunc

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

Tactic:
coeff_trunc,

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
n m : ℕ
f : R⟦X⟧
h : n < m
⊢ (if n < m then (coeff n) f else 0) = (coeff n) f
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ order 1 = 0

Tactic:
simpa using order_monomial_of_ne_zero 0 (1 : R) one_ne_zero

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
⊢ ContinuousAt (⇑(eval₂Hom φ a)) 0

Tactic:
rw [ContinuousAt, map_zero, IsLinearTopology.hasBasis_ideal.tendsto_right_iff]

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.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}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
this : ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, φ (MvPolynomial.coeff i x) ∈ I
p : MvPolynomial σ R
hp : ∀ i ∈ D, φ (MvPolynomial.coeff i p) ∈ I
⊢ (eval₂Hom φ a) p ∈ ↑I

Tactic:
rw [coe_eval₂Hom, SetLike.mem_coe, eval₂_eq]

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
hI : ↑I ∈ 𝓝 0
n : σ → ℕ := fun s ↦ sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
this : ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, φ (MvPolynomial.coeff i x) ∈ I
p : MvPolynomial σ R
hp : ∀ i ∈ D, φ (MvPolynomial.coeff i p) ∈ I
⊢ ∑ d ∈ p.support, φ (MvPolynomial.coeff d p) * ∏ i ∈ d.support, a i ^ d i ∈ I
Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology

Goal state before:
pp: case refine_1
σ : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
D : Set (σ →₀ ℕ)
I : TwoSidedIdeal R
hD : (D, I).1.Finite
hI : ↑(D, I).2 ∈ 𝓝 0
f : (σ →₀ ℕ) → R
hf : ∀ e ≤ (I, hD.toFinset.sup id).2, (coeff e) f ∈ (I, hD.toFinset.sup id).1
d : σ →₀ ℕ
hd : d ∈ (D, I).1
⊢ f d ∈ (fun x ↦ ↑(D, I).2) d

Tactic:
convert! hf _ <| Finset.le_sup (hD.mem_toFinset.mpr hd)

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Continuum

Goal state before:
pp: ⊢ 2 ^ (ℵ₀ * ℵ₀) = 2 ^ ℵ₀

Tactic:
mul_eq_left le_rfl le_rfl aleph0_ne_zero

Goal state after:
⊢ 2 ^ ℵ₀ = 2 ^ ℵ₀
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
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
ha : HasSubst a
⊢ ⇑(substAlgHom ha) = ⇑(aeval ⋯)

Tactic:
by
  simp only [substAlgHom, coe_aeval ha.hasEval]
  convert! coe_aeval (R := R) (hasSubst_iff_hasEval_of_discreteTopology.mp ha) <;>
  exact DiscreteUniformity.eq_bot.symm

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

Goal state before:
pp: ⊢ #ℝ = 𝔠

Tactic:
by
  apply le_antisymm
  · rw [Real.equivCauchy.cardinal_eq]
    apply mk_quotient_le.trans
    apply (mk_subtype_le _).trans_eq
    rw [← power_def, mk_nat, mkRat, aleph0_power_aleph0]
  · convert! mk_le_of_injective (cantorFunction_injective _ _)
    · rw [← power_def, mk_bool, mk_nat, two_power_aleph0]
    · exact 1 / 3
    · simp
    · norm_num

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

Goal state before:
pp: a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ #↑(Iio a ∪ {a} ∪ Ioi a) < 𝔠

Tactic:
mk_union_le,

Goal state after:
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ #↑(Iio a ∪ {a}) + #↑(Ioi a) < 𝔠
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ∃ a, q ^ a = n
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) (f * g)) 0 n =
    ∑ x ∈ n.divisorsAntidiagonal,
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 x.1 *
        Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 x.2

Tactic:
obtain ⟨k, rfl⟩ := hn
        rw [(Nat.pow_right_injective hq).extend_apply]
        have hs : (Finset.antidiagonal k).map (.prodMap ⟨fun k ↦ q ^ k, Nat.pow_right_injective hq⟩
            ⟨fun k ↦ q ^ k, Nat.pow_right_injective hq⟩) ⊆ (q ^ k).divisorsAntidiagonal :=
          Nat.antidiagonal_map_subset_divisorsAntidiagonal_pow hq k
        rw [PowerSeries.coeff_mul k f g, ← Finset.sum_subset hs]
        · simp [(Nat.pow_right_injective hq).extend_apply]
        · intro (a, b) hab h
          by_cases ha : ∃ i, q ^ i = a
          · by_cases hb : ∃ j, q ^ j = b
            · obtain ⟨i, rfl⟩ := ha
              obtain ⟨j, rfl⟩ := hb
              rw [Nat.mem_divisorsAntidiagonal, ← pow_add, Nat.pow_right_inj hq] at hab
              simp_rw [Finset.mem_map, not_exists, not_and, Finset.mem_antidiagonal] at h
              simpa using h (i, j) hab.1
            · rwa [mul_comm, Function.extend_apply', Pi.zero_apply, zero_mul]
          · rwa [Function.extend_apply', Pi.zero_apply, zero_mul]

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
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
U : Set E
V : Set F
hU : Balanced 𝕜 U
hV : Balanced 𝕜 V
a : E
b : F
r : ℝ≥0∞
x : 𝕜
hx : a ∈ x • U
hxr : ‖x‖ₑ < r
y : 𝕜
hy : b ∈ y • V
hyr : ‖y‖ₑ < r
hle : ‖y‖ ≤ ‖x‖
⊢ ∃ c, (a, b) ∈ (c • U) ×ˢ (c • V) ∧ ‖c‖ₑ < r

Tactic:
| inr hle =>

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

Goal state before:
pp: case pos.refine_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (i : ι), (f i).IsMultiplicative
hf' : Multipliable f
h✝ : ∀ (s : Finset ι), (∏ b ∈ s, f b).IsMultiplicative
key : ∀ (n : ℕ), ∀ᶠ (i : Finset ι) in (SummationFilter.unconditional ι).filter, (∏ b ∈ i, f b) n = (∏' (b : ι), f b) n
h : ∀ (x : Finset ι) {m n : ℕ}, m.Coprime n → (∏ b ∈ x, f b) (m * n) = (∏ b ∈ x, f b) m * (∏ b ∈ x, f b) n
m n : ℕ
hmn : m.Coprime n
⊢ (eulerProduct f) (m * n) = (eulerProduct f) m * (eulerProduct f) n

Tactic:
replace h s : (∏ b ∈ s, f b) (m * n) = (∏ b ∈ s, f b) m * (∏ b ∈ s, f b) n := h s hmn
      have h2 := key (m * n)
      simp_rw [h] at h2
      exact eventually_const.mp (EventuallyEq.trans (.symm h2) (.mul (key m) (key n)))

Goal state after:
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 t : Set E
x : E
h : s ⊆ t
⊢ ∀ (a : E), ClusterPt a (⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0) → ClusterPt a (⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' t] 0)

Tactic:
refine fun y hy ↦ hy.mono ?_

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : SMul 𝕜 E
inst✝ : TopologicalSpace E
s t : Set E
x : E
h : s ⊆ t
y : E
hy : ClusterPt y (⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0)
⊢ ⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0 ≤ ⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' t] 0
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
𝕜' : Type u_3
inst✝³ : Monoid 𝕜'
inst✝² : SMul 𝕜 𝕜'
inst✝¹ : MulAction 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
⊢ ∀ (a : E), ClusterPt a (⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0) → ClusterPt a (⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0)

Tactic:
refine fun y hy ↦ hy.mono ?_

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : SMul 𝕜 E
inst✝⁴ : TopologicalSpace E
s : Set E
x : E
𝕜' : Type u_3
inst✝³ : Monoid 𝕜'
inst✝² : SMul 𝕜 𝕜'
inst✝¹ : MulAction 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
y : E
hy : ClusterPt y (⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0)
⊢ ⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0 ≤ ⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0
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 t : Set E
x : E
inst✝ : ContinuousAdd E
h : 𝓝[s] x ≤ 𝓝[t] x
⊢ ∀ (a : E), ClusterPt a (⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0) → ClusterPt a (⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' t] 0)

Tactic:
refine fun y hy ↦ hy.mono ?_

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : SMul 𝕜 E
inst✝¹ : TopologicalSpace E
s t : Set E
x : E
inst✝ : ContinuousAdd E
h : 𝓝[s] x ≤ 𝓝[t] x
y : E
hy : ClusterPt y (⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0)
⊢ ⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0 ≤ ⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' t] 0
Module: Mathlib.Analysis.Calculus.FDeriv.Congr

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s t : Set E
h : s =ᶠ[𝓝[≠] x] t
⊢ 𝓝[s \ {x}] x = 𝓝[t \ {x}] x

Tactic:
simpa only [set_eventuallyEq_iff_inf_principal, ← nhdsWithin_inter', sdiff_eq, inter_comm]
        using h

Goal state after:
Module: Mathlib.Analysis.Calculus.TangentCone.Real

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul ℝ E
s : Set E
x : E
inst✝ : IsTopologicalAddGroup E
conv : Convex ℝ s
hx : x ∈ closure[inst✝²] s
y : E
hy : y ∈ interior s
this : y - x ∈ interior (tangentConeAt ℝ s x)
⊢ (interior ↑(Submodule.span ℝ (tangentConeAt ℝ s x))).Nonempty

Tactic:
exact ⟨y - x, interior_mono Submodule.subset_span this⟩

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 : (fun x ↦ egauge 𝕜 V (g x)) ≤ᶠ[l] fun x ↦ egauge 𝕜 W (k x)
x : α
⊢ egauge 𝕜 U (f x) ≤ egauge 𝕜 V (g x) → egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x) → egauge 𝕜 U (f x) ≤ egauge 𝕜 W (k x)

Tactic:
hx₁

Goal state after:
α : 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 : (fun x ↦ egauge 𝕜 V (g x)) ≤ᶠ[l] fun x ↦ egauge 𝕜 W (k x)
x : α
hx₁ : egauge 𝕜 U (f x) ≤ egauge 𝕜 V (g x)
⊢ egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x) → egauge 𝕜 U (f x) ≤ egauge 𝕜 W (k x)
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 : ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 V (g x)
W : Set G
hW₀ : W ∈ 𝓝 0
hW : (fun x ↦ egauge 𝕜 V (g x)) ≤ᶠ[l] fun x ↦ egauge 𝕜 W (k x)
ε : ℝ≥0
hε : ε ≠ 0
x : α
⊢ egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 V (g x) →
    egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x) → egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 W (k x)

Tactic:
hx₁

Goal state after:
α : 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 : ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 V (g x)
W : Set G
hW₀ : W ∈ 𝓝 0
hW : (fun x ↦ egauge 𝕜 V (g x)) ≤ᶠ[l] fun x ↦ egauge 𝕜 W (k x)
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx₁ : egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 V (g x)
⊢ egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x) → egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 W (k x)
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
x : α
⊢ egauge 𝕜 U (f x) ≤ egauge 𝕜 V (g x) →
    egauge 𝕜 V (g x) ≤ ↑ε * egauge 𝕜 W (k x) → egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 W (k x)

Tactic:
hx₁

Goal state after:
α : 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
x : α
hx₁ : egauge 𝕜 U (f x) ≤ egauge 𝕜 V (g x)
⊢ egauge 𝕜 V (g x) ≤ ↑ε * egauge 𝕜 W (k x) → egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 W (k 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
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
inst✝³ : ContinuousAdd E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousSMul 𝕜 F
L : Filter E
hL : L ≤ 𝓝 x
h : HasFDerivAtFilter f f' (L ×ˢ pure x)
⊢ Tendsto f L (𝓝 (f x))

Tactic:
by
  have : (f · - f x) =o[𝕜; L] (1 : E → 𝕜) := by
    refine h.isBigOTVS_sub |>.comp_tendsto prod_pure.ge |>.trans_isLittleOTVS ?_
    rw [isLittleOTVS_one]
    simpa [sub_eq_add_neg] using! (tendsto_id'.mpr hL).add_const (-x)
  rw [isLittleOTVS_one] at this
  simpa using! this.add_const (f x)

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✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ j, 0 < j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ : ∀ (ε_1 : ℝ≥0), ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 ↑ε) (f x) ≤ ↑ε_1 * egauge 𝕜 (ball 0 ↑δ) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 ↑ε) (f x) ≤ ↑(δ / ‖c‖₊) * egauge 𝕜 (ball 0 ↑δ) (g x)
⊢ ↑(δ / ‖c‖₊) * egauge 𝕜 (ball 0 ↑δ) (g x) ≤ ↑δ / ↑‖c‖₊ * (↑‖c‖₊ * ↑‖g x‖₊ / ↑δ)

Tactic:
by
        gcongr
        exacts [ENNReal.coe_div_le, egauge_ball_le_of_one_lt_norm hc (.inl <| ne_of_gt hδ₀)]

Goal state after: