mathlib-initiative/mathlib-tactics huggingface dataset:
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) γ)}
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x✝¹ : ∃ γ, {x | extensionValuation.restrict x < ↑γ} ⊆ s
γ : (ofClass extensionValuation).ValueGroup₀ˣ
h : {x | extensionValuation.restrict x < ↑γ} ⊆ s
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ embedding (extension x✝) < embedding ↑((Units.map valueGroup₀_equiv_extensionValuation.symm.toMonoidHom) γ) ↔
    extensionValuation.restrict x✝ < ↑γ

Tactic:
← this

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) γ)}
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x✝¹ : ∃ γ, {x | extensionValuation.restrict x < ↑γ} ⊆ s
γ : (ofClass extensionValuation).ValueGroup₀ˣ
h : {x | extensionValuation.restrict x < ↑γ} ⊆ s
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ extensionValuation.restrict x✝ <
      ↑((Units.map valueGroup₀_equiv_extensionValuation.toMonoidHom)
          ((Units.map valueGroup₀_equiv_extensionValuation.symm.toMonoidHom) γ)) ↔
    extensionValuation.restrict x✝ < ↑γ
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type u_4
inst✝¹ : Semiring B
inst✝ : Algebra R B
a : R
φ : MvPowerSeries σ A
n : σ →₀ ℕ
⊢ (coeff n) (((map (algebraMap R A)).comp C) a * φ) = (coeff n) (φ * ((map (algebraMap R A)).comp C) a)

Tactic:
simp [Algebra.commutes]

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 Γ₀
⊢ Function.Surjective ⇑v ↔ Function.Surjective ⇑v

Tactic:
constructor <;> intro h γ <;> obtain ⟨a, ha⟩ := h γ

Goal state after:
case mp
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
a : hat K
ha : v a = γ
⊢ ∃ a, v a = γ

case mpr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
a : K
ha : v a = γ
⊢ ∃ a, v a = γ
Module: Mathlib.Data.Finsupp.Interval

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Zero α
f✝ : ι →₀ α
i✝ : ι
a : α
f : ι →₀ α
i : ι
⊢ i ∉ f.support ↔ ¬{f i} ≠ 0

Tactic:
notMem_support_iff,

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
f✝ : ι →₀ α
i✝ : ι
a : α
f : ι →₀ α
i : ι
⊢ f i = 0 ↔ ¬{f i} ≠ 0
Module: Mathlib.Data.Finsupp.Interval

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : Zero α
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq ι
f✝ g✝ : ι →₀ α
i✝ : ι
a : α
f g : ι →₀ α
i : ι
⊢ i ∉ f.support ∧ i ∉ g.support ↔ ¬Icc (f i) (g i) ≠ 0

Tactic:
notMem_support_iff,

Goal state after:
ι : Type u_1
α : Type u_2
inst✝³ : Zero α
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq ι
f✝ g✝ : ι →₀ α
i✝ : ι
a : α
f g : ι →₀ α
i : ι
⊢ f i = 0 ∧ i ∉ g.support ↔ ¬Icc (f i) (g i) ≠ 0
Module: Mathlib.Data.Finsupp.Interval

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : Zero α
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq ι
f✝ g✝ : ι →₀ α
i✝ : ι
a : α
f g : ι →₀ α
i : ι
⊢ f i = 0 ∧ i ∉ g.support ↔ ¬Icc (f i) (g i) ≠ 0

Tactic:
notMem_support_iff,

Goal state after:
ι : Type u_1
α : Type u_2
inst✝³ : Zero α
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq ι
f✝ g✝ : ι →₀ α
i✝ : ι
a : α
f g : ι →₀ α
i : ι
⊢ f i = 0 ∧ g i = 0 ↔ ¬Icc (f i) (g i) ≠ 0
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
n₁ n₂ : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h₁ : m < n₁
h₂ : m < n₂
⊢ m ∈ Iio n₁

Tactic:
simpa

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
n₁ n₂ : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h₁ : m < n₁
h₂ : m < n₂
⊢ m ∈ Iio n₂

