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

Goal state before:
pp: case inr.succ
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
⊢ (coeff (0, 1).1) (φ ^ n') * (coeff (0, 1).2) φ + (coeff (1, 0).1) (φ ^ n') * (coeff (1, 0).2) φ =
    ↑(n' + 1) * (coeff 1) φ * constantCoeff φ ^ (n' + 1 - 1)

Tactic:
simp only [coeff_zero_eq_constantCoeff, map_pow, Nat.cast_add, Nat.cast_one,
          add_tsub_cancel_right]
        have h₀ : n' = 0 ∨ 1 ≤ n' := by lia
        rcases h₀ with h' | h'
        · by_contra h''
          rw [h'] at h''
          simp only [pow_zero, one_mul, coeff_one, one_ne_zero, ↓reduceIte, zero_mul, add_zero,
            mul_one] at h''
          norm_num at h''
        · rw [ih]
          · conv => lhs; arg 2; rw [mul_comm, ← mul_assoc]
            move_mul [← constantCoeff φ ^ (n' - 1)]
            conv => enter [1, 2, 1, 1, 2]; rw [← pow_one (a := constantCoeff φ)]
            rw [← pow_add (a := constantCoeff φ)]
            conv => enter [1, 2, 1, 1]; rw [Nat.sub_add_cancel h']
            ring
          exact h'

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

Goal state before:
pp: case refine_1
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✝ : ∃ i, {x | embedding (extension x) < embedding ↑i} ⊆ s
γ : (ofClass v).ValueGroup₀ˣ
h : {x | embedding (extension x) < embedding ↑γ} ⊆ s
⊢ ∃ γ, {x | extensionValuation.restrict x < ↑γ} ⊆ s

pp: case refine_2
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
⊢ ∃ i, {x | embedding (extension x) < embedding ↑i} ⊆ s

Tactic:
· use Units.map valueGroup₀_equiv_extensionValuation.toMonoidHom γ
        convert! h
        apply this

Goal state after:
case refine_2
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
⊢ ∃ i, {x | embedding (extension x) < embedding ↑i} ⊆ s
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
⊢ weightedOrder w f ≠ ⊤ ↔ f ≠ 0

Tactic:
ne_zero_iff_weightedOrder_finite w,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
⊢ weightedOrder w f ≠ ⊤ ↔ ↑(weightedOrder w f).toNat = weightedOrder w f
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
p : ℕ
r : R
⊢ (MvPowerSeries.monomial (p • e)) r = MvPowerSeries.C r * e.prod fun s e ↦ (MvPowerSeries.X s ^ p) ^ e

Tactic:
MvPowerSeries.monomial_eq',

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
p : ℕ
r : R
⊢ (MvPowerSeries.C r * (p • e).prod fun s e ↦ MvPowerSeries.X s ^ e) =
    MvPowerSeries.C r * e.prod fun s e ↦ (MvPowerSeries.X s ^ p) ^ e
Module: Mathlib.RingTheory.MvPowerSeries.Order

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

Tactic:
rw [← hn, ← hd] at H

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

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

Tactic:
rwa [ne_eq, Ideal.span_singleton_eq_bot]

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

Goal state before:
pp: case refine_2.refine_1
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
⊢ {y | Valued.v.restrict y < ↑((Units.mapEquiv (valueGroupOrderIso K v).toMulEquiv) γ)} ∈ 𝓝 0

Tactic:
rw [Valued.mem_nhds_zero]
        exact ⟨Units.mapEquiv (valueGroupOrderIso K v).toMulEquiv γ, subset_rfl⟩

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

Goal state before:
pp: σ : Type u_3
R : Type u_4
t u : TopologicalSpace R
htu : t ≤ u
⊢ ⨅ i, TopologicalSpace.induced (fun f ↦ f i) ((fun i ↦ t) i) ≤
    ⨅ i, TopologicalSpace.induced (fun f ↦ f i) ((fun i ↦ u) i)

Tactic:
gcongr

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

Goal state before:
pp: case pos.inr.inr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : ↑p ≤ weightedOrder w f
hg : ↑q ≤ weightedOrder w g
d : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hd : (weight w) x.1 + (weight w) x.2 = p + q
hx : x.1 + x.2 = d
h : (weight w) x.2 < q
⊢ (coeff x.1) f * (coeff x.2) g =
    (if (weight w) x.1 = p then (coeff x.1) f else 0) * if (weight w) x.2 = q then (coeff x.2) g else 0

Tactic:
· rw [if_neg (ne_of_lt h), mul_zero]
      rw [← ENat.natCast_lt_natCast] at h
      rw [coeff_eq_zero_of_lt_weightedOrder w (lt_of_lt_of_le h hg), mul_zero]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : CommSemiring R
f : MvPowerSeries σ R
hf : constantCoeff f = 0
⊢ IsNilpotent 0

Tactic:
exact IsNilpotent.zero

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
J : Submodule R' M
hJ : ↑J ∈ 𝓝 0
J_sub_I : ↑J ⊆ ↑I
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • ↑I ⊆ ↑I
hR'J : uR' • ↑J ⊆ ↑J
hRJ : uR • ↑J ⊆ ↑I
S : Set M := ↑J ∪ uR • ↑J
S_sub_I : S ⊆ ↑I
⊢ uR • ↑J ∪ (uR * uR) • ↑J ⊆ uR • ↑J ∪ uR • ↑J

Tactic:
gcongr

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
J : Submodule R' M
hJ : ↑J ∈ 𝓝 0
J_sub_I : ↑J ⊆ ↑I
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • ↑I ⊆ ↑I
hR'J : uR' • ↑J ⊆ ↑J
hRJ : uR • ↑J ⊆ ↑I
S : Set M := ↑J ∪ uR • ↑J
S_sub_I : S ⊆ ↑I
hRS : uR • S ⊆ S
⊢ uR' • ↑J ∪ uR • uR' • ↑J ⊆ ↑J ∪ uR • ↑J

Tactic:
gcongr

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

Goal state before:
pp: case inl
σ : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : CommSemiring R
ι : Type u_5
f : ι → MvPowerSeries σ R
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
w : σ → ℕ
h : Tendsto (fun i ↦ weightedOrder w (f i)) atTop (𝓝 ⊤)
hempty : IsEmpty ι
⊢ Summable fun x ↦ ∏ i ∈ x, f i

pp: case inr
σ : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : CommSemiring R
ι : Type u_5
f : ι → MvPowerSeries σ R
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
w : σ → ℕ
h : Tendsto (fun i ↦ weightedOrder w (f i)) atTop (𝓝 ⊤)
hempty : Nonempty ι
⊢ Summable fun x ↦ ∏ i ∈ x, f i

Tactic:
· apply Summable.of_finite

Goal state after:
case inr
σ : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : CommSemiring R
ι : Type u_5
f : ι → MvPowerSeries σ R
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
w : σ → ℕ
h : Tendsto (fun i ↦ weightedOrder w (f i)) atTop (𝓝 ⊤)
hempty : Nonempty ι
⊢ Summable fun x ↦ ∏ i ∈ x, f i
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
⊢ ∃ b ∈ R⁰, a * ↑b ∈ adicCompletionIntegers K v

Tactic:
by_cases ha : a ∈ v.adicCompletionIntegers K
  · use 1
    simp [ha]
  · rw [notMem_adicCompletionIntegers] at ha
    -- let ϖ be a uniformiser
    obtain ⟨ϖ, hϖ⟩ := intValuation_exists_uniformizer v
    have : Valued.v (algebraMap R (v.adicCompletion K) ϖ) = (exp (1 : ℤ))⁻¹ := by
      simp [valuedAdicCompletion_eq_valuation, valuation_of_algebraMap, hϖ, exp]
    have hϖ0 : ϖ ≠ 0 := by rintro rfl; simp [exp_ne_zero.symm] at hϖ
    refine ⟨ϖ^(log (Valued.v a)).natAbs, pow_mem (mem_nonZeroDivisors_of_ne_zero hϖ0) _, ?_⟩
    -- now manually translate the goal (an inequality in ℤᵐ⁰) to an inequality of "log" of ℤ
    simp only [map_pow, mem_adicCompletionIntegers, map_mul, this, inv_pow, ← exp_nsmul, nsmul_one,
      Int.natCast_natAbs]
    exact mul_inv_le_one_of_le₀ (le_exp_log.trans (by simp [le_abs_self])) zero_le

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
f : R⟦X⟧
j : ℕ
⊢ (coeff j) f = (coeff j) ((mk fun i ↦ (coeff (i + n)) f) * X ^ n) + ((trunc n) f).coeff j

Tactic:
coeff_mul_X_pow',

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℕ
f : R⟦X⟧
j : ℕ
⊢ (coeff j) f = (if n ≤ j then (coeff (j - n)) (mk fun i ↦ (coeff (i + n)) f) else 0) + ((trunc n) f).coeff j
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case insert
R : Type u_2
ι : Type u_3
inst✝ : CommRing R
k : ℕ
φ : R⟦X⟧
f : ι → R⟦X⟧
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑k < (f i).order) → (coeff k) (φ * ∏ i ∈ s, (1 - f i)) = (coeff k) φ
t : ↑k < (f a).order ∧ ∀ a ∈ s, ↑k < (f a).order
⊢ (coeff k) ((φ * ∏ x ∈ s, (1 - f x)) * (1 - f a)) = (coeff k) φ

Tactic:
coeff_mul_one_sub_of_lt_order _ t.1

Goal state after:
case insert
R : Type u_2
ι : Type u_3
inst✝ : CommRing R
k : ℕ
φ : R⟦X⟧
f : ι → R⟦X⟧
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑k < (f i).order) → (coeff k) (φ * ∏ i ∈ s, (1 - f i)) = (coeff k) φ
t : ↑k < (f a).order ∧ ∀ a ∈ s, ↑k < (f a).order
⊢ (coeff k) (φ * ∏ x ∈ s, (1 - f x)) = (coeff k) φ
Module: Mathlib.RingTheory.PowerSeries.PiTopology

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : CommSemiring R
ι : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
h : Tendsto (fun i ↦ (f i).order) atTop (𝓝 ⊤)
hempty : IsEmpty ι
⊢ Summable fun x ↦ ∏ i ∈ x, f i

pp: case inr
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : CommSemiring R
ι : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
h : Tendsto (fun i ↦ (f i).order) atTop (𝓝 ⊤)
hempty : Nonempty ι
⊢ Summable fun x ↦ ∏ i ∈ x, f i

Tactic:
· apply Summable.of_finite

Goal state after:
case inr
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : CommSemiring R
ι : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
h : Tendsto (fun i ↦ (f i).order) atTop (𝓝 ⊤)
hempty : Nonempty ι
⊢ Summable fun x ↦ ∏ i ∈ x, f 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✝⁶ : IsTopologicalSemiring R
inst✝⁵ : IsUniformAddGroup R
inst✝⁴ : IsUniformAddGroup S
inst✝³ : CompleteSpace S
inst✝² : T2Space S
inst✝¹ : IsTopologicalRing S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁹.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑φ
ha : HasEval a
⊢ UniformContinuous ⇑(eval₂Hom hφ ha)

Tactic:
exact uniformContinuous_uniformly_extend
    toMvPowerSeries_isUniformInducing
    denseRange_toMvPowerSeries
    (toMvPowerSeries_uniformContinuous hφ ha)

Goal state after:
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 g : MvPowerSeries σ R
⊢ subst a (f - g) = subst a f - subst a g

Tactic:
simp_rw [← substAlgHom_apply ha, map_sub]

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

Goal state before:
pp: case succ
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
n : ℕ
ih : ∀ {f g : ℕ → Bool}, (∀ k < n, f k = g k) → f n = false → g n = true → cantorFunction c f < cantorFunction c g
f g : ℕ → Bool
hn : ∀ k < n + 1, f k = g k
fn : f (n + 1) = false
gn : g (n + 1) = true
⊢ ((bif g 0 then 1 else 0) + c * cantorFunction c fun n ↦ f (n + 1)) <
    (bif g 0 then 1 else 0) + c * cantorFunction c fun n ↦ g (n + 1)

Tactic:
gcongr

Goal state after:
case hbc
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
n : ℕ
ih : ∀ {f g : ℕ → Bool}, (∀ k < n, f k = g k) → f n = false → g n = true → cantorFunction c f < cantorFunction c g
f g : ℕ → Bool
hn : ∀ k < n + 1, f k = g k
fn : f (n + 1) = false
gn : g (n + 1) = true
⊢ (cantorFunction c fun n ↦ f (n + 1)) < cantorFunction c fun n ↦ g (n + 1)
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
⊢ (PowerSeries.coeff k) (f * g) =
    ∑ x ∈ (q ^ k).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:
rw [PowerSeries.coeff_mul k f g, ← Finset.sum_subset hs]

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
⊢ ∑ p ∈ Finset.antidiagonal k, (PowerSeries.coeff p.1) f * (PowerSeries.coeff p.2) g =
    ∑
      x ∈
        Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
          (Finset.antidiagonal k),
      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

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
⊢ ∀ x ∈ (q ^ k).divisorsAntidiagonal,
    x ∉
        Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
          (Finset.antidiagonal k) →
      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 =
        0
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: a : ℝ
⊢ (fun x ↦ a + a - x) '' Iio a = Ioi a

Tactic:
simp only [image_const_sub_Iio, add_sub_cancel_right]

Goal state after:
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
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
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
ha : HasSubst a
b : τ → T
hb : HasEval b
f : MvPowerSeries σ R
⊢ eval₂ (algebraMap S T) b (subst a f) = eval₂ (algebraMap R T) (fun s ↦ eval₂ (algebraMap S T) b (a s)) f

Tactic:
by
  let ε : MvPowerSeries τ S →ₐ[R] T := (aeval hb).restrictScalars R
  have hε : Continuous ε := continuous_aeval hb
  simpa only [AlgHom.coe_restrictScalars', AlgHom.toRingHom_eq_coe,
    AlgHom.coe_restrictScalars, RingHom.coe_coe, ε, coe_aeval]
    using comp_subst_apply ha hε f

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

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

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

Goal state before:
pp: case isFalse
f g : ℕ → ℂ
s : ℂ
n : ℕ
h : ‖f n‖ ≤ ‖g n‖
h✝ : ¬n = 0
⊢ ‖f n‖ / ↑n ^ s.re ≤ ‖g n‖ / ↑n ^ s.re

Tactic:
gcongr

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

Goal state before:
pp: f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
n : ℕ
hn : ¬n = 0
⊢ ‖f n‖ / ↑n ^ s'.re ≤ ‖f n‖ / ↑n ^ s.re

Tactic:
gcongr

Goal state after:
case hx
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
n : ℕ
hn : ¬n = 0
⊢ 1 ≤ ↑n
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 : σ →₀ ℕ
hi : ¬(coeff i) f = 0
j : σ
hj : j ∈ i.support
⊢ (⨅ i, weightedOrder (fun x ↦ 1) (a i)) * ↑(i j) ≤ (fun i c ↦ ↑c * weightedOrder (fun x ↦ 1) (a i)) j (i j)

Tactic:
by
      simp [mul_comm, mul_le_mul_right (iInf_le_iff.mpr fun _ a ↦ a j)]

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

Goal state before:
pp: case inl
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : f =O[atTop] fun n ↦ ↑n ^ (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖↑x_1 ^ (x - 1)‖
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ‖f b‖ ≤ C * ‖↑b ^ (x - 1)‖
C' : ℝ := max C ((insert 0 (image (fun n ↦ ‖f n‖ / ↑n ^ (x - 1)) (range m))).max' ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀✝ : n ≠ 0
hn : m ≤ n
hn₀ : 0 ≤ ↑n
⊢ C * ‖↑n ^ (x - 1)‖ ≤ C' * ↑n ^ (x - 1)

Tactic:
gcongr

Goal state after:
case h₂
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : f =O[atTop] fun n ↦ ↑n ^ (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖↑x_1 ^ (x - 1)‖
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ‖f b‖ ≤ C * ‖↑b ^ (x - 1)‖
C' : ℝ := ⋯
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀✝ : n ≠ 0
hn : m ≤ n
hn₀ : 0 ≤ ↑n
⊢ ‖↑n ^ (x - 1)‖ ≤ ↑n ^ (x - 1)
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
⊢ egauge 𝕜 (c⁻¹ • c • s) x = egauge 𝕜 s x

Tactic:
inv_smul_smul₀ hc

Goal state after:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ egauge 𝕜 s x = egauge 𝕜 s x
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
c : 𝕜
s : Set E
h : c = 0 → s.Nonempty
x : E
hc : c ≠ 0
⊢ egauge 𝕜 s (c⁻¹ • c • x) = egauge 𝕜 s x

Tactic:
inv_smul_smul₀ hc

Goal state after:
case inr
𝕜 : 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
⊢ egauge 𝕜 s x = egauge 𝕜 s x
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: case e_a.succ.succ
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 (n + 1 + 1)) ((B + -(C k * X ^ (n + 2))) ^ (i + 1 + 1)) =
    (coeff (n + 1 + 1)) (B ^ (i + 1 + 1)) - if i + 1 + 1 = 1 then k else 0

Tactic:
· simp only [add_assoc, Nat.reduceAdd]
            rw [add_comm B, add_pow, map_sum, Finset.sum_eq_single (a := 0)]
            · simp
            · rintro (_ | _ | j) hj hj'
              · simp at hj'
              · simp [mul_comm (C k), hB', mul_assoc, coeff_X_pow_mul']
              · rw [← neg_mul, mul_pow, ← pow_mul, mul_comm (_ ^ _)]
                simp [mul_assoc, coeff_X_pow_mul']
            · simp

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
h : (comap (fun p ↦ p.1 • p.2) (𝓝 y) ⊓ ⊤ ×ˢ 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0).NeBot
⊢ ⊤ ×ˢ 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0 ≤ ⊤ ×ˢ 𝓝 0

Tactic:
gcongr

Goal state after:
case hg
R : Type u
E : Type v
inst✝² : AddCommGroup E
inst✝¹ : SMul R E
inst✝ : TopologicalSpace E
s : Set E
x y : E
h : (comap (fun p ↦ p.1 • p.2) (𝓝 y) ⊓ ⊤ ×ˢ 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0).NeBot
⊢ 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0 ≤ 𝓝 0
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ≥0
c : 𝕜
y : E
hy : ‖y‖₊ ≤ r
⊢ ‖c‖ₑ * ‖y‖ₑ ≤ ‖c‖ₑ * ↑r

Tactic:
gcongr

Goal state after:
case h₂
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ≥0
c : 𝕜
y : E
hy : ‖y‖₊ ≤ r
⊢ ‖y‖ₑ ≤ ↑r
Module: Mathlib.Analysis.Calculus.TangentCone.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : SMul 𝕜 E
inst✝ : TopologicalSpace E
s 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

Tactic:
gcongr

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
y : E
hy : y ∈ tangentConeAt 𝕜 s x
hy₀ : y ≠ 0
⊢ AccPt x (𝓟 s)

Tactic:
contrapose hy₀
  exact tangentConeAt_subset_zero hy₀ hy

Goal state after: