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 Γ₀
F : Filter K
hF : Cauchy F
h0 : 𝓝 0 ⊓ F = ⊥
U : Set K
U_in : U ∈ 𝓝 0
M : Set K
M_in : M ∈ F
H : U ∩ M = ∅
γ₀ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
hU : {x | v.restrict x < ↑γ₀} ⊆ U
x : K
xM : x ∈ M
⊢ ↑γ₀ ≤ v.restrict x

Tactic:
apply le_of_not_gt _

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
hF : Cauchy F
h0 : 𝓝 0 ⊓ F = ⊥
U : Set K
U_in : U ∈ 𝓝 0
M : Set K
M_in : M ∈ F
H : U ∩ M = ∅
γ₀ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
hU : {x | v.restrict x < ↑γ₀} ⊆ U
x : K
xM : x ∈ M
⊢ ¬v.restrict x < ↑γ₀
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case ih
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x✝ y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x y : K
⊢ v.restrict (x * y) = v.restrict x * v.restrict y

Tactic:
exact Valuation.map_mul _ _ _

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

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : (ofClass v).ValueGroup₀ := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := extensionValuation x
hγ₀_def : γ₀ = extensionValuation x
heq : γ₀ = embedding γ₀'
this : γ₀ ≠ 0 → (x ∈ closure (Completion.coe' '' {x | v x < ↑γ}) ↔ γ₀ < ↑γ)
h : γ₀ = 0
⊢ x ∈ closure (Completion.coe' '' {x | v x < ↑γ}) ↔ x ∈ {x | extensionValuation x < ↑γ}

Tactic:
simp only [(Valuation.zero_iff _).mp h, mem_ofPred_eq, Valuation.map_zero, Units.zero_lt,
        iff_true]

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : (ofClass v).ValueGroup₀ := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := extensionValuation x
hγ₀_def : γ₀ = extensionValuation x
heq : γ₀ = embedding γ₀'
this : γ₀ ≠ 0 → (x ∈ closure (Completion.coe' '' {x | v x < ↑γ}) ↔ γ₀ < ↑γ)
h : γ₀ = 0
⊢ 0 ∈ closure (Completion.coe' '' {x | v x < ↑γ})
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
⊢ Commute φ ((monomial n) a) ↔ ∀ (m : σ →₀ ℕ), Commute ((coeff m) φ) a

Tactic:
rw [commute_iff_eq, MvPowerSeries.ext_iff]
  refine ⟨fun h m => ?_, fun h m => ?_⟩
  · have := h (m + n)
    rwa [coeff_add_mul_monomial, add_comm, coeff_add_monomial_mul] at this
  · rw [coeff_mul_monomial, coeff_monomial_mul]
    split_ifs <;> [apply h; rfl]

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

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

Tactic:
set nmin :=
          min ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)
            ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
⊢ X s = X t → s = t

Tactic:
classical
    intro h
    replace h := congr_arg (coeff (single s 1)) h
    rw [coeff_X, if_pos rfl, coeff_X] at h
    split_ifs at h with H
    · rw [Finsupp.single_eq_single_iff] at H
      rcases H with H | H
      · exact H.1
      · exfalso
        exact one_ne_zero H.1
    · exfalso
      exact one_ne_zero h

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
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)
    ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)
⊢ nmin ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors

Tactic:
exact min_le_left _ _

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : DivisionSemiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
φ : MvPowerSeries σ R
f : R →+* S
⊢ (map f) φ = 0 ↔ φ = 0

Tactic:
simp only [MvPowerSeries.ext_iff]

Goal state after:
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : DivisionSemiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
φ : MvPowerSeries σ R
f : R →+* S
⊢ (∀ (n : σ →₀ ℕ), (coeff n) ((map f) φ) = (coeff n) 0) ↔ ∀ (n : σ →₀ ℕ), (coeff n) φ = (coeff n) 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ ∀ (x y : R⟦X⟧),
    (mk fun n ↦ a ^ n * (coeff n) (x + y)) = (mk fun n ↦ a ^ n * (coeff n) x) + mk fun n ↦ a ^ n * (coeff n) y

Tactic:
intros
    ext
    exact mul_add _ _ _

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
r : R
⊢ (valuation K v) ↑r < 1 ↔ v.asIdeal ∣ Ideal.span {r}

Tactic:
by
  rw [valuation_of_algebraMap]; exact v.intValuation_lt_one_iff_dvd r

Goal state after:
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 : weightedOrder w f = ↑n
d : σ →₀ ℕ
hd : (coeff d) f ≠ 0 ∧ ↑((weight w) d) = weightedOrder w f
e : σ →₀ ℕ
he : (weight w) e < n
⊢ ↑((weight w) e) < weightedOrder w f

Tactic:
by simp only [h, Nat.cast_lt, he]

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
⊢ ∀ (x : ↥(adicCompletionIntegers K v)),
    Valued.v ((algebraMap (↥(adicCompletionIntegers K v)) (adicCompletion K v)) x) ≤ 1

Tactic:
simp [mem_adicCompletionIntegers]

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
⊢ ∀ ⦃r : adicCompletion K v⦄,
    Valued.v r ≤ 1 → ∃ x, (algebraMap (↥(adicCompletionIntegers K v)) (adicCompletion K v)) x = r

Tactic:
simp [mem_adicCompletionIntegers]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
r : R
f : R⟦X⟧
⊢ (trunc n) (C r * f) = Polynomial.C r * (trunc n) f

Tactic:
ext i; simp [coeff_trunc]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
f : R⟦X⟧
r : R
⊢ (trunc n) (f * C r) = (trunc n) f * Polynomial.C r

Tactic:
ext i; simp [coeff_trunc]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : ↑n < ψ.order
⊢ (coeff n) (φ * ψ) = 0

Tactic:
suffices coeff n (φ * ψ) = ∑ p ∈ antidiagonal n, 0 by rw [this, Finset.sum_const_zero]
  rw [coeff_mul]
  apply Finset.sum_congr rfl
  intro x hx
  refine mul_eq_zero_of_right (coeff x.fst φ) (coeff_of_lt_order x.snd (lt_of_le_of_lt ?_ h))
  rw [mem_antidiagonal] at hx
  norm_cast
  lia

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

Goal state before:
pp: case inr.coe
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
⊢ ↑φ.order.toNat ≤ emultiplicity X φ

pp: R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
⊢ emultiplicity X φ ≤ ↑φ.order.toNat

Tactic:
· apply le_emultiplicity_of_pow_dvd
      apply X_pow_order_dvd

Goal state after:
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
⊢ emultiplicity X φ ≤ ↑φ.order.toNat
Module: Mathlib.RingTheory.PowerSeries.Order

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

Tactic:
order_monomial

Goal state after:
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.toNat + 1) * ψ
this : (coeff n) φ = (coeff n) (ψ * X ^ (φ.order.toNat + 1))
⊢ ↑n < if 1 = 0 then ⊤ else ↑(φ.order.toNat + 1)
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}
⊢ ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, (eval₂Hom φ a) x ∈ ↑I

Tactic:
have hn_ne : ∀ s, Set.Nonempty {n : ℕ | (a s) ^ n.succ ∈ I} := fun s ↦ by
    rcases ha.hpow s |>.eventually_mem hI |>.exists_forall_of_atTop with ⟨n, hn⟩
    use n
    simpa using hn n.succ n.le_succ

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
⊢ ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, (eval₂Hom φ a) x ∈ ↑I
Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsLinearTopology R R
f : MvPowerSeries σ R
hf : IsTopologicallyNilpotent (constantCoeff f)
d : σ →₀ ℕ
⊢ ∀ (i : Ideal R), ↑i ∈ 𝓝 0 → ∀ᶠ (x : ℕ) in atTop, (coeff d) (f ^ x) ∈ ↑i

Tactic:
I

Goal state after:
σ : Type u_1
R : Type u_3
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsLinearTopology R R
f : MvPowerSeries σ R
hf : IsTopologicallyNilpotent (constantCoeff f)
d : σ →₀ ℕ
I : Ideal R
⊢ ↑I ∈ 𝓝 0 → ∀ᶠ (x : ℕ) in atTop, (coeff d) (f ^ x) ∈ ↑I
Module: Mathlib.SetTheory.Cardinal.Continuum

Goal state before:
pp: c : Cardinal.{u}
⊢ 𝔠 ≤ lift.{v, u} c ↔ 𝔠 ≤ c

Tactic:
← lift_continuum.{v, u},

Goal state after:
c : Cardinal.{u}
⊢ lift.{v, u} 𝔠 ≤ lift.{v, u} c ↔ 𝔠 ≤ c
Module: Mathlib.SetTheory.Cardinal.Continuum

Goal state before:
pp: c : Cardinal.{u}
⊢ lift.{v, u} c ≤ 𝔠 ↔ c ≤ 𝔠

Tactic:
← lift_continuum.{v, u},

Goal state after:
c : Cardinal.{u}
⊢ lift.{v, u} c ≤ lift.{v, u} 𝔠 ↔ c ≤ 𝔠
Module: Mathlib.SetTheory.Cardinal.Continuum

Goal state before:
pp: c : Cardinal.{u}
⊢ 𝔠 < lift.{v, u} c ↔ 𝔠 < c

Tactic:
← lift_continuum.{v, u},

Goal state after:
c : Cardinal.{u}
⊢ lift.{v, u} 𝔠 < lift.{v, u} c ↔ 𝔠 < c
Module: Mathlib.SetTheory.Cardinal.Continuum

Goal state before:
pp: c : Cardinal.{u}
⊢ lift.{v, u} c < 𝔠 ↔ c < 𝔠

Tactic:
← lift_continuum.{v, u},

Goal state after:
c : Cardinal.{u}
⊢ lift.{v, u} c < lift.{v, u} 𝔠 ↔ c < 𝔠
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
h : f =ᶠ[cofinite] g
hf : LSeriesSummable f s
⊢ term f s =ᶠ[cofinite] term g s

Tactic:
eventuallyEq_iff_exists_mem

Goal state after:
f g : ℕ → ℂ
s : ℂ
h : ∃ s ∈ cofinite, Set.EqOn f g s
hf : LSeriesSummable f s
⊢ ∃ s_1 ∈ cofinite, Set.EqOn (term f s) (term g s) s_1
Module: Mathlib.NumberTheory.LSeries.Basic

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

Tactic:
simpa only [term_zero, norm_zero] using norm_nonneg _

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
r : R
f : R⟦X⟧
n : ℕ
⊢ (coeff n) ((rescale r) f) = (coeff n) ((MvPowerSeries.rescale fun x ↦ r) f)

Tactic:
rw [coeff_rescale, coeff, MvPowerSeries.coeff_rescale]

Goal state after:
R : Type u_2
inst✝ : CommRing R
r : R
f : R⟦X⟧
n : ℕ
⊢ r ^ n * (MvPowerSeries.coeff (Finsupp.single () n)) f =
    ((Finsupp.single () n).prod fun s m ↦ r ^ m) * (MvPowerSeries.coeff (Finsupp.single () n)) f
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
this : UniformSpace R := ⋯
⊢ IsClosed (Set.range DFunLike.coe)

Tactic:
have : Set.range ((↑) : ArithmeticFunction R → (ℕ → R)) = {f | f 0 = 0} := by
    ext f
    exact ⟨by rintro ⟨f, rfl⟩; simp, fun hf ↦ ⟨⟨f, hf⟩, rfl⟩⟩

Goal state after:
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
this✝ : UniformSpace R := ⊥
this : Set.range DFunLike.coe = {f | f 0 = 0}
⊢ IsClosed (Set.range DFunLike.coe)
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
inst✝ : (𝓝[≠] 0).NeBot
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → x ∈ c • s → r ≤ ‖c‖ₑ
⊢ r ≤ egauge 𝕜 s x

Tactic:
by
  rw [le_egauge_iff]
  intro c hc
  rcases ne_or_eq c 0 with hc₀ | rfl
  · exact h c hc₀ hc
  obtain rfl : x = 0 := by
    grw [zero_smul_set_subset, Set.mem_zero] at hc
    exact hc
  apply le_of_forall_gt
  intro b hb
  rcases Filter.nonempty_of_mem <|
    inter_mem_nhdsWithin {(0 : 𝕜)}ᶜ (Metric.eball_mem_nhds 0 (by simpa using hb))
    with ⟨c, hc₀, hcb⟩
  exact (h c (by simpa using hc₀) ⟨_, hs₀, by simp⟩).trans_lt (by simpa using hcb)

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

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝²¹ : CommSemiring A
R✝ : Type u_3
inst✝²⁰ : CommRing R✝
inst✝¹⁹ : Algebra A R✝
τ : Type u_4
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R✝ S
inst✝¹⁵ : IsScalarTower A R✝ S
a✝¹ a✝ : σ → MvPowerSeries τ S
T✝ : Type u_6
inst✝¹⁴ : CommRing T✝
inst✝¹³ : UniformSpace T✝
inst✝¹² : T2Space T✝
inst✝¹¹ : CompleteSpace T✝
inst✝¹⁰ : IsUniformAddGroup T✝
inst✝⁹ : IsTopologicalRing T✝
inst✝⁸ : IsLinearTopology T✝ T✝
inst✝⁷ : Algebra R✝ T✝
ε : MvPowerSeries τ S →ₐ[R✝] T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R✝ S T✝
υ : Type u_7
T : Type u_8
inst✝⁴ : CommRing T
inst✝³ : Algebra R✝ T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R✝ S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst✝ : CommSemiring R
a : σ → R
⊢ ∀ (x y : MvPowerSeries σ R),
    (fun n ↦ (n.prod fun s m ↦ a s ^ m) * (coeff n) (x + y)) =
      (fun n ↦ (n.prod fun s m ↦ a s ^ m) * (coeff n) x) + fun n ↦ (n.prod fun s m ↦ a s ^ m) * (coeff n) y

Tactic:
intros
    ext
    exact mul_add _ _ _

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

Goal state before:
pp: case neg
𝕜 : 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
⊢ ∃ c₀, (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r

Tactic:
have : (𝓝[≠] (0 : 𝕜)).NeBot := (hI₀.resolve_left H.2).resolve_left (by simpa)

Goal state after:
case neg
𝕜 : 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
this : (𝓝[≠] 0).NeBot
⊢ ∃ c₀, (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r
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]

Goal state after:
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) = (coeff (n + 1 + 1)) (subst B P)
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ MvPolynomial.coeff e ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ (single () (e 0 + e 1)) PUnit.unit) *
      (MvPowerSeries.coeff (single () (e 0 + e 1))) f =
    ↑((e 0 + e 1).choose (e 0)) * (coeff (e 0 + e 1)) f

pp: R : Type u_2
inst✝ : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ ∀ (x : Unit →₀ ℕ),
    x ≠ single () (e 0 + e 1) →
      (MvPowerSeries.coeff x) f * MvPolynomial.coeff e ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ x PUnit.unit) = 0

Tactic:
· simp [MvPolynomial.coeff_add_pow, coeff]

Goal state after:
R : Type u_2
inst✝ : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ ∀ (x : Unit →₀ ℕ),
    x ≠ single () (e 0 + e 1) →
      (MvPowerSeries.coeff x) f * MvPolynomial.coeff e ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ x PUnit.unit) = 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
⊢ HasFDerivWithinAt f f' (s \ {x}) x ↔ HasFDerivWithinAt f f' (t \ {x}) x

Tactic:
suffices 𝓝[s \ {x}] x = 𝓝[t \ {x}] x by simp only [HasFDerivWithinAt, this]

Goal state after:
𝕜 : 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
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
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : ↑‖x‖₊ + ↑‖y‖₊ < p.radius
x_mem_ball : x ∈ Metric.eball 0 p.radius
y_mem_ball : y ∈ Metric.eball 0 (p.changeOrigin x).radius
x_add_y_mem_ball : x + y ∈ Metric.eball 0 p.radius
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s ↦ ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y
⊢ Summable f

Tactic:
refine .of_nnnorm_bounded (p.changeOriginSeries_summable_aux₁ h) ?_

Goal state after:
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : ↑‖x‖₊ + ↑‖y‖₊ < p.radius
x_mem_ball : x ∈ Metric.eball 0 p.radius
y_mem_ball : y ∈ Metric.eball 0 (p.changeOrigin x).radius
x_add_y_mem_ball : x + y ∈ Metric.eball 0 p.radius
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s ↦ ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y
⊢ ∀ (i : (k : ℕ) × (l : ℕ) × { s // s.card = l }), ‖f i‖₊ ≤ ‖p (i.fst + i.snd.fst)‖₊ * ‖x‖₊ ^ i.snd.fst * ‖y‖₊ ^ i.fst
Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry

Goal state before:
pp: 𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : Ei 0 →L[𝕜] Ei i.succ [×n]→L[𝕜] G
⊢ f.uncurryLeft.curryLeft = f

Tactic:
ext m x

Goal state after:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : Ei 0 →L[𝕜] Ei i.succ [×n]→L[𝕜] G
m : Ei 0
x : (i : Fin n) → Ei i.succ
⊢ (f.uncurryLeft.curryLeft m) x = (f m) x
Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry

Goal state before:
pp: 𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : Ei i.castSucc [×n]→L[𝕜] Ei (last n) →L[𝕜] G
⊢ f.uncurryRight.curryRight = f

Tactic:
ext m x

Goal state after:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : Ei i.castSucc [×n]→L[𝕜] Ei (last n) →L[𝕜] G
m : (i : Fin n) → Ei i.castSucc
x : Ei (last n)
⊢ (f.uncurryRight.curryRight m) x = (f m) x
Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry

Goal state before:
pp: 𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : Ei i.castSucc [×n]→L[𝕜] Ei (last n) →L[𝕜] G
⊢ f.uncurryRight.curryRight = f

Tactic:
ext m x
  rw [ContinuousMultilinearMap.curryRight_apply, ContinuousMultilinearMap.uncurryRight_apply,
    snoc_last, init_snoc]

Goal state after: