mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case neg
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) γ)}
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
γ : (ofClass v).ValueGroup₀ˣ
hx0 : ¬x = 0
⊢ (if h : (ofClass extensionValuation) x = 0 then 0 else ↑⟨Units.mk0 ((ofClass extensionValuation) x) h, ⋯⟩) <
      valueGroup₀_equiv_extensionValuation ↑γ ↔
    extension x < ↑γ

Tactic:
rw [dif_neg (by simp [hx0])]
          · set y := (restrict₀_surjective (.ofClass hv.v) γ).choose with hy_def
            have hy := (restrict₀_surjective (.ofClass hv.v) γ).choose_spec
            apply_fun embedding at hy
            simp only [← hy_def, embedding_restrict₀, coe_ofClass] at hy
            simp only [coe_ofClass, extensionValuation_toFun, valueGroup₀_equiv_extensionValuation,
              valueGroup₀_hom_extensionValuation, MulEquiv.ofBijective_apply, coe_mk,
              ZeroHom.coe_mk]
            rw [Valuation.restrict_def, restrict₀_apply, ← hy_def, dif_neg]
            · simp only [coe_ofClass, extensionValuation_toFun, extension_extends,
              Valuation.embedding_restrict, WithZero.coe_lt_coe, Subtype.mk_lt_mk,
              ← Units.val_lt_val, Units.val_mk0]
              convert embedding_strictMono (f := (.ofClass hv.v)).lt_iff_lt
            · simp only [coe_ofClass, extensionValuation_apply_coe, map_eq_zero, ← ne_eq]
              apply_fun v
              simp [hy]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R[X]
⊢ ↑φ = ↑0 ↔ φ = 0

Tactic:
coe_inj

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ : R[X]
⊢ φ = 0 ↔ φ = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R[X]
⊢ ↑φ = ↑1 ↔ φ = 1

Tactic:
coe_inj

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ : R[X]
⊢ φ = 1 ↔ φ = 1
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff (k i)) f = constantCoeff f
hs'' : ∀ i ∈ s, k i = 0
i : ℕ
⊢ i < n → (i < n → ¬k i = 0) → 1 ≤ degree (k i)

Tactic:
hi

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff (k i)) f = constantCoeff f
hs'' : ∀ i ∈ s, k i = 0
i : ℕ
hi : i < n
⊢ (i < n → ¬k i = 0) → 1 ≤ degree (k i)
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case top
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ⊤ → (coeff d) f = 0
d : σ →₀ ℕ
⊢ (coeff d) f = (coeff d) 0

Tactic:
exact h d (ENat.natCast_lt_top _)

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
φ : MvPolynomial σ R
⊢ ↑φ = ↑0 ↔ φ = 0

Tactic:
coe_inj

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
φ : MvPolynomial σ R
⊢ φ = 0 ↔ φ = 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
φ : MvPolynomial σ R
⊢ ↑φ = ↑1 ↔ φ = 1

Tactic:
coe_inj

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
φ : MvPolynomial σ R
⊢ φ = 1 ↔ φ = 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 : ℕ
⊢ weightedOrder w f = ↑n ↔
    (∃ d, (coeff d) f ≠ 0 ∧ (weight w) d = n) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff d) f = 0

