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

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : v (x - y) < min (↑γ * (v y * v y)) (v y)
hyp1 : v (x - y) < ↑γ * (v y * v y)
hyp1' : v (x - y) * (v y * v y)⁻¹ < ↑γ
hyp2 : v (x - y) < v y
key : v x = v y
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
⊢ v (y - x) * (v y * v y)⁻¹ = v (x - y) * (v y * v y)⁻¹

Tactic:
Valuation.map_sub_swap

Goal state after:
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : v (x - y) < min (↑γ * (v y * v y)) (v y)
hyp1 : v (x - y) < ↑γ * (v y * v y)
hyp1' : v (x - y) * (v y * v y)⁻¹ < ↑γ
hyp2 : v (x - y) < v y
key : v x = v y
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
⊢ v (x - y) * (v y * v y)⁻¹ = v (x - y) * (v y * v y)⁻¹
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: 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
⊢ MonoidHom.mker (valuation K (maximalIdeal A)) = Submonoid.map (algebraMap A K) (IsUnit.submonoid A)

Tactic:
ext a

Goal state after:
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
a : K
⊢ a ∈ MonoidHom.mker (valuation K (maximalIdeal A)) ↔ a ∈ Submonoid.map (algebraMap A K) (IsUnit.submonoid A)
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
ha : a ≠ 1
⊢ b ∈ closure {a} ↔ ∃! k, a ^ k = b

Tactic:
by
  rw [mem_closure_singleton]
  constructor
  · suffices Function.Injective (a ^ · : ℤ → G) by
      rintro ⟨m, rfl⟩
      exact ⟨m, rfl, fun k hk ↦ this hk⟩
    rcases ha.lt_or_gt with ha | ha
    · exact (zpow_right_strictAnti ha).injective
    · exact (zpow_right_strictMono ha).injective
  · exact fun h ↦ h.exists

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case neg
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
x y : G
H : ¬IsLeast {y | 0 < y} (y - x)
hxy : x < y
z : G
hz : 0 < z ∧ z < y - x
⊢ ∃ a, x < a ∧ a < y

Tactic:
refine ⟨x + z, ?_, ?_⟩

Goal state after:
case neg.refine_1
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
x y : G
H : ¬IsLeast {y | 0 < y} (y - x)
hxy : x < y
z : G
hz : 0 < z ∧ z < y - x
⊢ x < x + z

case neg.refine_2
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
x y : G
H : ¬IsLeast {y | 0 < y} (y - x)
hxy : x < y
z : G
hz : 0 < z ∧ z < y - x
⊢ x + z < y
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case pos.inr
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
⊢ False

Tactic:
refine this (-y) ?_ ?_

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

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.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case neg
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun a ↦ (valuation R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
⊢ ∃ C, IsIntegral R (C • W)

Tactic:
have hlmax_ge_1 : lmax ≥ 1 := le_of_not_ge hlmax_le_1
    have h : ∃ a : K, valuation R K a = lmax := by
      let i : ℕ := l.idxOf lmax
      have hi : i < l.length := List.idxOf_lt_length_of_mem hlmax_mem
      use l₀[i]
      have hi₁ : (valuation R K) l₀[i] = l[i] := by simp [l]
      simpa only [hi₁] using (List.getElem_idxOf hi)
    choose a ha using h
    have ha₀ : a ≠ 0 := by
      by_contra ha₀; simp only [ha₀, map_zero] at ha
      exact (ha ▸ hlmax_le_1) zero_le_one
    use ⟨Units.mk0 a ha₀, 0, 0, 0⟩
    apply isIntegral_of_exists_lift R
    all_goals
      apply (mem_integer_iff _ _ _).mp
      simp only [variableChange_def, Units.val_inv_eq_inv_val, Units.val_mk0, mul_zero, add_zero,
        inv_pow, zero_mul, sub_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow]
      apply (Valuation.mem_integer_iff _ _).mpr
      simp only [map_mul, map_inv₀, map_pow, ha]
      refine inv_mul_le_one_of_le₀ ?_ zero_le
      refine (hlmax _ (by simp [l₀, l])).trans ?_
    any_goals
      apply le_self_pow hlmax_ge_1.le
      linarith
    rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ = 0
⊢ ∀ (n : ℕ), (coeff n) φ = 0

Tactic:
by simp [h]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ X ^ n ∣ φ ↔ ∀ m < n, (coeff m) φ = 0

Tactic:
convert! @MvPowerSeries.X_pow_dvd_iff Unit R _ () n φ
  constructor <;> intro h m hm
  · rw [Finsupp.unique_single m]
    convert! h _ hm
  · apply h
    simpa only [Finsupp.single_eq_same] using hm

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

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
m : ℕ
a : R
n : ℕ
⊢ (monomial m) a ^ n = (monomial (n * m)) (a ^ n)

Tactic:
simpa [monomial] using MvPowerSeries.monomial_pow (Finsupp.single () m) a n

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

Goal state before:
pp: case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff (l i)) (f i)
u v : σ →₀ ℕ
⊢ (coeff u) (f a) * ∑ l ∈ s.finsuppAntidiag v, ∏ i ∈ s, (coeff (l i)) (f i) =
    ∑ x ∈ (s.finsuppAntidiag v).attach, ∏ x_1 ∈ insert a s, (coeff (Function.update (⇑↑x) a u x_1)) (f x_1)

Tactic:
Finset.mul_sum,

Goal state after:
case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff (l i)) (f i)
u v : σ →₀ ℕ
⊢ ∑ i ∈ s.finsuppAntidiag v, (coeff u) (f a) * ∏ i_1 ∈ s, (coeff (i i_1)) (f i_1) =
    ∑ x ∈ (s.finsuppAntidiag v).attach, ∏ x_1 ∈ insert a s, (coeff (Function.update (⇑↑x) a u x_1)) (f x_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
ha₀ : a ≠ 0
⊢ 1 < (valuation K v) (↑a / ↑b)

Tactic:
have hva : v.valuation K a ≠ 0 := (Valuation.ne_zero_iff _).2 (by simp [ha₀])

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
hva : (valuation K v) ↑a ≠ 0
⊢ 1 < (valuation K v) (↑a / ↑b)
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R[X]
x✝ : ℕ
a✝ : x✝ ∈ Finset.range (φ.natDegree + 1)
⊢ PowerSeries.C (φ.coeff x✝) * PowerSeries.X ^ x✝ = coeToPowerSeries.ringHom (C (φ.coeff x✝) * X ^ x✝)

Tactic:
rw [map_mul, map_pow, coeToPowerSeries.ringHom_apply,
    coeToPowerSeries.ringHom_apply, coe_C, coe_X]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
⊢ (if n = m then a else 0) = (MvPowerSeries.coeff m) ((MvPowerSeries.monomial n) a)

Tactic:
MvPowerSeries.coeff_monomial

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
⊢ (if n = m then a else 0) = if m = n then a else 0
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
⊢ ((∃ d, (coeff d) f ≠ 0 ∧ (weight w) d = n) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff d) f = 0) →
    weightedOrder w f = ↑n

Tactic:
· 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.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
f g : MvPowerSeries σ R
h : f = g
⊢ ∀ (n : σ →₀ ℕ), (trunc' R n) f = (trunc' R n) g

Tactic:
by simp [h]

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

Goal state before:
pp: case h
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 : K
hv : (valuation K v) x ≤ 1
γ : (WithZero (Multiplicative ℤ))ˣ
n d : R
hd✝ : d ∈ v.asIdeal.primeCompl
hd : v.intValuation d = 1
hnd : x * (algebraMap R K) ↑⟨d, hd✝⟩ = (algebraMap R K) n
hd' : v.intValuation n ≤ v.intValuation d
a : R
hval : v.intValuation (n - a * d) < ↑γ
⊢ (valuation K v) ((algebraMap R K) a - x) = (valuation K v) (x - (algebraMap R K) a)

Tactic:
Valuation.map_sub_swap

Goal state after:
case h
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 : K
hv : (valuation K v) x ≤ 1
γ : (WithZero (Multiplicative ℤ))ˣ
n d : R
hd✝ : d ∈ v.asIdeal.primeCompl
hd : v.intValuation d = 1
hnd : x * (algebraMap R K) ↑⟨d, hd✝⟩ = (algebraMap R K) n
hd' : v.intValuation n ≤ v.intValuation d
a : R
hval : v.intValuation (n - a * d) < ↑γ
⊢ (valuation K v) (x - (algebraMap R K) a) = (valuation K v) (x - (algebraMap R K) a)
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: case inr
σ : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace R
inst✝² : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
w : σ → ℕ
hempty : Nonempty ι
h : ∀ (n : ℕ), ∃ a, ∀ (b : ι), a ≤ b → ↑n < weightedOrder w (f b)
d : σ →₀ ℕ
i : ι
hi : ∀ (b : ι), i ≤ b → ↑((Finsupp.weight w) d) < weightedOrder w (f b)
k : ι
hk : i < k
⊢ (coeff d) (f k) = 0

Tactic:
exact coeff_eq_zero_of_lt_weightedOrder w <| hi k hk.le

Goal state after:
Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: case neg
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:
case neg => simp_rw [smul_neg]; exact neg_mem hx

Goal state after:
Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: case neg
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:
case neg => simp_rw [smul_neg]; exact neg_mem hx

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ (X ^ n).order = ↑n

Tactic:
rw [X_pow_eq, order_monomial_of_ne_zero]

Goal state after:
case h
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ 1 ≠ 0
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:
by
      classical
      rw [coeff_mul]
      apply sum_mem
      rintro uv huv
      exact TwoSidedIdeal.mul_mem_right _ _ _
        (hf _ (le_trans (Finset.HasAntidiagonal.antidiagonal.fst_le huv) he))

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

Goal state before:
pp: case refine_2
σ : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
⊢ ∀ (i' : TwoSidedIdeal R × (σ →₀ ℕ)),
    ↑i'.1 ∈ 𝓝 0 → ∃ i, (i.1.Finite ∧ ↑i.2 ∈ 𝓝 0) ∧ (i.1.pi fun x ↦ ↑i.2) ⊆ ↑(basis σ R i')

Tactic:
· intro ⟨I, d⟩ hI
    refine ⟨⟨Iic d, I⟩, ⟨finite_Iic d, hI⟩, ?_⟩
    simpa [basis, coeff_apply, Iic, Set.pi] using! subset_rfl

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

Goal state before:
pp: case zero
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
hn : f 0 = true
⊢ f_max 0 = true

Tactic:
rw [fn] at hn

Goal state after:
case zero
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
hn : false = true
⊢ f_max 0 = true
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
e : τ →₀ ℕ
this✝¹ : UniformSpace R := ⊥
this✝ : UniformSpace S := ⊥
this : HasSum (⇑(coeff e) ∘ fun d ↦ (coeff d) f • d.prod fun s e ↦ a s ^ e) ((coeff e) ((aeval ⋯) f))
⊢ (coeff e) (subst a f) = ∑ᶠ (d : σ →₀ ℕ), (coeff d) f • (coeff e) (d.prod fun s e ↦ a s ^ e)

Tactic:
simp [← coe_substAlgHom ha, substAlgHom, ← this.tsum_eq,
    tsum_eq_finsum (coeff_subst_finite ha f e)]

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

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

Tactic:
by simp [h]

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

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

Tactic:
by simp [h]

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

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

Tactic:
by simp [h]

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
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) (f * g)) 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:
rw [Function.extend_apply' _ _ _ hn, Pi.zero_apply, Finset.sum_eq_zero]

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
⊢ ∀ 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 =
      0
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: τ : Type u_3
S : Type u_4
inst✝ : CommRing S
n : τ →₀ ℕ
hn : n ≠ 0
s : S
⊢ HasSubst ((MvPowerSeries.monomial n) s)

Tactic:
classical
  apply HasSubst.of_constantCoeff_zero
  rw [← MvPowerSeries.coeff_zero_eq_constantCoeff, MvPowerSeries.coeff_monomial,
    if_neg hn.symm]

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

Goal state before:
pp: case pos
σ : 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
f : MvPowerSeries σ R
inst✝ : Finite τ
k : ℕ
ha : HasSubst a
ha₁ : ∀ (i : σ), constantCoeff (a i) = 0
d : τ →₀ ℕ
hd : Finsupp.degree d < k
h1 : Function.HasFiniteSupport fun d_1 ↦ (coeff d_1) f • (coeff d) (d_1.prod fun s e ↦ a s ^ e)
h2 :
  Function.HasFiniteSupport fun d_1 ↦
    (coeff d_1) (∑ i ∈ range k, (homogeneousComponent i) f) • (coeff d) (d_1.prod fun s e ↦ a s ^ e)
⊢ ∑ᶠ (d_1 : σ →₀ ℕ), (coeff d_1) f • (coeff d) (d_1.prod fun s e ↦ a s ^ e) =
    ∑ᶠ (d_1 : σ →₀ ℕ), (coeff d_1) (∑ i ∈ range k, (homogeneousComponent i) f) • (coeff d) (d_1.prod fun s e ↦ a s ^ e)

Tactic:
finsum_eq_sum _ h1,

Goal state after:
case pos
σ : 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
f : MvPowerSeries σ R
inst✝ : Finite τ
k : ℕ
ha : HasSubst a
ha₁ : ∀ (i : σ), constantCoeff (a i) = 0
d : τ →₀ ℕ
hd : Finsupp.degree d < k
h1 : Function.HasFiniteSupport fun d_1 ↦ (coeff d_1) f • (coeff d) (d_1.prod fun s e ↦ a s ^ e)
h2 :
  Function.HasFiniteSupport fun d_1 ↦
    (coeff d_1) (∑ i ∈ range k, (homogeneousComponent i) f) • (coeff d) (d_1.prod fun s e ↦ a s ^ e)
⊢ ∑ i ∈ Set.Finite.toFinset h1, (coeff i) f • (coeff d) (i.prod fun s e ↦ a s ^ e) =
    ∑ᶠ (d_1 : σ →₀ ℕ), (coeff d_1) (∑ i ∈ range k, (homogeneousComponent i) f) • (coeff d) (d_1.prod fun s e ↦ a s ^ e)
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
I : Set ι
hI : I.Finite
U : (i : ι) → Set (E i)
hU : ∀ i ∈ I, Balanced 𝕜 (U i)
x : (i : ι) → E i
hI₀ : I = univ ∨ (∃ i ∈ I, x i ≠ 0) ∨ (𝓝[≠] 0).NeBot
r : ℝ≥0∞
hr : ⨆ i ∈ I, egauge 𝕜 (U i) (x i) < r
c : ι → 𝕜
hc : ∀ i ∈ I, x i ∈ c i • U i
hcr : ∀ i ∈ I, ‖c i‖ₑ < r
⊢ ∃ c₀, (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r

Tactic:
have hr₀ : 0 < r := hr.bot_lt

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
I : Set ι
hI : I.Finite
U : (i : ι) → Set (E i)
hU : ∀ i ∈ I, Balanced 𝕜 (U i)
x : (i : ι) → E i
hI₀ : I = univ ∨ (∃ i ∈ I, x i ≠ 0) ∨ (𝓝[≠] 0).NeBot
r : ℝ≥0∞
hr : ⨆ i ∈ I, egauge 𝕜 (U i) (x i) < r
c : ι → 𝕜
hc : ∀ i ∈ I, x i ∈ c i • U i
hcr : ∀ i ∈ I, ‖c i‖ₑ < r
hr₀ : 0 < r
⊢ ∃ c₀, (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case insert
ι : 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
a✝² : ι
s✝ : Finset ι
a✝¹ : a✝² ∉ s✝
a✝ : (∀ i ∈ s✝, i ∈ s) → ∀ k ≤ n, (∏ x ∈ s✝, f x) k = 1 k
hw : ∀ i ∈ insert a✝² s✝, i ∈ s
⊢ ∀ k ≤ n, (∏ x ∈ insert a✝² s✝, f x) k = 1 k

Tactic:
case insert i w hi hw' =>
    intro k hk
    rw [← one_mul (1 : ArithmeticFunction R), Finset.prod_insert hi, mul_apply, mul_apply]
    refine Finset.sum_congr rfl fun j hj ↦ ?_
    have h1 := hs' i (hw i (Finset.mem_insert_self i w)) j.1
      ((Nat.divisor_le (Nat.fst_mem_divisors_of_mem_antidiagonal hj)).trans hk)
    have h2 := hw' (fun i hi ↦ hw i (Finset.mem_insert_of_mem hi)) j.2
      ((Nat.divisor_le (Nat.snd_mem_divisors_of_mem_antidiagonal hj)).trans hk)
    rw [h1, h2]

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

Goal state before:
pp: case pos.refine_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (i : ι), (f i).IsMultiplicative
hf' : Multipliable f
h✝ : ∀ (s : Finset ι), (∏ b ∈ s, f b).IsMultiplicative
key : ∀ (n : ℕ), ∀ᶠ (i : Finset ι) in (SummationFilter.unconditional ι).filter, (∏ b ∈ i, f b) n = (∏' (b : ι), f b) n
m n : ℕ
hmn : m.Coprime n
h : ∀ (s : Finset ι), (∏ b ∈ s, f b) (m * n) = (∏ b ∈ s, f b) m * (∏ b ∈ s, f b) n
h2 :
  ∀ᶠ (i : Finset ι) in (SummationFilter.unconditional ι).filter,
    (∏ b ∈ i, f b) m * (∏ b ∈ i, f b) n = (∏' (b : ι), f b) (m * n)
⊢ (eulerProduct f) (m * n) = (eulerProduct f) m * (eulerProduct f) n

Tactic:
exact eventually_const.mp (EventuallyEq.trans (.symm h2) (.mul (key m) (key n)))

Goal state after:
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:
simp_rw [← h, eq_aux]

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

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
x : E
h : f =ᶠ[𝓝 x] 0
⊢ HasStrictFDerivAt f 0 x
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
⊢ fderiv 𝕜 f x = 0

Tactic:
notMem_tsupport_iff_eventuallyEq

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
x : E
h : f =ᶠ[𝓝 x] 0
⊢ fderiv 𝕜 f x = 0
Module: Mathlib.Analysis.Calculus.Deriv.Support

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : x ∉ tsupport f
⊢ HasStrictDerivAt f 0 x

Tactic:
notMem_tsupport_iff_eventuallyEq

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : f =ᶠ[nhds x] 0
⊢ HasStrictDerivAt f 0 x