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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x y u : R
hi : u * x ∈ I
v : R
hx : I ⊔ span {v * x} = span {x}
hy : Submodule.colon I ↑(span {v * x}) = span {y}
⊢ u ∈ Submodule.colon I ↑(span {v * x})

Tactic:
mem_colon_span_singleton,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x y u : R
hi : u * x ∈ I
v : R
hx : I ⊔ span {v * x} = span {x}
hy : Submodule.colon I ↑(span {v * x}) = span {y}
⊢ u * (v * x) ∈ I
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: case h
Γ : 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₀
m : ℤ
hm : Units.mk0 (v ↑π.val) ⋯ ^ m = vr
hm' : v ↑π.val ^ m = v ↑r
hm₀ : 0 ≤ m
n : ℕ
hn : m = ↑n
hpow : v (↑π.val ^ (-m) * ↑r) = 1
a : ↥v.valuationSubring := ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
ha : a = ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
ha₀ : ↑a ≠ 0
h_unit_a : IsUnit a
⊢ ↑r = ↑π.val ^ n * ↑a

Tactic:
ha,

Goal state after:
case h
Γ : 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₀
m : ℤ
hm : Units.mk0 (v ↑π.val) ⋯ ^ m = vr
hm' : v ↑π.val ^ m = v ↑r
hm₀ : 0 ≤ m
n : ℕ
hn : m = ↑n
hpow : v (↑π.val ^ (-m) * ↑r) = 1
a : ↥v.valuationSubring := ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
ha : a = ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
ha₀ : ↑a ≠ 0
h_unit_a : IsUnit a
⊢ ↑r = ↑π.val ^ n * ↑⟨↑π.val ^ (-m) * ↑r, ⋯⟩
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 : Fin 3 → R
⊢ (W'.map f).dblZ (⇑f ∘ P) = f (W'.dblZ P)

Tactic:
simp only [dblZ, negY]
  map_simp

Goal state after:
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case h
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
H : (valuation K (maximalIdeal A)) x ≤ 1
π : A
hπ : Irreducible π
a b : A
hb : b ∈ nonZeroDivisors A
h_frac : (algebraMap A K) a / (algebraMap A K) b = x
ha : a = 0
⊢ (algebraMap A K) 0 = (algebraMap A K) a / (algebraMap A K) b

Tactic:
ha,

Goal state after:
case h
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
H : (valuation K (maximalIdeal A)) x ≤ 1
π : A
hπ : Irreducible π
a b : A
hb : b ∈ nonZeroDivisors A
h_frac : (algebraMap A K) a / (algebraMap A K) b = x
ha : a = 0
⊢ (algebraMap A K) 0 = (algebraMap A K) 0 / (algebraMap A K) b
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
h : x ≠ 0
v_ne : v.restrict x ≠ 0
⊢ Tendsto (⇑v.restrict) (𝓝 x) (𝓝 (v.restrict x))

Tactic:
WithZeroTopology.tendsto_of_ne_zero v_ne

Goal state after:
case inr
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
h : x ≠ 0
v_ne : v.restrict x ≠ 0
⊢ ∀ᶠ (x_1 : K) in 𝓝 x, v.restrict x_1 = v.restrict x
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y | y ∈ closure {b ^ n} ∧ 1 < y} b
this✝ : closure {b ^ n} = closure {b}
this : (∃ n_1, (b ^ n) ^ n_1 = b) ∧ 1 < b
m : ℤ
hm : (b ^ n) ^ m = b
⊢ b = b ^ 1

Tactic:
zpow_one

Goal state after:
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y | y ∈ closure {b ^ n} ∧ 1 < y} b
this✝ : closure {b ^ n} = closure {b}
this : (∃ n_1, (b ^ n) ^ n_1 = b) ∧ 1 < b
m : ℤ
hm : (b ^ n) ^ m = b
⊢ b = b
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 Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
nhds_right : (fun x ↦ x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : v.restrict z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑a = (fun x ↦ x * x₀) y
this : ↑z₀⁻¹ = (↑z₀)⁻¹
⊢ ↑a * (↑z₀)⁻¹ ∈ V

Tactic:
ha,

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
nhds_right : (fun x ↦ x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : v.restrict z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑a = (fun x ↦ x * x₀) y
this : ↑z₀⁻¹ = (↑z₀)⁻¹
⊢ (fun x ↦ x * x₀) y * (↑z₀)⁻¹ ∈ V
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case ih
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∀ (a b : K), extension (↑a + ↑b) ≤ extension ↑a ∨ extension (↑a + ↑b) ≤ extension ↑b

Tactic:
· intro x y
      norm_cast
      exact le_max_iff.mp (v.restrict.map_add x y)

Goal state after:
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 Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : (ofClass v).ValueGroup₀ := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := extensionValuation x
hγ₀_def : γ₀ = extensionValuation x
heq : γ₀ = embedding γ₀'
h : γ₀ ≠ 0
h' : γ₀' ≠ 0
hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x
hx : ∀ t ∈ 𝓝 x, ∃ y, ↑y ∈ t
y : K
hy₁ : v y < ↑γ
hy₂ : (restrict₀ (ofClass v)) y = γ₀'
⊢ v y = γ₀

Tactic:
apply_fun embedding at hy₂

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : (ofClass v).ValueGroup₀ := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := extensionValuation x
hγ₀_def : γ₀ = extensionValuation x
heq : γ₀ = embedding γ₀'
h : γ₀ ≠ 0
h' : γ₀' ≠ 0
hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x
hx : ∀ t ∈ 𝓝 x, ∃ y, ↑y ∈ t
y : K
hy₁ : v y < ↑γ
hy₂ : embedding ((restrict₀ (ofClass v)) y) = embedding γ₀'
⊢ v y = γ₀
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsDiscreteValuationRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
W : WeierstrassCurve K
inst✝ : IsMinimal R W
⊢ IsIntegral R W

Tactic:
simpa using IsMinimal.val_Δ_maximal.1

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (coeff (n + 1)) (φ * X) = (coeff n) φ

Tactic:
simp only [coeff, Finsupp.single_add]
  convert! φ.coeff_add_mul_monomial (single () n) (single () 1) _
  rw [mul_one]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : n ≤ d
⊢ (coeff d) (p * X ^ n) = (coeff (d - n)) p

Tactic:
rw [← tsub_add_cancel_of_le h, coeff_mul_X_pow, add_tsub_cancel_right]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
⊢ (coeff d) (X ^ n * p) = 0

Tactic:
· refine (coeff_mul _ _ _).trans (Finset.sum_eq_zero fun x hx => ?_)
    rw [coeff_X_pow, if_neg, zero_mul]
    have := mem_antidiagonal.mp hx
    rw [add_comm] at this
    exact ((le_of_add_le_right this.le).trans_lt <| not_le.mp h).ne

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

Goal state before:
pp: a b c : ℕ
⊢ ofAdd (-↑c) ≤ max (ofAdd (-↑a)) (ofAdd (-↑b)) ↔ min a b ≤ c

Tactic:
rw [le_max_iff, ofAdd_le, ofAdd_le, neg_le_neg_iff, neg_le_neg_iff, Int.ofNat_le, Int.ofNat_le,
    ← min_le_iff]

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

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

Tactic:
v.intValuationDef_if_neg hy,

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ ∃ π, v.intValuation π = exp (-1)

Tactic:
have hv : Irreducible (Associates.mk v.asIdeal) := v.associates_irreducible

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
⊢ ∃ π, v.intValuation π = exp (-1)
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 b : R
hb : b ≠ 0
h : b ∈ v.asIdeal → a ∉ v.asIdeal
hv : b ∈ v.asIdeal
⊢ 1 < (valuation K v) (↑a / ↑b)

Tactic:
have ha₀ : a ≠ 0 := fun _ ↦ by simp_all

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
a b : R
hb : b ≠ 0
h : b ∈ v.asIdeal → a ∉ v.asIdeal
hv : b ∈ v.asIdeal
ha₀ : a ≠ 0
⊢ 1 < (valuation K v) (↑a / ↑b)
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case inr
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 : (WithZero (Multiplicative ℤ))ˣ
⊢ ∃ a, (valuation K v) a = ↑x

Tactic:
obtain ⟨π, hπ⟩ := v.valuation_exists_uniformizer K

Goal state after:
case inr
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 : (WithZero (Multiplicative ℤ))ˣ
π : K
hπ : (valuation K v) π = exp (-1)
⊢ ∃ a, (valuation K v) a = ↑x
Module: Mathlib.Data.Finsupp.Interval

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : Zero α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq α
f✝ g✝ f g x : ι →₀ α
⊢ (∀ (i : ι), x i ∈ (f.rangeIcc g) i) ↔ f ≤ x ∧ x ≤ g

Tactic:
simp_rw [mem_rangeIcc_apply_iff]

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : Zero α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq α
f✝ g✝ f g x : ι →₀ α
⊢ (∀ (i : ι), f i ≤ x i ∧ x i ≤ g i) ↔ f ≤ x ∧ x ≤ g
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R✝ : Type u_2
S : Type u_3
inst✝¹ : CommSemiring R✝
s✝ : Finset (σ →₀ ℕ)
R : Type u_4
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
x✝¹ x✝ : MvPowerSeries σ R
⊢ ∑ x ∈ s, (MvPolynomial.monomial x) ((coeff x) (x✝¹ + x✝)) =
    ∑ x ∈ s, (MvPolynomial.monomial x) ((coeff x) x✝¹) + ∑ x ∈ s, (MvPolynomial.monomial x) ((coeff x) x✝)

Tactic:
simp [sum_add_distrib]

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPowerSeries σ R
x : σ →₀ ℕ
h : degree x < n
⊢ MvPolynomial.coeff x ((truncTotal n) p) = if degree x < n then (coeff x) p else 0

Tactic:
rw [if_pos h, coeff_truncTotal _ h]

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
n : ℕ∞
h : ∀ (d : σ →₀ ℕ), ↑(degree d) < n → (coeff d) f = 0
⊢ n ≤ f.order

Tactic:
simp_rw [degree_eq_weight_one] at h
  exact le_weightedOrder _ h

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

Goal state before:
pp: case refine_1
σ : Type u_1
R : Type u_3
inst✝ : Ring R
p : MvPowerSeries σ R
T : Subring R
hp : ∀ (n : σ →₀ ℕ), (coeff n) p ∈ T
⊢ (p.toSubring T hp).order ≤ p.order

Tactic:
exact le_order fun d hd => by simp [coeff_of_lt_order hd, ← p.coeff_toSubring T hp]

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
hR'S : uR' • S ⊆ S
A : AddSubgroup M := AddSubgroup.closure S
r : R
i : M
hi : i ∈ A
x : M
x✝ : x ∈ AddSubgroup.closure S
hx : r • x ∈ A
⊢ -(r • x) ∈ A

Tactic:
exact neg_mem hx

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
hR'S : uR' • S ⊆ S
A : AddSubgroup M := AddSubgroup.closure S
hRA : ∀ (r : R), ∀ i ∈ A, r • i ∈ A
r' : R'
i : M
hi : i ∈ A
x : M
x✝ : x ∈ AddSubgroup.closure S
hx : r' • x ∈ A
⊢ -(r' • x) ∈ A

Tactic:
exact neg_mem hx

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
n : ℕ
⊢ (monomial n) r = C r * X ^ n

Tactic:
by
  ext; simp [coeff_X_pow, coeff_monomial]

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 × (σ →₀ ℕ)
x✝ y✝ : MvPowerSeries σ R
hf : x✝ ∈ {f | ∀ e ≤ Jd.2, (coeff e) f ∈ Jd.1}
hg : y✝ ∈ {f | ∀ e ≤ Jd.2, (coeff e) f ∈ Jd.1}
e : σ →₀ ℕ
he : e ≤ Jd.2
⊢ (coeff e) x✝ + (coeff e) y✝ ∈ Jd.1

Tactic:
exact add_mem (hf e he) (hg e he)

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

Goal state before:
pp: case «0»
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
f : MvPowerSeries (Fin 2) R
i j k : σ
hF : constantCoeff f = 0
⊢ constantCoeff (![subst ![X i, X j] f, X k] ((fun i ↦ i) ⟨0, ⋯⟩)) = 0

Tactic:
simp_all [constantCoeff_subst_eq_zero .X_X]

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

Goal state before:
pp: case «1»
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
f : MvPowerSeries (Fin 2) R
i j k : σ
hF : constantCoeff f = 0
⊢ constantCoeff (![subst ![X i, X j] f, X k] ((fun i ↦ i) ⟨1, ⋯⟩)) = 0

Tactic:
simp_all [constantCoeff_subst_eq_zero .X_X]

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

Goal state before:
pp: case «0»
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
f : MvPowerSeries (Fin 2) R
i j k : σ
hF : constantCoeff f = 0
⊢ constantCoeff (![X i, subst ![X j, X k] f] ((fun i ↦ i) ⟨0, ⋯⟩)) = 0

Tactic:
simp_all [constantCoeff_subst_eq_zero .X_X]

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

Goal state before:
pp: case «1»
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
f : MvPowerSeries (Fin 2) R
i j k : σ
hF : constantCoeff f = 0
⊢ constantCoeff (![X i, subst ![X j, X k] f] ((fun i ↦ i) ⟨1, ⋯⟩)) = 0

Tactic:
simp_all [constantCoeff_subst_eq_zero .X_X]

Goal state after:
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
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
ha : HasSubst a
⊢ substAlgHom ha = aeval ⋯

Tactic:
ext1 f
  simpa [substAlgHom] using! congr_fun (MvPowerSeries.substAlgHom_eq_aeval ha.const) f

Goal state after:
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 • s) x = egauge 𝕜 s x / ‖c‖ₑ

Tactic:
refine le_antisymm ?_ (le_egauge_smul_left _ _ _)

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 𝕜 (c • s) x ≤ egauge 𝕜 s x / ‖c‖ₑ
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
this✝¹ : UniformSpace R := ⊥
this✝ : IsUniformInducing DFunLike.coe
n : ℕ
s : Set ι
hs : s ∈ cofinite
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, (f y) i = 1 i
t : Finset ι := ⋯.toFinset
u v : Finset ι
hu : ∀ i ∈ u \ t, i ∈ s
hv : ∀ i ∈ v \ t, i ∈ s
this : ∀ (w : Finset ι), (∀ i ∈ w, i ∈ s) → ∀ k ≤ n, (∏ x ∈ w, f x) k = 1 k
⊢ ∀ k ≤ n, (∏ x ∈ u \ t, f x) k = (∏ x ∈ v \ t, f x) k

Tactic:
intro k hk
    rw [this (u \ t) hu k hk, this (v \ t) hv k hk]

Goal state after:
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 𝕜 (ball 0 1) x

Tactic:
by
  simpa using div_le_egauge_ball 𝕜 1 x

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
inst✝ : Nontrivial E
h : UniqueDiffWithinAt 𝕜 s x
⊢ AccPt x (𝓟 s)

Tactic:
by
  by_contra! h'
  have : Dense (Submodule.span 𝕜 (0 : Set E) : Set E) :=
    h.1.mono <| by gcongr; exact tangentConeAt_subset_zero h'
  simp [dense_iff_closure_eq] at this

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f₀ f₁ : E → F
f₀' f₁' : E →L[𝕜] F
L : Filter (E × E)
h₀ : Prod.map f₀ f₀ =ᶠ[L] Prod.map f₁ f₁
h₁ : ∀ (x : E), f₀' x = f₁' x
⊢ HasFDerivAtFilter f₀ f₀' L ↔ HasFDerivAtFilter f₁ f₁' L

Tactic:
by
  simp only [hasFDerivAtFilter_iff_isLittleOTVS]
  exact isLittleOTVS_congr (h₀.mono fun y hy => by simp_all [Prod.map]) .rfl

Goal state after:
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
f' : E →L[𝕜] F
x : E
s : Set E
⊢ HasFDerivWithinAt f f' (insert x s) x ↔ HasFDerivWithinAt f f' s x

Tactic:
hasFDerivWithinAt_insert_self

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
⊢ HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' s x
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
⊢ HasFDerivWithinAt f f' s x ↔ Tendsto (fun x' ↦ ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) (𝓝[s] x) (𝓝 0)

Tactic:
by
  simp [HasFDerivWithinAt, hasFDerivAtFilter_iff_tendsto, Function.comp_def]

Goal state after:
Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries

Goal state before:
pp: 𝕜 : Type u
E : Type v
F : Type w
G : Type x
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
⊢ p.compContinuousLinearMap 0 = constFormalMultilinearSeries 𝕜 E ((p 0) 0)

Tactic:
ext n v

Goal state after:
𝕜 : Type u
E : Type v
F : Type w
G : Type x
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
n : ℕ
v : Fin n → E
⊢ (p.compContinuousLinearMap 0 n) v = (constFormalMultilinearSeries 𝕜 E ((p 0) 0) n) v
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
⊢ p.radius = ∞ → ∀ (r : ℝ≥0), Summable fun n ↦ ‖p n‖ * ↑r ^ n

pp: case mpr
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
⊢ (∀ (r : ℝ≥0), Summable fun n ↦ ‖p n‖ * ↑r ^ n) → p.radius = ∞

Tactic:
· intro h r
    obtain ⟨a, ha : a ∈ Ioo (0 : ℝ) 1, C, - : 0 < C, hp⟩ := p.norm_mul_pow_le_mul_pow_of_lt_radius
      (show (r : ℝ≥0∞) < p.radius from h.symm ▸ ENNReal.coe_lt_top)
    refine .of_norm_bounded
      (g := fun n ↦ (C : ℝ) * a ^ n) ((summable_geometric_of_lt_one ha.1.le ha.2).mul_left _)
      fun n ↦ ?_
    specialize hp n
    rwa [Real.norm_of_nonneg (by positivity)]

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
⊢ (∀ (r : ℝ≥0), Summable fun n ↦ ‖p n‖ * ↑r ^ n) → p.radius = ∞
Module: Mathlib.Analysis.Analytic.CPolynomialDef

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : ∀ y ∈ Metric.eball x r, f y = 0
r_pos : 0 < r
hp : ∀ (n : ℕ), p n = 0
⊢ r ≤ p.radius

Tactic:
rw [p.radius_eq_top_of_forall_image_add_eq_zero 0 (fun n ↦ by rw [add_zero]; exact hp n)]

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : ∀ y ∈ Metric.eball x r, f y = 0
r_pos : 0 < r
hp : ∀ (n : ℕ), p n = 0
⊢ r ≤ ∞