Tactic:
by
  constructor
  · intro h
    obtain ⟨d, hd⟩ := f.exists_coeff_ne_zero_and_weightedOrder w (by simp only [h, toNat_natCast])
    exact ⟨⟨d, by simpa [h, Nat.cast_inj, ne_eq] using hd⟩,
      fun e he ↦ f.coeff_eq_zero_of_lt_weightedOrder w (by simp only [h, Nat.cast_lt, he])⟩
  · rintro ⟨⟨d, hd', hd⟩, h⟩
    exact le_antisymm (hd.symm ▸ f.weightedOrder_le w hd') (nat_le_weightedOrder w h)

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

Goal state before:
pp: 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 = γ

Tactic:
· exact ⟨a, by simp [ha]⟩

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

Goal state before:
pp: case inr
a : ℕ∞
ha : 0 < a
⊢ ContinuousAt (Function.uncurry fun x1 x2 ↦ x1 * x2) (a, ⊤)

Tactic:
simp only [ContinuousAt, Function.uncurry, mul_top ha.ne']

Goal state after:
case inr
a : ℕ∞
ha : 0 < a
⊢ Tendsto (Function.uncurry fun x1 x2 ↦ x1 * x2) (𝓝 (a, ⊤)) (𝓝 ⊤)
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
n : ℕ
hf : constantCoeff f = 0
⊢ ↑n ≤ (f ^ n).order

Tactic:
refine .trans ?_ (le_order_pow n)
  simpa using le_mul_of_one_le_right' (one_le_order_iff_constCoeff_eq_zero.mpr hf)

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g q
d : σ →₀ ℕ
hd : ¬(weight w) d = p + q
⊢ (coeff d) (f * g) = 0

Tactic:
rw [coeff_mul]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g q
d : σ →₀ ℕ
hd : ¬(weight w) d = p + q
⊢ ∑ p ∈ Finset.antidiagonal d, (coeff p.1) f * (coeff p.2) g = 0
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 : ℕ
⊢ i ≥ n → a ^ i = 0

Tactic:
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.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
n : (WithZero (Multiplicative ℤ))ˣ
x✝ : ∃ a, ¬Valued.v a = 0 ∧ ∃ x, Valued.v a * ↑n = Valued.v x
a : adicCompletion K v
ha0 : ¬Valued.v a = 0
x : adicCompletion K v
hx : Valued.v a * ↑n = Valued.v x
b : K
hb : (valuation K v) b = Valued.v a
y : K
hy : (valuation K v) y = Valued.v x
⊢ ¬(valuation K v) b = 0

Tactic:
rw [hb]; exact ha0

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:
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:
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.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
b : ℝ≥0
hb : 1 < b
r : R
x : K
x✝ : R
⊢ ↑(v.intAdicAbvDef hb x✝) = 0 ↔ x✝ = 0

Tactic:
by simp [intAdicAbvDef, intValuation_def]

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
b : ℝ≥0
hb : 1 < b
r : R
⊢ (v.intAdicAbv hb) r ≤ 1

Tactic:
by
  simpa [intAdicAbv, intAdicAbvDef, toNNReal_le_one_iff hb] using intValuation_le_one v r

Goal state after:
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:
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:
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.Order

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

Tactic:
rw [coeff_mul]

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : ↑n < ψ.order
⊢ ∑ p ∈ antidiagonal n, (coeff p.1) φ * (coeff p.2) ψ = ∑ p ∈ antidiagonal n, 0
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⟧
u : Filter ι
g : R⟦X⟧
⊢ Tendsto f u (𝓝 g) ↔ ∀ (d : ℕ), Tendsto (fun i ↦ (coeff d) (f i)) u (𝓝 ((coeff d) g))

Tactic:
rw [MvPowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto]
  apply (Finsupp.uniqueLinearEquiv ℕ ℕ ()).toEquiv.forall_congr
  intro d
  simp only [LinearEquiv.coe_toEquiv, Finsupp.uniqueLinearEquiv_apply, coeff]
  apply iff_of_eq
  congr
  · ext _; congr; ext; simp
  · ext; simp

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

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
⊢ φ.order = emultiplicity X φ

Tactic:
by
  classical
  rcases eq_or_ne φ 0 with (rfl | hφ)
  · simp
  cases ho : order φ with
  | top => simp [hφ] at ho
  | coe n =>
    have hn : φ.order.toNat = n := by simp [ho]
    rw [← hn, eq_comm]
    apply le_antisymm _
    · apply le_emultiplicity_of_pow_dvd
      apply X_pow_order_dvd
    · apply Order.le_of_lt_add_one
      rw [← not_le, ← Nat.cast_one, ← Nat.cast_add, ← pow_dvd_iff_le_emultiplicity]
      rintro ⟨ψ, H⟩
      have := congr_arg (coeff n) H
      rw [X_pow_mul, coeff_mul_of_lt_order, ← hn] at this
      · exact coeff_order hφ this
      · rw [X_pow_eq, order_monomial]
        split_ifs
        · simp
        · rw [← hn, ENat.natCast_lt_natCast]
          simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Ring R
Jd : TwoSidedIdeal R × (σ →₀ ℕ)
f g : MvPowerSeries σ R
hg : g ∈ {f | ∀ e ≤ Jd.2, (coeff e) f ∈ Jd.1}
e : σ →₀ ℕ
he : e ≤ Jd.2
⊢ (coeff e) (f * g) ∈ Jd.1

Tactic:
rw [coeff_mul]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Ring R
Jd : TwoSidedIdeal R × (σ →₀ ℕ)
f g : MvPowerSeries σ R
hg : g ∈ {f | ∀ e ≤ Jd.2, (coeff e) f ∈ Jd.1}
e : σ →₀ ℕ
he : e ≤ Jd.2
⊢ ∑ p ∈ Finset.antidiagonal e, (coeff p.1) f * (coeff p.2) g ∈ Jd.1
Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Ring R
Jd : TwoSidedIdeal R × (σ →₀ ℕ)
f g : MvPowerSeries σ R
hf : f ∈ {f | ∀ e ≤ Jd.2, (coeff e) f ∈ Jd.1}
e : σ →₀ ℕ
he : e ≤ Jd.2
⊢ (coeff e) (f * g) ∈ Jd.1

Tactic:
rw [coeff_mul]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Ring R
Jd : TwoSidedIdeal R × (σ →₀ ℕ)
f g : MvPowerSeries σ R
hf : f ∈ {f | ∀ e ≤ Jd.2, (coeff e) f ∈ Jd.1}
e : σ →₀ ℕ
he : e ≤ Jd.2
⊢ ∑ p ∈ Finset.antidiagonal e, (coeff p.1) f * (coeff p.2) g ∈ Jd.1
Module: Mathlib.SetTheory.Cardinal.Continuum

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

Tactic:
← succ_aleph0

Goal state after:
⊢ Order.succ ℵ₀ ≤ 𝔠
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f g : ℕ → Bool
hn : ∀ k < n, f k = g k
fn : f n = false
gn : g n = true
⊢ c < 1

Tactic:
apply h2.trans

Goal state after:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f g : ℕ → Bool
hn : ∀ k < n, f k = g k
fn : f n = false
gn : g n = true
⊢ 1 / 2 < 1
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f g : ℕ → Bool
hn : ∀ k < n, f k = g k
fn : f n = false
gn : g n = true
⊢ 1 / 2 < 1

Tactic:
norm_num

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

Goal state before:
pp: c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n ↦ rec false (fun x x_1 ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n ↦ rec true (fun x x_1 ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
⊢ 1 = 1 / 2 + 1 / 2

Tactic:
norm_num

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

Goal state before:
pp: case a.convert_3
⊢ 1 / 3 < 1 / 2

Tactic:
norm_num

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

Goal state before:
pp: case neg
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
a b : ℕ
hab : (a, b) ∈ (q ^ k).divisorsAntidiagonal
h :
  (a, b) ∉
    Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k)
ha : ∃ i, q ^ i = a
hb : ¬∃ j, q ^ j = b
⊢ 0 (a, b).2 * Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (a, b).1 = 0

pp: case neg.hb
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
a b : ℕ
hab : (a, b) ∈ (q ^ k).divisorsAntidiagonal
h :
  (a, b) ∉
    Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k)
ha : ∃ i, q ^ i = a
hb : ¬∃ j, q ^ j = b
⊢ ¬∃ a_1, q ^ a_1 = (a, b).2

Tactic:
Pi.zero_apply,

Goal state after:
case neg
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
a b : ℕ
hab : (a, b) ∈ (q ^ k).divisorsAntidiagonal
h :
  (a, b) ∉
    Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k)
ha : ∃ i, q ^ i = a
hb : ¬∃ j, q ^ j = b
⊢ 0 * Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (a, b).1 = 0

case neg.hb
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
a b : ℕ
hab : (a, b) ∈ (q ^ k).divisorsAntidiagonal
h :
  (a, b) ∉
    Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k)
