mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Northcott

Goal state before:
pp: α : Type u_1
β : Type u_2
h : α → β
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
⊢ (∀ (b : β), {a | h a ≤ b}.Finite) ↔ ∀ (b : β), {x | ¬b ≤ h x}.Finite

Tactic:
not_le

Goal state after:
α : Type u_1
β : Type u_2
h : α → β
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
⊢ (∀ (b : β), {a | h a ≤ b}.Finite) ↔ ∀ (b : β), {x | h x < b}.Finite
Module: Mathlib.Order.Northcott

Goal state before:
pp: α : Type u_1
β : Type u_2
h : α → β
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
H : ∀ (b : β), {x | h x < b}.Finite
b : β
⊢ {a | h a ≤ b}.Finite

Tactic:
obtain ⟨b', hc⟩ := exists_gt b

Goal state after:
α : Type u_1
β : Type u_2
h : α → β
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
H : ∀ (b : β), {x | h x < b}.Finite
b b' : β
hc : b < b'
⊢ {a | h a ≤ b}.Finite
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case e'_2.mp
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
h : ∀ m < n, (coeff m) φ = 0
m : Unit →₀ ℕ
hm : m () < n
⊢ (MvPowerSeries.coeff (single default (m default))) φ = 0

Tactic:
convert! h _ hm

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

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : 1 ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors
notMem : ¬2 ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors = 1

Tactic:
not_le

Goal state after:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : 1 ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors
notMem : (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors < 2
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors = 1
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff d) f = 0
this : ↑(weightedOrder w f).toNat = weightedOrder w f
d : σ →₀ ℕ
H : (weight w) d < n
hfd : (coeff d) f ≠ 0
hd : ↑((weight w) d) = weightedOrder w f
⊢ False

Tactic:
exact hfd (h d H)

Goal state after:
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) γ)}
⊢ x ∈ {x | (valuation K v).restrict x < ↑γ}

Tactic:
Set.mem_ofPred_eq,

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) γ)}
⊢ (valuation K v).restrict x < ↑γ
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
⊢ DenseRange ⇑(algebraMap K (adicCompletion K v))

Tactic:
algebraMap_adicCompletion

Goal state after:
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
⊢ DenseRange ((fun x ↦ { toCompletion := ↑((WithVal.equiv (valuation K v)).symm x) }) ∘ ⇑(algebraMap K K))
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
f : MvPowerSeries σ R
⊢ HasSum (fun d ↦ (monomial d) ((coeff d) f)) f

Tactic:
Pi.hasSum

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
f : MvPowerSeries σ R
⊢ ∀ (x : σ →₀ ℕ), HasSum (fun i ↦ (monomial i) ((coeff i) f) x) (f x)
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)
⊢ (algebraMap R (adicCompletion K v)) r ∈ adicCompletionIntegers K v

Tactic:
algebraMap_adicCompletion

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
r : R
x : ↥(adicCompletionIntegers K v)
⊢ ((fun x ↦ { toCompletion := ↑((WithVal.equiv (valuation K v)).symm x) }) ∘ ⇑(algebraMap R K)) r ∈
    adicCompletionIntegers K v
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
a : (σ →₀ ℕ) → R
h : ∀ (d : σ →₀ ℕ), HasSum (fun i ↦ (coeff d) (f i)) (a d)
⊢ ∃ a, ∀ (d : σ →₀ ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) a)

Tactic:
exact ⟨a, by simpa using! h⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
hf : φ ≠ 0
⊢ ↑φ.order.toNat = φ.order

Tactic:
by
  rw [ENat.natCast_toNat_eq_self.mpr (order_eq_top.not.mpr hf)]

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
a : (adicCompletion K v)ˣ
⊢ a ∈ (adicCompletionIntegers K v).units ↔ Valued.v ↑a = 1

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦
     ⟨h.le, by simp [mem_adicCompletionIntegers, inv_le_one_iff₀, h.symm.le]⟩⟩
  convert! isUnit_iff_valued_eq_one.1 (Submonoid.unitsEquivIsUnitSubmonoid _ ⟨_, h⟩).2

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : constantCoeff φ = 0
⊢ 1 ≤ φ.order

Tactic:
refine le_order _ _ fun d hd ↦ ?_

Goal state after:
case mpr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : constantCoeff φ = 0
d : ℕ
hd : ↑d < 1
⊢ (coeff d) φ = 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
⊢ (coeff (φ.order.toNat + ψ.order.toNat)) (φ * ψ) ≠ 0

Tactic:
rw [coeff_mul, Finset.sum_eq_single_of_mem ⟨φ.order.toNat, ψ.order.toNat⟩ (by simp)]

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
⊢ (coeff (φ.order.toNat, ψ.order.toNat).1) φ * (coeff (φ.order.toNat, ψ.order.toNat).2) ψ ≠ 0

case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
⊢ ∀ b ∈ antidiagonal (φ.order.toNat + ψ.order.toNat),
    b ≠ (φ.order.toNat, ψ.order.toNat) → (coeff b.1) φ * (coeff b.2) ψ = 0
Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology

Goal state before:
pp: case mp.right
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff e) a ∈ J) → ∀ e_1 ≤ e, (coeff e_1) a ∈ K
h' : ¬e ≤ d
⊢ K = ⊤

Tactic:
eq_top_iff

Goal state after:
case mp.right
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff e) a ∈ J) → ∀ e_1 ≤ e, (coeff e_1) a ∈ K
h' : ¬e ≤ d
⊢ ⊤ ≤ K
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
s : σ
⊢ eval₂ φ a (X s) = a s

Tactic:
rw [← coe_X, eval₂_coe, MvPolynomial.eval₂_X]

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
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : IsUniformAddGroup T
inst✝⁵ : IsTopologicalRing T
inst✝⁴ : IsLinearTopology T T
inst✝³ : T2Space T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous[inst✝¹⁸.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑ε
⊢ eval₂ ((↑ε).comp (algebraMap R S)) (⇑↑ε ∘ a) = eval₂ (algebraMap R T) fun s ↦ ε.toRingHom (a s)

Tactic:
congr!

Goal state after:
case e'_8
σ : 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
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : IsUniformAddGroup T
inst✝⁵ : IsTopologicalRing T
inst✝⁴ : IsLinearTopology T T
inst✝³ : T2Space T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous[inst✝¹⁸.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑ε
⊢ (↑ε).comp (algebraMap R S) = algebraMap R T
Module: Mathlib.SetTheory.Cardinal.Continuum

Goal state before:
pp: x : Cardinal.{u_1}
h₁ : 2 ≤ x
h₂ : x ≤ 𝔠
⊢ x ^ ℵ₀ = 𝔠

Tactic:
apply le_antisymm

Goal state after:
case a
x : Cardinal.{u_1}
h₁ : 2 ≤ x
h₂ : x ≤ 𝔠
⊢ x ^ ℵ₀ ≤ 𝔠

case a
x : Cardinal.{u_1}
h₁ : 2 ≤ x
h₂ : x ≤ 𝔠
⊢ 𝔠 ≤ x ^ ℵ₀
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: ⊢ #ℝ = 𝔠

Tactic:
apply le_antisymm

Goal state after:
case a
⊢ #ℝ ≤ 𝔠

case a
⊢ 𝔠 ≤ #ℝ
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
hq : 1 < q
k : ℕ
hs :
  Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k) ⊆
    (q ^ k).divisorsAntidiagonal
i j : ℕ
hab : i + j = k ∧ q ^ k ≠ 0
h :
  ¬∃ a ∈ Finset.antidiagonal k,
      ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ }) a = (q ^ i, q ^ j)
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (q ^ i, q ^ j).1 *
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (q ^ i, q ^ j).2 =
    0

Tactic:
not_exists,

Goal state after:
case pos
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
hq : 1 < q
k : ℕ
hs :
  Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k) ⊆
    (q ^ k).divisorsAntidiagonal
i j : ℕ
hab : i + j = k ∧ q ^ k ≠ 0
h :
  ∀ (x : ℕ × ℕ),
    ¬(x ∈ Finset.antidiagonal k ∧
        ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ }) x = (q ^ i, q ^ j))
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (q ^ i, q ^ j).1 *
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (q ^ i, q ^ j).2 =
    0
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: x y : ℝ
h : x < y
⊢ ¬𝔠 ≤ ℵ₀

Tactic:
not_le

Goal state after:
x y : ℝ
h : x < y
⊢ ℵ₀ < 𝔠
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: case pos
σ : 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
f : MvPowerSeries σ R
hf : IsNilpotent (constantCoeff f)
d : σ →₀ ℕ
hd : d = 0
⊢ IsNilpotent ((coeff d) f • constantCoeff (d.prod fun s e ↦ a s ^ e))

pp: case neg
σ : 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
f : MvPowerSeries σ R
hf : IsNilpotent (constantCoeff f)
d : σ →₀ ℕ
hd : ¬d = 0
⊢ IsNilpotent ((coeff d) f • constantCoeff (d.prod fun s e ↦ a s ^ e))

Tactic:
· rw [← algebraMap_smul S, smul_eq_mul, mul_comm, ← smul_eq_mul, hd]
    apply IsNilpotent.smul
    simpa using IsNilpotent.map hf (algebraMap R S)

Goal state after:
case neg
σ : 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
f : MvPowerSeries σ R
hf : IsNilpotent (constantCoeff f)
d : σ →₀ ℕ
hd : ¬d = 0
⊢ IsNilpotent ((coeff d) f • constantCoeff (d.prod fun s e ↦ a s ^ e))
Module: Mathlib.LinearAlgebra.Complex.FiniteDimensional

Goal state before:
pp: ⊢ Cardinal.lift.{0, 0} #ℚ < Cardinal.lift.{0, 0} #ℂ

Tactic:
simpa using aleph0_lt_continuum

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case inl
s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
⊢ term f s 0 = f 0 / ↑0 ^ s

pp: case inr
s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
n : ℕ
hn : n ≠ 0
⊢ term f s n = f n / ↑n ^ s

Tactic:
· rw [term_zero, Nat.cast_zero, zero_cpow hs, div_zero]

Goal state after:
case inr
s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
n : ℕ
hn : n ≠ 0
⊢ term f s n = f n / ↑n ^ s
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_9
inst✝ : CommSemiring R
n : ℕ
r : R
f : MvPowerSeries σ R
hf : ∀ d ∈ Function.support f, Finsupp.degree d = n
e : σ →₀ ℕ
he : e ∉ Function.support f
⊢ (r ^ ∑ i ∈ e.support, e i) * (coeff e) f = r ^ n * (coeff e) f

Tactic:
simp only [Function.mem_support, ne_eq, not_not] at he
    simp [he, mul_zero, coeff_apply]

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

Goal state before:
pp: case pos.refine_1
ι : 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 ι), (∏ b ∈ x, f b) 1 = 1
⊢ (eulerProduct f) 1 = 1

Tactic:
specialize key 1
      simp_rw [h] at key
      rwa [eventually_const, eq_comm] at key

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

Goal state before:
pp: case refine_1
R : Type u
E : Type v
inst✝² : AddCommGroup E
inst✝¹ : SMul R E
inst✝ : TopologicalSpace E
s : Set E
x y : E
α : Type u_1
l : Filter α
c : α → R
d : α → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∃ᶠ (n : α) in l, x + d n ∈ s
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
⊢ Tendsto d (l ⊓ 𝓟 {y | x + d y ∈ s}) (𝓝 0)

pp: case refine_2
R : Type u
E : Type v
inst✝² : AddCommGroup E
inst✝¹ : SMul R E
inst✝ : TopologicalSpace E
s : Set E
x y : E
α : Type u_1
l : Filter α
c : α → R
d : α → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∃ᶠ (n : α) in l, x + d n ∈ s
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
⊢ ∀ᶠ (n : α) in l ⊓ 𝓟 {y | x + d y ∈ s}, d n ∈ (fun x_1 ↦ x + x_1) ⁻¹' s

Tactic:
· exact hd₀.mono_left inf_le_left

Goal state after:
case refine_2
R : Type u
E : Type v
inst✝² : AddCommGroup E
inst✝¹ : SMul R E
inst✝ : TopologicalSpace E
s : Set E
x y : E
α : Type u_1
l : Filter α
c : α → R
d : α → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∃ᶠ (n : α) in l, x + d n ∈ s
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
⊢ ∀ᶠ (n : α) in l ⊓ 𝓟 {y | x + d y ∈ s}, d n ∈ (fun x_1 ↦ x + x_1) ⁻¹' s
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)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
⊢ (∑ᶠ (i : ℕ), (coeff i) P * (coeff (n + 1 + 1)) (B ^ i) - if 1 = 1 then (coeff 1) P * k else 0) = 0

Tactic:
simp only [↓reduceIte, ← hk, mul_invOf_cancel_left', sub_eq_zero]
            rw [coeff_subst']
            · rfl
            · simp [HasSubst, ← PowerSeries.constantCoeff.eq_def, hB']

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Semiring 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : ContinuousAdd E
s : Set E
x : E
inst✝¹ : T2Space E
inst✝ : Nontrivial E
h : UniqueDiffWithinAt 𝕜 s x
⊢ AccPt x (𝓟 s)

Tactic:
by_contra! h'
  have : Dense (Submodule.span 𝕜 (0 : Set E) : Set E) :=
    h.1.mono <| by gcongr; exact tangentConeAt_subset_zero h'
  simp [dense_iff_closure_eq] at 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
⊢ f =o[𝕜; l] k

Tactic:
refine ⟨fun U hU₀ ↦ ?_⟩
  obtain ⟨V, hV₀, hV⟩ := hfg.1 U hU₀
  obtain ⟨W, hW₀, hW⟩ := hgk.1 V hV₀
  refine ⟨W, hW₀, fun ε hε ↦ ?_⟩
  filter_upwards [hV ε hε, hW] with x hx₁ hx₂ using hx₁.trans <| by gcongr

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₁ : 𝕜 → F
x : 𝕜
s : Set 𝕜
hs : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ derivWithin f₁ s x = derivWithin f s x

Tactic:
unfold derivWithin
  rw [hs.fderivWithin_eq hx]

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

Goal state before:
pp: case refine_2
α : 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 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : δ ≠ 0
⊢ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 ε) (f x) ≤ ↑δ * egauge 𝕜 (ball 0 1) (g x)

Tactic:
filter_upwards [@h ↑(ε * δ / ‖c‖₊) (by positivity)] with x (hx : ‖f x‖₊ ≤ ε * δ / ‖c‖₊ * ‖g x‖₊)

Goal state after:
α : 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 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : δ ≠ 0
x : α
hx : ↑‖f x‖₊ ≤ ε * ↑δ / ↑‖c‖₊ * ↑‖g x‖₊
⊢ egauge 𝕜 (ball 0 ε) (f x) ≤ ↑δ * egauge 𝕜 (ball 0 1) (g x)
Module: Mathlib.Analysis.Analytic.ChangeOrigin

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
p : FormalMultilinearSeries 𝕜 E F
k l : ℕ
⊢ ∑ a, ‖p.changeOriginSeriesTerm k l ↑a ⋯‖₊ = ∑' (x : { s // s.card = l }), ‖p (k + l)‖₊

Tactic:
simp_rw [tsum_fintype, nnnorm_changeOriginSeriesTerm (p := p) (k := k) (l := l)]

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

Goal state before:
pp: 𝕜 : 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
h₀ : r ≠ 0
a : ℝ
ha : a ∈ Ioo (-1) 1
hp : (fun n ↦ ‖p n‖ * ↑r ^ n) =O[atTop] fun x ↦ a ^ x
⊢ ↑r < p.radius

Tactic:
have := ((TFAE_exists_lt_isLittleO_pow (fun n => ‖p n‖ * (r : ℝ) ^ n) 1).out 2 5)

Goal state after:
𝕜 : 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
h₀ : r ≠ 0
a : ℝ
ha : a ∈ Ioo (-1) 1
hp : (fun n ↦ ‖p n‖ * ↑r ^ n) =O[atTop] fun x ↦ a ^ x
this :
  (∃ a ∈ Ioo (-1) 1, (fun n ↦ ‖p n‖ * ↑r ^ n) =O[atTop] fun x ↦ a ^ x) ↔
    ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n
⊢ ↑r < p.radius
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
h_zero : 0 < ‖u‖₊
r : ℝ≥0
hr : ↑r < p.radius
C : ℝ
hC_pos : C > 0
hC : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
n : ℕ
⊢ ‖p n‖ * ‖u‖ ^ n * ↑(r / ‖u‖₊) ^ n = ‖p n‖ * ↑r ^ n

Tactic:
simp only [NNReal.coe_div, coe_nnnorm, div_pow, mul_assoc]
      rw [mul_div_cancel₀]
      rw [← NNReal.coe_pos] at h_zero
      positivity

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

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
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h : y ∈ Metric.eball x r
⊢ AnalyticAt 𝕜 f y

Tactic:
by
  rw [← hasFPowerSeriesWithinOnBall_univ] at hf
  rw [← analyticWithinAt_univ]
  exact hf.analyticWithinAt_of_mem (by simpa using h)

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

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
x y✝ : E × F
x✝ : y✝ ∈ Metric.eball 0 ∞
⊢ HasSum (fun n ↦ (f.fpowerSeriesBilinear x (n + 3)) fun x ↦ y✝)
    ((f (x + y✝).1) (x + y✝).2 - ∑ i ∈ Finset.range 3, (f.fpowerSeriesBilinear x i) fun x ↦ y✝)

Tactic:
by
        simp only [Finset.sum_range_succ, Prod.fst_add, Prod.snd_add, f.map_add_add]
        simp [fpowerSeriesBilinear, hasSum_zero]

Goal state after:
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
s : Set E
hf : AnalyticOnNhd 𝕜 f s
y x : E
hx : x + -y ∈ s
⊢ x - y ∈ s

Tactic:
convert hx; abel

Goal state after:
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
s : Set E
hf : AnalyticOn 𝕜 f s
y x : E
hx : x + -y ∈ s
⊢ x - y ∈ s

Tactic:
convert hx; abel

Goal state after: