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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = span {x}
y : R
hy : Submodule.colon I ↑(span {a}) = span {y}
⊢ (I ⊔ span {a}) * span {y} ≤ I

Tactic:
Ideal.sup_mul,

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = span {x}
y : R
hy : Submodule.colon I ↑(span {a}) = span {y}
⊢ I * span {y} ⊔ span {a} * span {y} ≤ I
Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
H : ∀ (P : Ideal R), P.IsPrime → Submodule.IsPrincipal P
I : Ideal R
hI : ¬Submodule.IsPrincipal I
⊢ ¬IsPrincipalIdealRing R

Tactic:
isPrincipalIdealRing_iff,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
H : ∀ (P : Ideal R), P.IsPrime → Submodule.IsPrincipal P
I : Ideal R
hI : ¬Submodule.IsPrincipal I
⊢ ¬∀ (S : Ideal R), Submodule.IsPrincipal S
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Jacobian R
f : R →+* S
P Q : Fin 3 → R
⊢ (W'.map f).addY (⇑f ∘ P) (⇑f ∘ Q) = f (W'.addY P Q)

Tactic:
simp only [addY, negY_eq, map_negAddY, map_addX, map_addZ]

Goal state after:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Jacobian R
f : R →+* S
P Q : Fin 3 → R
⊢ -f (W'.negAddY P Q) - (W'.map f).a₁ * f (W'.addX P Q) * f (addZ P Q) - (W'.map f).a₃ * f (addZ P Q) ^ 3 =
    f (-W'.negAddY P Q - W'.a₁ * W'.addX P Q * addZ P Q - W'.a₃ * addZ P Q ^ 3)
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: case h
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
x : R
hx : Valued.v.restrict x < Valued.v.restrict r.ofVal / Valued.v.restrict s.ofVal
⊢ Valued.v.restrict (toVal v x) < ↑γ

Tactic:
lt_div_iff₀,

Goal state after:
case h
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
x : R
hx : Valued.v.restrict x * Valued.v.restrict s.ofVal < Valued.v.restrict r.ofVal
⊢ Valued.v.restrict (toVal v x) < ↑γ

case h
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
x : R
hx : Valued.v.restrict x < Valued.v.restrict r.ofVal / Valued.v.restrict s.ofVal
⊢ 0 < Valued.v.restrict s.ofVal
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G✝ : Type u_1
inst✝⁷ : CommGroup G✝
inst✝⁶ : LinearOrder G✝
inst✝⁵ : IsOrderedMonoid G✝
inst✝⁴ : MulArchimedean G✝
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
x : G
h : IsLeast {y | 0 < y} x
this : ⊤ = AddSubgroup.closure {x}
e : G ≃+o ↥⊤ := { toAddEquiv := AddSubsemigroup.topEquiv.symm, map_le_map_iff' := ⋯ }
⊢ G ≃+o ℤ

Tactic:
let e' : (⊤ : AddSubgroup G) ≃+o AddSubgroup.closure {x} :=
    ⟨AddEquiv.subsemigroupCongr (by simp [this]),
     (AddEquiv.strictMono_subsemigroupCongr _).le_iff_le⟩

Goal state after:
G✝ : Type u_1
inst✝⁷ : CommGroup G✝
inst✝⁶ : LinearOrder G✝
inst✝⁵ : IsOrderedMonoid G✝
inst✝⁴ : MulArchimedean G✝
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
x : G
h : IsLeast {y | 0 < y} x
this : ⊤ = AddSubgroup.closure {x}
e : G ≃+o ↥⊤ := { toAddEquiv := AddSubsemigroup.topEquiv.symm, map_le_map_iff' := ⋯ }
e' : ↥⊤ ≃+o ↥(AddSubgroup.closure {x}) := { toAddEquiv := AddEquiv.subsemigroupCongr ⋯, map_le_map_iff' := ⋯ }
⊢ G ≃+o ℤ
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case pos.inr.refine_1
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
y : G
hy : y ≠ 0
this : ∀ (y : G), y ≠ 0 → 0 < y → False
hy' : y ≤ 0
⊢ -y ≠ 0

pp: case pos.inr.refine_2
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
y : G
hy : y ≠ 0
this : ∀ (y : G), y ≠ 0 → 0 < y → False
hy' : y ≤ 0
⊢ 0 < -y

Tactic:
· simp [hy]

Goal state after:
case pos.inr.refine_2
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
y : G
hy : y ≠ 0
this : ∀ (y : G), y ≠ 0 → 0 < y → False
hy' : y ≤ 0
⊢ 0 < -y
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 Γ₀
a b : (ofClass v).ValueGroup₀
x : K := ⋯.choose
hx_def : x = ⋯.choose
hx : (restrict₀ (ofClass v)) ⋯.choose = a
y : K := ⋯.choose
hy_def : y = ⋯.choose
hy : (restrict₀ (ofClass v)) ⋯.choose = b
⊢ extensionValuation.restrict ↑⋯.choose = extensionValuation.restrict ↑x * extensionValuation.restrict ↑y

Tactic:
set xy := (restrict₀_surjective (.ofClass hv.v) (a * b)).choose with hxy_def

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
x : K := ⋯.choose
hx_def : x = ⋯.choose
hx : (restrict₀ (ofClass v)) ⋯.choose = a
y : K := ⋯.choose
hy_def : y = ⋯.choose
hy : (restrict₀ (ofClass v)) ⋯.choose = b
xy : K := ⋯.choose
hxy_def : xy = ⋯.choose
⊢ extensionValuation.restrict ↑xy = extensionValuation.restrict ↑x * extensionValuation.restrict ↑y
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case succ
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
ih : X s ^ n = (monomial (single s n)) 1
⊢ X s ^ (n + 1) = (monomial (single s (n + 1))) 1

Tactic:
| succ n ih =>

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

Goal state before:
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.symm.toMonoidHom γ

Goal state after:
case h
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝ : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x✝ : ∃ γ, {x | extensionValuation.restrict x < ↑γ} ⊆ s
γ : (ofClass extensionValuation).ValueGroup₀ˣ
h : {x | extensionValuation.restrict x < ↑γ} ⊆ s
⊢ {x | embedding (extension x) < embedding ↑((Units.map valueGroup₀_equiv_extensionValuation.symm.toMonoidHom) γ)} ⊆ s
Module: Mathlib.RingTheory.MvPowerSeries.Basic

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

Tactic:
simp only [← coe_X, ← coe_pow, ← coe_monomial, monomial_eq, map_one, one_mul]
  simp only [← coeToMvPowerSeries.ringHom_apply, ← map_finsuppProd]

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

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
H : ∃ x, v x = γ
⊢ IsClosed {a | v a = γ → ∃ a, v a = γ}

pp: case neg
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
H : ¬∃ x, v x = γ
⊢ IsClosed {a | v a = γ → ∃ a, v a = γ}

Tactic:
· simp [H]

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
H : ¬∃ x, v x = γ
⊢ IsClosed {a | v a = γ → ∃ a, v a = γ}
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: n : ℕ
⊢ 𝓝 ↑n = pure ↑n

Tactic:
by
  simp [← isOpenEmbedding_natCast.map_nhds_eq]

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 : adicCompletion K v
⊢ embedding ((valueGroupOrderIso K v) ((valuation K v).restrict x)) = embedding (Valued.v.restrict x.toCompletion)

Tactic:
rw [embedding_valueGroupOrderIso, embedding_restrict, embedding_restrict]

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
x : adicCompletion K v
⊢ (valuation K v) x = Valued.v x.toCompletion
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
n m : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPowerSeries σ R
⊢ (truncTotal n) (p ^ m) = (truncTotal n) (↑((truncTotal n) p) ^ m)

Tactic:
ext d
  by_cases hd : d.degree < n
  · simp_rw [coeff_truncTotal _ hd]
    exact_mod_cast (coeff_truncTotal_pow _ hd).symm
  simp_rw [coeff_truncTotal_eq_zero _ (not_lt.mp hd)]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
p : ℕ
hf : f.IsHomogeneous p
d : σ →₀ ℕ
hd : degree d ≠ p
⊢ (weight 1) d ≠ p

Tactic:
rwa [degree_eq_weight_one] at hd

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
⊢ Valued.v ↑r = (valuation K v) ↑r

Tactic:
rw [← adicCompletion.valued_toCompletion]
  exact Valued.valuedCompletion_apply _

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
k : K
⊢ Valued.v { toCompletion := ↑((WithVal.equiv (valuation K v)).symm k) } = (valuation K v) k

Tactic:
rw [← adicCompletion.valued_toCompletion]
  exact Valued.valuedCompletion_apply _

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
ih : n • φ.order ≤ (φ ^ n).order
⊢ (φ ^ n).order + φ.order ≤ (φ ^ n * φ).order

Tactic:
le_order_mul

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
ih : n • φ.order ≤ (φ ^ n).order
⊢ (φ ^ n * φ).order ≤ (φ ^ n * φ).order
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
ih : n • φ.order ≤ (φ ^ n).order
⊢ (n + 1) • φ.order ≤ (φ ^ (n + 1)).order

Tactic:
| succ n ih =>

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

Goal state before:
pp: case cons
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
φ : ι → R⟦X⟧
a : ι
s : Finset ι
ha : a ∉ s
ih : ∑ i ∈ s, (φ i).order ≤ (∏ i ∈ s, φ i).order
⊢ (φ a).order + (∏ i ∈ s, φ i).order ≤ (φ a * ∏ x ∈ s, φ x).order

Tactic:
le_order_mul

Goal state after:
case cons
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
φ : ι → R⟦X⟧
a : ι
s : Finset ι
ha : a ∉ s
ih : ∑ i ∈ s, (φ i).order ≤ (∏ i ∈ s, φ i).order
⊢ (φ a * ∏ i ∈ s, φ i).order ≤ (φ a * ∏ x ∈ s, φ x).order
Module: Mathlib.RingTheory.PowerSeries.Trunc

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

Tactic:
by
  induction a with
  | zero =>
    rw [pow_zero, pow_zero]
  | succ a ih =>
    rw [_root_.pow_succ', _root_.pow_succ', trunc_trunc_mul,
      ← trunc_trunc_mul_trunc, ih, trunc_trunc_mul_trunc]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
⊢ (coeff (φ.order.toNat, ψ.order.toNat).1) φ * (coeff (φ.order.toNat, ψ.order.toNat).2) ψ ≠ 0

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
⊢ ∀ b ∈ antidiagonal (φ.order.toNat + ψ.order.toNat),
    b ≠ (φ.order.toNat, ψ.order.toNat) → (coeff b.1) φ * (coeff b.2) ψ = 0

Tactic:
· exact mul_ne_zero (coeff_order h.1) (coeff_order h.2)

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
⊢ ∀ b ∈ antidiagonal (φ.order.toNat + ψ.order.toNat),
    b ≠ (φ.order.toNat, ψ.order.toNat) → (coeff b.1) φ * (coeff b.2) ψ = 0
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:
| succ n ih =>

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

Goal state before:
pp: a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x ↦ a + a - x) '' Ioi a = Iio a
⊢ #↑{a} < 𝔠

Tactic:
rw [mk_singleton]

Goal state after:
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x ↦ a + a - x) '' Ioi a = Iio a
⊢ 1 < 𝔠
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: x y : ℝ
h : y ≤ x
⊢ (Icc x y).Countable

Tactic:
by
    rcases le_iff_eq_or_lt.mp h with heq | hlt
    · simp [heq]
    · simp [hlt]

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 : MvPowerSeries σ R
i : σ →₀ ℕ
hi : ¬(coeff i) f = 0
⊢ (⨅ i, (a i).order) * f.order ≤ (Finsupp.weight ((weightedOrder fun x ↦ 1) ∘ a)) i

Tactic:
trans (⨅ (i : σ), (order ∘ a) i) * ↑i.degree

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 ≤ (⨅ i, (order ∘ a) i) * ↑(Finsupp.degree i)

σ : 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, (order ∘ a) i) * ↑(Finsupp.degree i) ≤ (Finsupp.weight ((weightedOrder fun x ↦ 1) ∘ a)) i
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (n : ℕ), ∀ᶠ (i : ι) in cofinite, (f i) n = 1 n
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
⊢ Cauchy (map (fun s ↦ ∏ b ∈ s, f b) atTop)

Tactic:
← this.cauchy_map_iff,

Goal state after:
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (n : ℕ), ∀ᶠ (i : ι) in cofinite, (f i) n = 1 n
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
⊢ Cauchy (map DFunLike.coe (map (fun s ↦ ∏ b ∈ s, f b) atTop))
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)
this : Invertible ((coeff 1) P.substInv)
Q : R⟦X⟧ := P.substInv.substInv
hQ : HasSubst Q
eq_aux : subst Q P.substInv = X
h : Q = P
⊢ subst P P.substInv = X

Tactic:
by simp_rw [← h, eq_aux]

Goal state after:
Module: Mathlib.Analysis.Calculus.TangentCone.Real

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul ℝ E
s : Set E
x : E
inst✝ : IsTopologicalAddGroup E
conv : Convex ℝ s
hx : x ∈ closure[inst✝²] s
y : E
hy : interior s ∈ 𝓝 y
z : E
zs : z ∈ interior s
⊢ (fun x_1 ↦ x_1 - x) z ∈ tangentConeAt ℝ s x

Tactic:
refine mem_tangentConeAt_of_openSegment_subset (Subset.trans ?_ interior_subset)

Goal state after:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul ℝ E
s : Set E
x : E
inst✝ : IsTopologicalAddGroup E
conv : Convex ℝ s
hx : x ∈ closure[inst✝²] s
y : E
hy : interior s ∈ 𝓝 y
z : E
zs : z ∈ interior s
⊢ openSegment ℝ x z ⊆ interior s
Module: Mathlib.Analysis.Calculus.FDeriv.Const

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
x : E
h : x ∉ tsupport f
⊢ HasStrictFDerivAt f 0 x

Tactic:
rw [notMem_tsupport_iff_eventuallyEq] at h
  exact (hasStrictFDerivAt_const (0 : F) x).congr_of_eventuallyEq h.symm

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
f : α → E
g : α → F
l : Filter α
h : f =o[𝕜; l] g
U : Set E
hU : U ∈ 𝓝 0
V : Set F
hV₀ : V ∈ 𝓝 0
hV : ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 V (g x)
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ε * egauge 𝕜 V (g x)

Tactic:
cases ε with

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : ¬DifferentiableWithinAt ℝ f (Ioi x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x

Tactic:
· rw [derivWithin_zero_of_not_differentiableWithinAt H,
      derivWithin_zero_of_not_differentiableWithinAt]
    rwa [differentiableWithinAt_Ioi_iff_Ici] at H

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
σ σ' : 𝕜 →+* 𝕜
inst✝³ : RingHomIsometric σ
inst✝² : RingHomInvPair σ σ'
F' : Type u_1
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕜 F'
L : F →SL[σ] F'
hf : HasDerivAt f f' x
⊢ HasDerivAt (⇑L ∘ f ∘ ⇑σ') (L f') (σ x)

Tactic:
have : RingHomIsometric σ' := .inv σ

Goal state after:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
σ σ' : 𝕜 →+* 𝕜
inst✝³ : RingHomIsometric σ
inst✝² : RingHomInvPair σ σ'
F' : Type u_1
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕜 F'
L : F →SL[σ] F'
hf : HasDerivAt f f' x
this : RingHomIsometric σ'
⊢ HasDerivAt (⇑L ∘ f ∘ ⇑σ') (L f') (σ x)
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

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
x : E
s : Set E
h : DifferentiableWithinAt 𝕜 f s x
⊢ HasFDerivWithinAt f (if HasFDerivWithinAt f 0 s x then 0 else Classical.choose h) s x

Tactic:
split_ifs with h₀

Goal state after:
case pos
𝕜 : 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
x : E
s : Set E
h : DifferentiableWithinAt 𝕜 f s x
h₀ : HasFDerivWithinAt f 0 s x
⊢ HasFDerivWithinAt f 0 s x

case neg
𝕜 : 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
x : E
s : Set E
h : DifferentiableWithinAt 𝕜 f s x
h₀ : ¬HasFDerivWithinAt f 0 s x
⊢ HasFDerivWithinAt f (Classical.choose h) s x
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

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
s t : Set E
hf : DifferentiableOn 𝕜 f s
hf' : DifferentiableOn 𝕜 f t
hst : s ∪ t = univ
hs : IsOpen[inst✝³] s
ht : IsOpen[inst✝³] t
⊢ Differentiable 𝕜 f

Tactic:
rw [← differentiableOn_univ, ← hst]

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
s t : Set E
hf : DifferentiableOn 𝕜 f s
hf' : DifferentiableOn 𝕜 f t
hst : s ∪ t = univ
hs : IsOpen[inst✝³] s
ht : IsOpen[inst✝³] t
⊢ DifferentiableOn 𝕜 f (s ∪ t)
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
V' : Type u_3
W : Type u_4
W' : Type u_5
inst✝¹⁰ : NontriviallyNormedField 𝕜
σ σ' : 𝕜 →+* 𝕜
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : NormedSpace 𝕜 V
inst✝⁷ : NormedAddCommGroup V'
inst✝⁶ : NormedSpace 𝕜 V'
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : NormedAddCommGroup W'
inst✝² : NormedSpace 𝕜 W'
inst✝¹ : RingHomIsometric σ
inst✝ : RingHomInvPair σ σ'
L : W →SL[σ] W'
R : V' →SL[σ'] V
f : V → W
z : V'
f' : V →L[𝕜] W
hf : HasFDerivAt f f' (R z)
⊢ HasFDerivAt (⇑L ∘ f ∘ ⇑R) (L ∘SL f' ∘SL R) z

Tactic:
have : RingHomIsometric σ' := .inv σ

Goal state after:
𝕜 : Type u_1
V : Type u_2
V' : Type u_3
W : Type u_4
W' : Type u_5
inst✝¹⁰ : NontriviallyNormedField 𝕜
σ σ' : 𝕜 →+* 𝕜
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : NormedSpace 𝕜 V
inst✝⁷ : NormedAddCommGroup V'
inst✝⁶ : NormedSpace 𝕜 V'
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : NormedAddCommGroup W'
inst✝² : NormedSpace 𝕜 W'
inst✝¹ : RingHomIsometric σ
inst✝ : RingHomInvPair σ σ'
L : W →SL[σ] W'
R : V' →SL[σ'] V
f : V → W
z : V'
f' : V →L[𝕜] W
hf : HasFDerivAt f f' (R z)
this : RingHomIsometric σ'
⊢ HasFDerivAt (⇑L ∘ f ∘ ⇑R) (L ∘SL f' ∘SL R) z