ha : ∃ i, q ^ i = a
hb : ¬∃ j, q ^ j = b
⊢ ¬∃ a_1, q ^ a_1 = (a, b).2
Module: Mathlib.LinearAlgebra.Complex.FiniteDimensional

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

Tactic:
refine (Free.rank_eq_mk_of_infinite_lt ℚ ℝ ?_).trans mk_real

Goal state after:
⊢ lift.{0, 0} #ℚ < lift.{0, 0} #ℝ
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case neg
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
a b : ℕ
hab : (a, b) ∈ (q ^ k).divisorsAntidiagonal
h :
  (a, b) ∉
    Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k)
ha : ¬∃ i, q ^ i = a
⊢ 0 (a, b).1 * Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (a, b).2 = 0

pp: case neg.hb
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
a b : ℕ
hab : (a, b) ∈ (q ^ k).divisorsAntidiagonal
h :
  (a, b) ∉
    Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k)
ha : ¬∃ i, q ^ i = a
⊢ ¬∃ a_1, q ^ a_1 = (a, b).1

Tactic:
Pi.zero_apply,

Goal state after:
case neg
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
a b : ℕ
hab : (a, b) ∈ (q ^ k).divisorsAntidiagonal
h :
  (a, b) ∉
    Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k)
ha : ¬∃ i, q ^ i = a
⊢ 0 * Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (a, b).2 = 0

case neg.hb
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
a b : ℕ
hab : (a, b) ∈ (q ^ k).divisorsAntidiagonal
h :
  (a, b) ∉
    Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k)
ha : ¬∃ i, q ^ i = a
⊢ ¬∃ a_1, q ^ a_1 = (a, b).1
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

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

Tactic:
Pi.zero_apply,

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
⊢ 0 =
    ∑ x ∈ n.divisorsAntidiagonal,
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 x.1 *
        Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 x.2
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:
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 : ‖f n‖ / ↑n ^ s.re ≤ ∑' (i : ℕ), ‖term f s i‖
⊢ False

Tactic:
div_le_iff₀ <| Real.rpow_pos_of_pos (Nat.cast_pos.mpr <| Nat.pos_of_ne_zero hn₀) _

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.ArithmeticFunction.LFunction

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
a b : ℕ
hk : (a, b) ∈ n.divisorsAntidiagonal
hab : (a, b).1 * (a, b).2 = n
ha : ∃ i, q ^ i = a
hb : ¬∃ j, q ^ j = b
⊢ 0 (a, b).2 * Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (a, b).1 = 0

pp: case neg.hb
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
a b : ℕ
hk : (a, b) ∈ n.divisorsAntidiagonal
hab : (a, b).1 * (a, b).2 = n
ha : ∃ i, q ^ i = a
hb : ¬∃ j, q ^ j = b
⊢ ¬∃ a_1, q ^ a_1 = (a, b).2

Tactic:
Pi.zero_apply,

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
a b : ℕ
hk : (a, b) ∈ n.divisorsAntidiagonal
hab : (a, b).1 * (a, b).2 = n
ha : ∃ i, q ^ i = a
hb : ¬∃ j, q ^ j = b
⊢ 0 * Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (a, b).1 = 0

case neg.hb
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
a b : ℕ
hk : (a, b) ∈ n.divisorsAntidiagonal
hab : (a, b).1 * (a, b).2 = n
ha : ∃ i, q ^ i = a
hb : ¬∃ j, q ^ j = b
⊢ ¬∃ a_1, q ^ a_1 = (a, b).2
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

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

pp: case neg.hb
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
a b : ℕ
hk : (a, b) ∈ n.divisorsAntidiagonal
hab : (a, b).1 * (a, b).2 = n
ha : ¬∃ i, q ^ i = a
⊢ ¬∃ a_1, q ^ a_1 = (a, b).1

Tactic:
Pi.zero_apply,

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
a b : ℕ
hk : (a, b) ∈ n.divisorsAntidiagonal
hab : (a, b).1 * (a, b).2 = n
ha : ¬∃ i, q ^ i = a
⊢ 0 * Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (a, b).2 = 0

case neg.hb
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
a b : ℕ
hk : (a, b) ∈ n.divisorsAntidiagonal
hab : (a, b).1 * (a, b).2 = n
ha : ¬∃ i, q ^ i = a
⊢ ¬∃ a_1, q ^ a_1 = (a, b).1
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : ¬1 < q
⊢ ((algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff (f + g))) n =
    ((algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff f) +
        (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff g))
      n

Tactic:
by_cases hn : n = 1 <;> simp [hn]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
x : R
n : ℕ
hq : 1 < q
hn : ¬∃ k, q ^ k = n
⊢ 0 n = (x • 1) n

Tactic:
Pi.zero_apply,

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
x : R
n : ℕ
hq : 1 < q
hn : ¬∃ k, q ^ k = n
⊢ 0 = (x • 1) n