Tactic:
simpa

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
n₁ n₂ : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h₁ : m ≤ n₁
h₂ : m ≤ n₂
⊢ m ∈ Iic n₁

Tactic:
simpa

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
n₁ n₂ : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h₁ : m ≤ n₁
h₂ : m ≤ n₂
⊢ m ∈ Iic n₂

Tactic:
simpa

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPowerSeries σ R
x : σ →₀ ℕ
h : degree x < n
⊢ x ∈ ⋯.toFinset

Tactic:
simpa

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPowerSeries σ R
x : σ →₀ ℕ
h : n ≤ degree x
⊢ x ∉ ⋯.toFinset

Tactic:
simpa

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

Goal state before:
pp: n a : ℕ
ha : n + 1 ≤ a
⊢ ↑n < ↑a

Tactic:
simpa

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p q : MvPowerSeries σ R
x : σ →₀ ℕ
hx : degree x < n
⊢ x ∈ ⋯.toFinset

Tactic:
simpa

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

Goal state before:
pp: R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : MonoidWithZero R
a : R
n : ℕ
hn : a ^ n = 0
⊢ ∀ i ≥ n, a ^ i = 0

Tactic:
intro i hi

Goal state after:
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : MonoidWithZero R
a : R
n : ℕ
hn : a ^ n = 0
i : ℕ
hi : i ≥ n
⊢ a ^ i = 0
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : ↑p < weightedOrder w f
d : σ →₀ ℕ
hd : ¬(weight w) d = p
⊢ 0 = (coeff d) 0

Tactic:
· rw [map_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
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ Function.Surjective ⇑Valued.v

Tactic:
have h : Function.Surjective (Valued.v : (v.valuation K).Completion → ℤᵐ⁰) :=
    Valued.valuedCompletion_surjective_iff.mpr <| .of_comp (v.valuation_surjective K)
  exact h.comp (adicCompletion.toCompletion_surjective K v)

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace R
inst✝² : DecidableEq σ
inst✝¹ : CommSemiring R
inst✝ : Nonempty σ
f : MvPowerSeries σ R
d : σ →₀ ℕ
s : σ
h✝ : True
n : σ →₀ ℕ
hn : n ≥ d + Finsupp.single s 1
⊢ d < d + Finsupp.single s 1

Tactic:
simpa [Finsupp.lt_def] using ⟨s, by simp⟩

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring R'
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Module R' M
inst✝³ : SMulCommClass R R' M
inst✝² : TopologicalSpace M
inst✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
I : Submodule R M
hI : ↑I ∈ 𝓝 0
⊢ ∃ i', (↑i' ∈ 𝓝 0 ∧ (∀ (r : R), ∀ x ∈ i', r • x ∈ i') ∧ ∀ (r' : R'), ∀ x ∈ i', r' • x ∈ i') ∧ ↑i' ⊆ ↑I

Tactic:
rcases (hasBasis_submodule R').mem_iff.mp hI with ⟨J, hJ, J_sub_I⟩

Goal state after:
R : Type u_1
R' : Type u_2
M : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring R'
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Module R' M
inst✝³ : SMulCommClass R R' M
inst✝² : TopologicalSpace M
inst✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
I : Submodule R M
hI : ↑I ∈ 𝓝 0
J : Submodule R' M
hJ : ↑J ∈ 𝓝 0
J_sub_I : ↑J ⊆ ↑I
⊢ ∃ i', (↑i' ∈ 𝓝 0 ∧ (∀ (r : R), ∀ x ∈ i', r • x ∈ i') ∧ ∀ (r' : R'), ∀ x ∈ i', r' • x ∈ i') ∧ ↑i' ⊆ ↑I
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ = 0
⊢ ⊤ < ⊤ ↔ φ ≠ 0

Tactic:
simpa

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : ¬φ = 0
⊢ ↑(Nat.find ⋯) < ⊤ ↔ φ ≠ 0

Tactic:
simpa

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

Tactic:
by
    ext
    simp +instances only [Algebra.smul_def]
    rfl

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

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

Tactic:
simpa

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

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

Tactic:
intro i hi

Goal state after:
case left
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
i : ℕ
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

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

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

Tactic:
intro i hi

Goal state after:
case neg.left
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : ↑i = ↑n
⊢ (coeff i) ((monomial n) a) ≠ 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg.right
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ∀ (i : ℕ), ↑i < ↑n → (coeff i) ((monomial n) a) = 0

Tactic:
intro i hi

Goal state after:
case neg.right
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : ↑i < ↑n
⊢ (coeff i) ((monomial n) a) = 0
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n a b : ℕ
f g : R⟦X⟧
ha : n < a
hb : n < b
⊢ (coeff n) (↑((trunc a) f) * ↑((trunc b) g)) = (coeff n) (f * g)

Tactic:
← coeff_coe_trunc_of_lt n.lt_succ_self,

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
n a b : ℕ
f g : R⟦X⟧
ha : n < a
hb : n < b
⊢ (coeff n) ↑((trunc n.succ) (↑((trunc a) f) * ↑((trunc b) g))) = (coeff n) (f * g)
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case inr
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
x✝ : ℕ∞
ho : φ.order = x✝
⊢ x✝ = emultiplicity X φ

Tactic:
cases ho : order φ with

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

Goal state before:
pp: R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ a, ∀ (b : ι), a ≤ b → ↑n < (f b).order
i : ι
hi : ∀ (b : ι), i ≤ b → ↑n < (f b).order
k : ι
hk : i < k
⊢ ↑n < (f k).order

Tactic:
by simpa using (hi k hk.le)

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

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

Tactic:
simpa

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R⟦X⟧
h : f ≠ 0 ∧ g ≠ 0
⊢ f.divXPowOrder * g.divXPowOrder * X ^ (g.order.toNat + f.order.toNat) =
    f.divXPowOrder * g.divXPowOrder * X ^ (f.order.toNat + g.order.toNat)

Tactic:
add_comm

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R⟦X⟧
h : f ≠ 0 ∧ g ≠ 0
⊢ f.divXPowOrder * g.divXPowOrder * X ^ (f.order.toNat + g.order.toNat) =
    f.divXPowOrder * g.divXPowOrder * X ^ (f.order.toNat + g.order.toNat)
Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
⊢ basis σ R (J, d) ≤ basis σ R (K, e) → J ≤ K ∧ e ≤ d

Tactic:
simp only [basis, TwoSidedIdeal.le_iff, TwoSidedIdeal.coe_mk', ofPred_subset_ofPred]
    intro h
    constructor
    · intro x hx
      have (d' : _) : coeff d' (C (σ := σ) x) ∈ J := by
        rw [coeff_C]; split_ifs <;> [exact hx; exact J.zero_mem]
      simpa using h (C x) (fun _ _ ↦ this _) _ zero_le
    · by_contra h'
      apply hK
      rw [eq_top_iff]
      intro x _
      have (d') (hd'_le : d' ≤ d) : coeff d' (monomial e x) ∈ J := by
        rw [coeff_monomial]
        split_ifs with hd' <;> [exact (h' (hd' ▸ hd'_le)).elim; exact J.zero_mem]
      simpa using h (monomial e x) this _ le_rfl

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

Goal state before:
pp: ⊢ ℵ_ 1 ≤ 𝔠

Tactic:
by
  rw [← succ_aleph0]
  exact Order.succ_le_of_lt aleph0_lt_continuum

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.FiniteDimensional

Goal state before:
pp: ⊢ Module.rank ℚ ℂ = 𝔠

Tactic:
refine (Free.rank_eq_mk_of_infinite_lt ℚ ℂ ?_).trans Cardinal.mk_complex

Goal state after:
⊢ Cardinal.lift.{0, 0} #ℚ < Cardinal.lift.{0, 0} #ℂ
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
f : MvPowerSeries σ R
⊢ ∀ (i : σ →₀ ℕ), ¬(coeff i) f = 0 → (⨅ i, (a i).order) * f.order ≤ (Finsupp.weight ((weightedOrder fun x ↦ 1) ∘ a)) i

Tactic:
intro i hi

Goal state after:
σ : 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
i : σ →₀ ℕ
hi : ¬(coeff i) f = 0
⊢ (⨅ i, (a i).order) * f.order ≤ (Finsupp.weight ((weightedOrder fun x ↦ 1) ∘ a)) i
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case h
f : ℕ → ℂ
s : ℂ
h : Summable fun x ↦ ‖term f s x‖
n : ℕ
hn₀ : n ≠ 0
hn : (∑' (n : ℕ), ‖term f s n‖) * ↑n ^ s.re < ‖f n‖
this : ‖term f s n‖ ≤ ∑' (i : ℕ), ‖term f s i‖
⊢ False

Tactic:
rw [norm_term_eq, if_neg hn₀,
    div_le_iff₀ <| Real.rpow_pos_of_pos (Nat.cast_pos.mpr <| Nat.pos_of_ne_zero hn₀) _] at this

Goal state after:
case h
f : ℕ → ℂ
s : ℂ
h : Summable fun x ↦ ‖term f s x‖
n : ℕ
hn₀ : n ≠ 0
hn : (∑' (n : ℕ), ‖term f s n‖) * ↑n ^ s.re < ‖f n‖
this : ‖f n‖ ≤ (∑' (i : ℕ), ‖term f s i‖) * ↑n ^ s.re
⊢ False
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case refine_1
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
⊢ Summable fun n ↦ ↑n ^ (-s.re + x - 1)

Tactic:
simpa

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

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
f : A⟦X⟧
hf : HasSubst f
n k : ℕ
hk : MvPowerSeries.constantCoeff f ^ k = 0
n' : ℕ
hn' : n' ≤ n
m : ℕ
hm : k * (n + 1) + m ∈ Set.Ici (k * (n + 1))
⊢ ↑n' < ((f ^ k) ^ (n + 1)).order + (f ^ m).order

Tactic:
← le_order_pow_of_constantCoeff_eq_zero _
    (by rwa [map_pow]),

Goal state after:
A : Type u_1
inst✝ : CommRing A
f : A⟦X⟧
hf : HasSubst f
n k : ℕ
hk : MvPowerSeries.constantCoeff f ^ k = 0
n' : ℕ
hn' : n' ≤ n
m : ℕ
hm : k * (n + 1) + m ∈ Set.Ici (k * (n + 1))
⊢ ↑n' < ↑(n + 1) + (f ^ m).order
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
f : MvPowerSeries σ R
inst✝¹ : Finite τ
x : σ → ℕ
k : ℕ
inst✝ : Finite σ
h : ∀ (i : σ), constantCoeff (a i) = 0
hx : ∀ (i : σ), k ≤ x i
⊢ (truncTotal k) (∑ i ∈ range k, subst (fun i ↦ ↑((truncTotal (x i)) (a i))) ((homogeneousComponent i) f)) =
    (truncTotal k) (subst (fun i ↦ ↑((truncTotal (x i)) (a i))) ↑((truncTotal k) f))

Tactic:
truncTotal_eq_sum,

Goal state after:
σ : 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
f : MvPowerSeries σ R
inst✝¹ : Finite τ
x : σ → ℕ
k : ℕ
inst✝ : Finite σ
h : ∀ (i : σ), constantCoeff (a i) = 0
hx : ∀ (i : σ), k ≤ x i
⊢ (truncTotal k) (∑ i ∈ range k, subst (fun i ↦ ↑((truncTotal (x i)) (a i))) ((homogeneousComponent i) f)) =
    (truncTotal k) (subst (fun i ↦ ↑((truncTotal (x i)) (a i))) (∑ i ∈ range k, (homogeneousComponent i) f))
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
w : τ → ℕ
ha : HasSubst a
f : R⟦X⟧
⊢ ∀ (i : Unit →₀ ℕ),
    ¬(MvPowerSeries.coeff i) f = 0 →
      f.order * MvPowerSeries.weightedOrder w a ≤
        (Finsupp.weight (Function.const Unit (MvPowerSeries.weightedOrder w a))) i

Tactic:
intro i hi

Goal state after:
R : Type u_2
inst✝² : CommRing R
τ : Type u_3
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : MvPowerSeries τ S
w : τ → ℕ
ha : HasSubst a
f : R⟦X⟧
i : Unit →₀ ℕ
hi : ¬(MvPowerSeries.coeff i) f = 0
⊢ f.order * MvPowerSeries.weightedOrder w a ≤ (Finsupp.weight (Function.const Unit (MvPowerSeries.weightedOrder w a))) i
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hs : Balanced 𝕜 s
hx : egauge 𝕜 s x < 1
⊢ egauge 𝕜 s x < ‖1‖ₑ

Tactic:
simpa

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedDivisionRing 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : (𝓝[≠] 0).NeBot
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → 0 ∈ c • s → r ≤ ‖c‖ₑ
hc : 0 ∈ 0 • s
b : ℝ≥0∞
hb : ‖0‖ₑ < b
c : 𝕜
hc₀ : c ∈ {0}ᶜ
hcb : c ∈ eball 0 b
⊢ ‖c‖ₑ < b

Tactic:
simpa using hcb

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ c ≠ 0

Tactic:
simpa

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
n : ℕ
s : Set ι
hs : s ∈ cofinite
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, (f y) i = 1 i
t : Finset ι := ⋯.toFinset
u v : Finset ι
hu : t ⊆ u
hv : t ⊆ v
⊢ ∀ i ∈ u \ t, i ∈ s

Tactic:
intro i hi

Goal state after:
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
n : ℕ
s : Set ι
hs : s ∈ cofinite
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, (f y) i = 1 i
t : Finset ι := ⋯.toFinset
u v : Finset ι
hu : t ⊆ u
hv : t ⊆ v
i : ι
hi : i ∈ u \ t
⊢ i ∈ s
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
h : c = 0 → s.Nonempty
x : E
hc : c ≠ 0
⊢ ‖c‖ₑ ≠ 0

Tactic:
simpa

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
h : c = 0 → s.Nonempty
x : E
hc : c ≠ 0
⊢ c ≠ 0

Tactic:
simpa

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
n : ℕ
s : Set ι
hs : s ∈ cofinite
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, (f y) i = 1 i
t : Finset ι := ⋯.toFinset
u v : Finset ι
hv : t ⊆ v
hu : ∀ i ∈ u \ t, i ∈ s
⊢ ∀ i ∈ v \ t, i ∈ s

Tactic:
intro i hi

Goal state after:
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
n : ℕ
s : Set ι
hs : s ∈ cofinite
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, (f y) i = 1 i
t : Finset ι := ⋯.toFinset
u v : Finset ι
hv : t ⊆ v
hu : ∀ i ∈ u \ t, i ∈ s
i : ι
hi : i ∈ v \ t
⊢ i ∈ s
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
hIne : I.Nonempty
i₀ : ι
hi₀I : i₀ ∈ I
hc_max : IsMaxOn (fun x ↦ ‖c x‖ₑ) I i₀
H : c i₀ = 0 ∧ I ≠ univ
hc0 : ∀ i ∈ I, c i = 0
heg0 : ∀ i ∈ I, x i = 0
⊢ ¬∃ i ∈ I, x i ≠ 0

Tactic:
simpa

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
c₀ : 𝕜
hc₀ : c₀ ≠ 0 ∨ I = univ
hc₀I : ∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖
hc₀r : ‖c₀‖ₑ < r
⊢ x ∈ I.pi (c₀ • U)

Tactic:
intro i hi

Goal state after:
𝕜 : 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
c₀ : 𝕜
hc₀ : c₀ ≠ 0 ∨ I = univ
hc₀I : ∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖
hc₀r : ‖c₀‖ₑ < r
i : ι
hi : i ∈ I
⊢ x i ∈ (c₀ • U) i