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

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : Semiring R
inst✝² : ValuativeRel R
inst✝¹ : IsDiscrete R
inst✝ : IsNontrivial R
a : ValueGroupWithZero R
ha : 0 < a
⊢ a⁻¹ ≤ uniformizer R ↔ 1 < a

Tactic:
le_uniformizer_iff,

Goal state after:
case neg
R : Type u_1
inst✝³ : Semiring R
inst✝² : ValuativeRel R
inst✝¹ : IsDiscrete R
inst✝ : IsNontrivial R
a : ValueGroupWithZero R
ha : 0 < a
⊢ a⁻¹ < 1 ↔ 1 < a
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ -W'.negAddY P P - W'.a₁ * W'.addX P P * addZ P P - W'.a₃ * addZ P P ^ 3 = 0

Tactic:
addX_self hP,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ -W'.negAddY P P - W'.a₁ * 0 * addZ P P - W'.a₃ * addZ P P ^ 3 = 0
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : v ↑r ≠ 0
vr : Γˣ := Units.mk0 (v ↑r) hr₀
hvr_def : vr = Units.mk0 (v ↑r) hr₀
hvr : vr ∈ (MonoidWithZeroHom.ofClass v).valueGroup
⊢ ∃ n u, ↑r = ↑(π.val ^ n) * ↑↑u

Tactic:
π.2.zpowers_eq_valueGroup,

Goal state after:
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : v ↑r ≠ 0
vr : Γˣ := Units.mk0 (v ↑r) hr₀
hvr_def : vr = Units.mk0 (v ↑r) hr₀
hvr : vr ∈ zpowers (Units.mk0 (v ↑π.val) ⋯)
⊢ ∃ n u, ↑r = ↑(π.val ^ n) * ↑↑u
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ ![W'.addX P P, W'.addY P P, addZ P P] = ![0, 0, 0]

Tactic:
addX_self hP,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ ![0, W'.addY P P, addZ P P] = ![0, 0, 0]
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ofClass Valued.v).ValueGroup₀ˣ
r s : WithVal v
hr₀ : 0 < Valued.v r
hs₀ : 0 < Valued.v s
hr : Valued.v.restrict r / Valued.v.restrict s = ↑γ
h' : w.restrict.IsEquiv v.restrict
⊢ Valued.v.restrict ((equiv v) r) / Valued.v.restrict ((equiv v) s) ≠ 0

Tactic:
simp only [equiv_apply, restrict_def, ne_eq, div_eq_zero_iff, restrict₀_eq_zero_iff, hv,
      MonoidWithZeroHom.coe_ofClass, not_or, (eq_zero h (r := r.ofVal)).ne,
      (eq_zero h (r := s.ofVal)).ne]

Goal state after:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ofClass Valued.v).ValueGroup₀ˣ
r s : WithVal v
hr₀ : 0 < Valued.v r
hs₀ : 0 < Valued.v s
hr : Valued.v.restrict r / Valued.v.restrict s = ↑γ
h' : w.restrict.IsEquiv v.restrict
⊢ ¬v r.ofVal = 0 ∧ ¬v s.ofVal = 0
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
h : v.IsEquiv w
h_val : Valued.v.IsEquiv Valued.v
h_res : v.restrict.IsEquiv w.restrict
x : (ofClass Valued.v).ValueGroup₀ˣ
u : ↥(ofClass Valued.v).valueGroup := WithZero.unzero ⋯
⊢ ∃ ia, ∀ x_1 ∈ {x | Valued.v.restrict x < ↑ia}, (RingHom.id R) x_1 ∈ {x_2 | Valued.v.restrict x_2 < ↑x}

Tactic:
obtain ⟨a, ha, y, hu⟩ := (mem_valueGroup_iff_of_comm _).mp u.2

Goal state after:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
h : v.IsEquiv w
h_val : Valued.v.IsEquiv Valued.v
h_res : v.restrict.IsEquiv w.restrict
x : (ofClass Valued.v).ValueGroup₀ˣ
u : ↥(ofClass Valued.v).valueGroup := WithZero.unzero ⋯
a : R
ha : (ofClass Valued.v) a ≠ 0
y : R
hu : (ofClass Valued.v) a * ↑↑u = (ofClass Valued.v) y
⊢ ∃ ia, ∀ x_1 ∈ {x | Valued.v.restrict x < ↑ia}, (RingHom.id R) x_1 ∈ {x_2 | Valued.v.restrict x_2 < ↑x}
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
hyp : v.restrict x < ↑γ₀
⊢ False

Tactic:
have : x ∈ U ∩ M := ⟨hU hyp, xM⟩

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
hyp : v.restrict x < ↑γ₀
this : x ∈ U ∩ M
⊢ False
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case mpr.inr
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a b : G
h : b = |a|ₘ ∧ 1 < b
this : ∀ {a : G}, b = |a|ₘ ∧ 1 < b → 1 ≤ a → IsLeast {y | y ∈ closure {a} ∧ 1 < y} b
ha : ¬1 ≤ a
⊢ IsLeast {y | y ∈ closure {a} ∧ 1 < y} b

pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
b a : G
h : b = |a|ₘ ∧ 1 < b
ha : 1 ≤ a
⊢ IsLeast {y | y ∈ closure {a} ∧ 1 < y} b

Tactic:
· convert! @this (a⁻¹) ?_ (by simpa using le_of_not_ge ha) using 4
      · simp
      · rwa [mabs_inv]

Goal state after:
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
b a : G
h : b = |a|ₘ ∧ 1 < b
ha : 1 ≤ a
⊢ IsLeast {y | y ∈ closure {a} ∧ 1 < y} b
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_1
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : G ≃*o WithZero (Multiplicative ℤ)
⊢ Gˣ ≃*o Multiplicative ℤ

Tactic:
refine ⟨MulEquiv.withZero.symm (withZeroUnitsEquiv.trans f), ?_⟩
    intros
    simp only [MulEquiv.withZero, withZeroUnitsEquiv, MulEquiv.trans_apply,
      MulEquiv.coe_mk, Equiv.coe_fn_mk, recZeroCoe_coe, OrderMonoidIso.coe_mulEquiv,
      MulEquiv.symm_trans_apply, MulEquiv.symm_mk, Equiv.coe_fn_symm_mk, map_eq_zero, coe_ne_zero,
      ↓reduceDIte, unzero_coe, MulEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe]
    rw [← Units.val_le_val, ← map_le_map_iff f, ← coe_le_coe, coe_unzero, coe_unzero]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_1
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
h : ({x | g ≤ x} \ {0}).WellFoundedOn fun x1 x2 ↦ x1 < x2
x✝ : G₀ˣ
⊢ x✝ ∈ {x | Units.mk0 g hg ≤ x} → ↑x✝ ∈ {x | g ≤ x} \ {0}

Tactic:
simp [← Units.val_le_val]

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : ¬n ≤ k
h₂ : k = m + n
⊢ 0 = a * b

Tactic:
h₂

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : ¬n ≤ m + n
h₂ : k = m + n
⊢ 0 = a * b
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
⊢ v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)

Tactic:
rw [v.intValuationDef_if_neg hxy, v.intValuationDef_if_neg hx, v.intValuationDef_if_neg hy,
          le_max_iff]

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
⊢ exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x + y})).factors)) ≤
      exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)) ∨
    exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x + y})).factors)) ≤
      exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors))
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
hv : ¬v.intValuation r = 0
⊢ exp (-↑n) ≤ v.intValuation r ↔ exp (-↑n) < v.intValuation r * exp 1

Tactic:
rw [lt_mul_exp_iff_le hv]

Goal state after:
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
r : R
⊢ (algebraMap R (MvPowerSeries σ A)) r = C ((algebraMap R A) r)

Tactic:
change (MvPowerSeries.map (algebraMap R A)).comp C r = _

Goal state after:
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
⊢ ((map (algebraMap R A)).comp C) r = C ((algebraMap R A) r)
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
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 + (coeff d) g ≠ 0

Tactic:
coeff_eq_zero_of_lt_weightedOrder w 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 + 0 ≠ 0
Module: Mathlib.Data.Finsupp.Interval

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : Lattice α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f g : ι →₀ α
⊢ #(uIcc f g) = ∏ i ∈ f.support ∪ g.support, #(uIcc (f i) (g i))

Tactic:
← support_inf_union_support_sup

Goal state after:
ι : Type u_1
α : Type u_2
inst✝² : Lattice α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f g : ι →₀ α
⊢ #(uIcc f g) = ∏ i ∈ (f ⊓ g).support ∪ (f ⊔ g).support, #(uIcc (f i) (g i))
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
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = d
hp : (weight w) x.1 = p
hq : (weight w) x.2 = q
⊢ False

Tactic:
apply hd

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
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = d
hp : (weight w) x.1 = p
hq : (weight w) x.2 = q
⊢ (weight w) d = p + q
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
f : MvPowerSeries σ R
⊢ Tendsto (fun d ↦ ↑((trunc' R d) f)) atTop (𝓝 f)

Tactic:
rw [tendsto_iff_coeff_tendsto]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
f : MvPowerSeries σ R
⊢ ∀ (d : σ →₀ ℕ), Tendsto (fun i ↦ (coeff d) ↑((trunc' R i) f)) atTop (𝓝 ((coeff d) f))
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
⊢ Tendsto (fun d ↦ ↑((trunc R d) f)) atTop (𝓝 f)

Tactic:
rw [tendsto_iff_coeff_tendsto]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace R
inst✝² : DecidableEq σ
inst✝¹ : CommSemiring R
inst✝ : Nonempty σ
f : MvPowerSeries σ R
⊢ ∀ (d : σ →₀ ℕ), Tendsto (fun i ↦ (coeff d) ↑((trunc R i) f)) atTop (𝓝 ((coeff d) f))
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
⊢ Valued.v { toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) r)) }.toCompletion ≤ 1

Tactic:
rw [Valued.valuedCompletion_apply]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
⊢ Valued.v ((WithVal.equiv (valuation K v)).symm ((algebraMap R K) r)) ≤ 1
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
x y : R
⊢ (↑⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) (x * y))) }, ⋯⟩).toCompletion =
    (↑(⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) x)) }, ⋯⟩ *
          ⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) y)) }, ⋯⟩)).toCompletion

Tactic:
simp [map_mul, UniformSpace.Completion.coe_mul]

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
⊢ ∃ i', (↑i' ∈ 𝓝 0 ∧ (∀ (r : R), ∀ x ∈ i', r • x ∈ i') ∧ ∀ (r' : R'), ∀ x ∈ i', r' • x ∈ i') ∧ ↑i' ⊆ ↑I

Tactic:
have hRJ : uR • (J : Set M) ⊆ I := subset_trans (smul_subset_smul_left J_sub_I) hRI

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
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
⊢ ∃ i', (↑i' ∈ 𝓝 0 ∧ (∀ (r : R), ∀ x ∈ i', r • x ∈ i') ∧ ∀ (r' : R'), ∀ x ∈ i', r' • x ∈ i') ∧ ↑i' ⊆ ↑I
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : R⟦X⟧
m : ℕ
H : ¬m < n
⊢ 0 = 0 + 0

Tactic:
· rw [zero_add]

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

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

Tactic:
by
  constructor
  · intro h
    rw [← coeff_zero_eq_constantCoeff]
    apply coeff_of_lt_order
    simpa using Order.one_le_iff_pos.mp h
  · intro h
    refine le_order _ _ fun d hd ↦ ?_
    rw [Nat.cast_lt_one] at hd
    simp [hd, h]

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

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

Tactic:
rw [trunc_trunc_mul, trunc_mul_trunc]

Goal state after:
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 n.succ) (↑((trunc n.succ) ↑((trunc a) f)) * ↑((trunc n.succ) ↑((trunc b) g)))) = (coeff n) (f * g)

Tactic:
trunc_trunc_of_le f ha,

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 n.succ) f) * ↑((trunc n.succ) ↑((trunc b) g)))) = (coeff n) (f * g)
Module: Mathlib.RingTheory.PowerSeries.PiTopology

Goal state before:
pp: R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : CommSemiring R
f : R⟦X⟧
⊢ Tendsto (fun d ↦ ↑((trunc d) f)) atTop (𝓝 f)

Tactic:
rw [tendsto_iff_coeff_tendsto]

Goal state after:
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : CommSemiring R
f : R⟦X⟧
⊢ ∀ (d : ℕ), Tendsto (fun i ↦ (coeff d) ↑((trunc i) f)) atTop (𝓝 ((coeff d) f))
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:
by
      classical
      rw [coeff_mul]
      apply sum_mem
      rintro uv huv
      exact TwoSidedIdeal.mul_mem_left _ _ _
        (hg _ (le_trans (Finset.HasAntidiagonal.antidiagonal.snd_le huv) he))

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

Goal state before:
pp: ⊢ ℶ_ 1 = 𝔠

Tactic:
simpa using beth_succ 0

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

Goal state before:
pp: c : ℝ
f : ℕ → Bool
n : ℕ
h : f n = true
⊢ cantorFunctionAux c f n = c ^ n

Tactic:
simp [cantorFunctionAux, h]

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

Goal state before:
pp: c : ℝ
f : ℕ → Bool
n : ℕ
h : f n = false
⊢ cantorFunctionAux c f n = 0

Tactic:
simp [cantorFunctionAux, h]

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

Goal state before:
pp: c : ℝ
f g : ℕ → Bool
n : ℕ
h : f n = g n
⊢ cantorFunctionAux c f n = cantorFunctionAux c g n

Tactic:
simp [cantorFunctionAux, h]

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
⊢ cantorFunction c f < cantorFunction c g

Tactic:
rw [cantorFunction_succ f h1.le h3, cantorFunction_succ g h1.le h3]

Goal state after:
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 f 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)
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: x y : ℝ
h : x < y
⊢ ¬(Ioc x y).Countable

Tactic:
rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Ioc_real h, not_le]

Goal state after:
x y : ℝ
h : x < y
⊢ ℵ₀ < 𝔠
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: 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 ↦ ‖↑C‖ * ‖↑n ^ (-(s + (1 - ↑x)))‖

Tactic:
refine Summable.mul_left _ <|
      Summable.of_norm_bounded_eventually_nat (g := fun n ↦ (n : ℝ) ^ (-s.re + x - 1)) ?_ ?_

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

case refine_2
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
⊢ ∀ᶠ (i : ℕ) in Filter.atTop, ‖‖↑i ^ (-(s + (1 - ↑x)))‖‖ ≤ ↑i ^ (-s.re + x - 1)
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
τ : Type u_3
f g : MvPowerSeries τ R
hf : HasSubst f
⊢ HasSubst (f * g)

Tactic:
simp only [HasSubst, map_mul]

Goal state after:
R : Type u_2
inst✝ : CommRing R
τ : Type u_3
f g : MvPowerSeries τ R
hf : HasSubst f
⊢ IsNilpotent (MvPowerSeries.constantCoeff f * MvPowerSeries.constantCoeff g)
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
τ : Type u_3
f g : MvPowerSeries τ R
hf : HasSubst f
⊢ HasSubst (g * f)

Tactic:
simp only [HasSubst, map_mul]

Goal state after:
R : Type u_2
inst✝ : CommRing R
τ : Type u_3
f g : MvPowerSeries τ R
hf : HasSubst f
⊢ IsNilpotent (MvPowerSeries.constantCoeff g * MvPowerSeries.constantCoeff 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
ha : HasSubst a
f g : R⟦X⟧
⊢ subst a (f + g) = subst a f + subst a g

Tactic:
by
  rw [← coe_substAlgHom ha, map_add]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : PowerSeries R
hf : PowerSeries.constantCoeff f = 1
m n : ℕ
hmn : m.Coprime n
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ ((ofPowerSeries p) (PowerSeries.subst (PowerSeries.X ^ k) f)) (m * n) =
    ((ofPowerSeries p) (PowerSeries.subst (PowerSeries.X ^ k) f)) m *
      ((ofPowerSeries p) (PowerSeries.subst (PowerSeries.X ^ k) f)) n

Tactic:
by_cases hm : ∃ i, p ^ i = m

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
f : PowerSeries R
hf : PowerSeries.constantCoeff f = 1
m n : ℕ
hmn : m.Coprime n
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hm : ∃ i, p ^ i = m
⊢ ((ofPowerSeries p) (PowerSeries.subst (PowerSeries.X ^ k) f)) (m * n) =
    ((ofPowerSeries p) (PowerSeries.subst (PowerSeries.X ^ k) f)) m *
      ((ofPowerSeries p) (PowerSeries.subst (PowerSeries.X ^ k) f)) n

case neg
R : Type u_1
inst✝ : CommRing R
f : PowerSeries R
hf : PowerSeries.constantCoeff f = 1
m n : ℕ
hmn : m.Coprime n
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hm : ¬∃ i, p ^ i = m
⊢ ((ofPowerSeries p) (PowerSeries.subst (PowerSeries.X ^ k) f)) (m * n) =
    ((ofPowerSeries p) (PowerSeries.subst (PowerSeries.X ^ k) f)) m *
      ((ofPowerSeries p) (PowerSeries.subst (PowerSeries.X ^ k) f)) n
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
a : σ → R
f : MvPowerSeries σ R
n b : σ →₀ ℕ
hb : b ∈ ⋯.toFinset
hbn : b ≠ n
⊢ ((coeff b) f * if n = b then b.prod fun s n ↦ a s ^ n else 0) = 0

Tactic:
if_neg (Ne.symm hbn),

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
a : σ → R
f : MvPowerSeries σ R
n b : σ →₀ ℕ
hb : b ∈ ⋯.toFinset
hbn : b ≠ n
⊢ (coeff b) f * 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
x : E
⊢ ‖x‖ₑ ≤ egauge 𝕜 (closedBall 0 1) x

Tactic:
by
  simpa using div_le_egauge_closedBall 𝕜 1 x

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Congr

Goal state before:
pp: case inr
𝕜 : 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
inst✝ : T1Space E
y : E
h : s =ᶠ[𝓝[{y}ᶜ] x] t
hne : x ≠ y
⊢ HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x

Tactic:
rw [hne.nhdsWithin_compl_singleton] at h
    exact hasFDerivWithinAt_congr_set h

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : Filter α
inst✝ : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
h : g =o[𝕜; l] f
⊢ Tendsto (fun x ↦ (f x)⁻¹ • g x) l (𝓝 0)

Tactic:
by
  rw [← isLittleOTVS_one (𝕜 := 𝕜), isLittleOTVS_iff]
  intro U hU
  rcases (h.smul_left f⁻¹).1 U hU with ⟨V, hV₀, hV⟩
  refine ⟨V, hV₀, fun ε hε ↦ (hV ε hε).mono fun x hx ↦ hx.trans ?_⟩
  by_cases hx₀ : f x = 0 <;> simp [hx₀, egauge_zero_right _ (Filter.nonempty_of_mem hV₀)]

Goal state after: