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

Goal state before:
pp: case mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
b c : ValueGroupWithZero R
x✝ : R
y✝ : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk x✝ y✝ * b * c = ValueGroupWithZero.mk x✝ y✝ * (b * c)

Tactic:
induction b using ValueGroupWithZero.ind

Goal state after:
case mk.mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
c : ValueGroupWithZero R
x✝¹ : R
y✝¹ : ↥(posSubmonoid R)
x✝ : R
y✝ : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk x✝¹ y✝¹ * ValueGroupWithZero.mk x✝ y✝ * c =
    ValueGroupWithZero.mk x✝¹ y✝¹ * (ValueGroupWithZero.mk x✝ y✝ * c)
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
b : ValueGroupWithZero R
x✝ : R
y✝ : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk x✝ y✝ * b = b * ValueGroupWithZero.mk x✝ y✝

Tactic:
induction b using ValueGroupWithZero.ind

Goal state after:
case mk.mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z x✝¹ : R
y✝¹ : ↥(posSubmonoid R)
x✝ : R
y✝ : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk x✝¹ y✝¹ * ValueGroupWithZero.mk x✝ y✝ =
    ValueGroupWithZero.mk x✝ y✝ * ValueGroupWithZero.mk x✝¹ y✝¹
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : W.Point
⊢ (P + Q).toAffineLift = P.toAffineLift + Q.toAffineLift

Tactic:
rcases P, Q with ⟨@⟨⟨_⟩, hP⟩, @⟨⟨_⟩, hQ⟩⟩
  exact toAffine_add hP hQ

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

Goal state before:
pp: case inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
this : ∀ (x y : Γ₀), x ≤ y → Tendsto (fun p ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))
hle : ¬x ≤ y
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))

pp: α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))

Tactic:
· have := (this y x (le_of_not_ge hle)).comp (continuous_swap.tendsto (x, y))
      simpa only [mul_comm, Function.comp_def, Prod.swap] using this

Goal state after:
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
b : ValueGroupWithZero R
x✝ : R
y✝ : ↥(posSubmonoid R)
hab : ValueGroupWithZero.mk x✝ y✝ ≤ b
hba : b ≤ ValueGroupWithZero.mk x✝ y✝
⊢ ValueGroupWithZero.mk x✝ y✝ = b

Tactic:
induction b using ValueGroupWithZero.ind

Goal state after:
case mk.mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z x✝¹ : R
y✝¹ : ↥(posSubmonoid R)
x✝ : R
y✝ : ↥(posSubmonoid R)
hab : ValueGroupWithZero.mk x✝¹ y✝¹ ≤ ValueGroupWithZero.mk x✝ y✝
hba : ValueGroupWithZero.mk x✝ y✝ ≤ ValueGroupWithZero.mk x✝¹ y✝¹
⊢ ValueGroupWithZero.mk x✝¹ y✝¹ = ValueGroupWithZero.mk x✝ y✝
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
b : ValueGroupWithZero R
x✝ : R
y✝ : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk x✝ y✝ ≤ b ∨ b ≤ ValueGroupWithZero.mk x✝ y✝

Tactic:
induction b using ValueGroupWithZero.ind

Goal state after:
case mk.mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z x✝¹ : R
y✝¹ : ↥(posSubmonoid R)
x✝ : R
y✝ : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk x✝¹ y✝¹ ≤ ValueGroupWithZero.mk x✝ y✝ ∨
    ValueGroupWithZero.mk x✝ y✝ ≤ ValueGroupWithZero.mk x✝¹ y✝¹
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
b c : ValueGroupWithZero R
x✝ : R
y✝ : ↥(posSubmonoid R)
hab : ValueGroupWithZero.mk x✝ y✝ ≤ b
⊢ ValueGroupWithZero.mk x✝ y✝ * c ≤ b * c

Tactic:
induction b using ValueGroupWithZero.ind

Goal state after:
case mk.mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
c : ValueGroupWithZero R
x✝¹ : R
y✝¹ : ↥(posSubmonoid R)
x✝ : R
y✝ : ↥(posSubmonoid R)
hab : ValueGroupWithZero.mk x✝¹ y✝¹ ≤ ValueGroupWithZero.mk x✝ y✝
⊢ ValueGroupWithZero.mk x✝¹ y✝¹ * c ≤ ValueGroupWithZero.mk x✝ y✝ * c
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : Ring R
inst✝ : ValuativeRel R
γ : (ValueGroupWithZero R)ˣ
a : R
b : ↥(posSubmonoid R)
hab : ¬0 <ᵥ a
⊢ (valuation R) a / (valuation R) ↑b ≠ ↑γ

Tactic:
not_vlt,

Goal state after:
R : Type u_2
inst✝¹ : Ring R
inst✝ : ValuativeRel R
γ : (ValueGroupWithZero R)ˣ
a : R
b : ↥(posSubmonoid R)
hab : a ≤ᵥ 0
⊢ (valuation R) a / (valuation R) ↑b ≠ ↑γ
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: case neg
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝² : Field K
v : Valuation K Γ
inst✝¹ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : ¬P = ⊥
π : v.Uniformizer := ⋯.some
⊢ Submodule.IsPrincipal P

Tactic:
obtain ⟨x, ⟨hx_mem, hx₀⟩⟩ := Submodule.exists_mem_ne_zero_of_ne_bot h_ne_bot

Goal state after:
case neg
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝² : Field K
v : Valuation K Γ
inst✝¹ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : ¬P = ⊥
π : v.Uniformizer := ⋯.some
x : ↥v.valuationSubring
hx_mem : x ∈ P
hx₀ : x ≠ 0
⊢ Submodule.IsPrincipal P
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:
rw [ha, map_zero, zero_div]

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

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
⊢ T2Space K

Tactic:
apply IsTopologicalAddGroup.t2Space_of_zero_sep

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
⊢ ∀ (x : K), x ≠ 0 → ∃ U ∈ 𝓝 0, x ∉ U
Module: Mathlib.Order.Interval.Finset.DenselyOrdered

Goal state before:
pp: case refine_2
X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered ↑s
x : X
hx : ↑x ∈ s
y : X
hy : ↑y ∈ s
hxy : x < y
this : ⟨↑x, hx⟩ < ⟨↑y, hy⟩
z : { x // x ∈ s }
hz : ↑x < ↑z
hz' : ↑z < ↑y
⊢ ↑x < ↑((↑z).unbot ⋯)

Tactic:
simp [hz.trans_le]

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

Goal state before:
pp: case pos
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 y : K
h : (valuation K (maximalIdeal A)) x = (valuation K (maximalIdeal A)) y
hx : ¬x = 0
hy : y = 0
⊢ ∃ u, u • x = y

pp: case neg
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 y : K
h : (valuation K (maximalIdeal A)) x = (valuation K (maximalIdeal A)) y
hx : ¬x = 0
hy : ¬y = 0
⊢ ∃ u, u • x = y

Tactic:
· simp_all

Goal state after:
case neg
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 y : K
h : (valuation K (maximalIdeal A)) x = (valuation K (maximalIdeal A)) y
hx : ¬x = 0
hy : ¬y = 0
⊢ ∃ u, u • x = 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 Γ₀
F : Filter K
hF : F.NeBot ∧ ∀ (γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
H₀ : ∀ x ∈ M₀, ↑γ₀ ≤ v.restrict x
⊢ (map (fun x ↦ x⁻¹) F).NeBot ∧
    ∀ (γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ),
      ∃ M ∈ map (fun x ↦ x⁻¹) F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ

Tactic:
refine ⟨hF.1.map _, ?_⟩

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
hF : F.NeBot ∧ ∀ (γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
H₀ : ∀ x ∈ M₀, ↑γ₀ ≤ v.restrict x
⊢ ∀ (γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ),
    ∃ M ∈ map (fun x ↦ x⁻¹) F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - 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
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
x : K
x_in₁ : x ∈ M₁
y : K
H₁ : v.restrict (y - x) < ↑(min (γ * γ₀ * γ₀) γ₀)
left✝ : y ∈ M₀
y_in₁ : y ∈ M₁
x_in₀ : ↑γ₀ ≤ v.restrict x
h : v.restrict x = 0
⊢ False

Tactic:
rw [h] at x_in₀

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
x : K
x_in₁ : x ∈ M₁
y : K
H₁ : v.restrict (y - x) < ↑(min (γ * γ₀ * γ₀) γ₀)
left✝ : y ∈ M₀
y_in₁ : y ∈ M₁
x_in₀ : ↑γ₀ ≤ 0
h : v.restrict x = 0
⊢ False
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_1
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedMonoid G
inst✝¹ : MulArchimedean G
inst✝ : Nontrivial G
⊢ IsCyclic G ↔ ¬DenselyOrdered G

Tactic:
rw [← isAddCyclic_additive_iff, LinearOrderedAddCommGroup.isAddCyclic_iff_not_denselyOrdered]
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: 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 ⋯
⊢ ∃ C, IsIntegral R (C • W)

Tactic:
have hlmax_mem : lmax ∈ l :=
    List.maximum_of_length_pos_mem (by simp [l₀, l])

Goal state after:
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
⊢ ∃ C, IsIntegral R (C • W)
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
f : R →+* S
n✝ : ℕ
⊢ (coeff n✝) ((map f) X) = (coeff n✝) X

Tactic:
simp [coeff_X, apply_ite f]

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : Ring R
p : MvPowerSeries σ R
T : Subring R
hp : ∀ (n : σ →₀ ℕ), (coeff n) p ∈ T
d : σ →₀ ℕ
hd : ↑(degree d) < p.order
⊢ (coeff d) (p.toSubring T hp) = 0

Tactic:
by exact_mod_cast (coeff_toSubring p T hp) ▸ (coeff_of_lt_order hd)

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : UniformSpace R
S : Type u_3
inst✝⁴ : CommRing S
inst✝³ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝² : IsUniformAddGroup R
inst✝¹ : IsUniformAddGroup S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁵.toTopologicalSpace, inst✝³.toTopologicalSpace] ⇑φ
ha : HasEval a
⊢ UniformContinuous ⇑(eval₂Hom φ a)

Tactic:
apply uniformContinuous_of_continuousAt_zero

Goal state after:
σ : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : UniformSpace R
S : Type u_3
inst✝⁴ : CommRing S
inst✝³ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝² : IsUniformAddGroup R
inst✝¹ : IsUniformAddGroup S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁵.toTopologicalSpace, inst✝³.toTopologicalSpace] ⇑φ
ha : HasEval a
⊢ ContinuousAt (⇑(eval₂Hom φ a)) 0
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case true
c : ℝ
f g : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
n : ℕ
h : f n = true
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n

Tactic:
replace h3 : g n = true := h3 n h

Goal state after:
case true
c : ℝ
f g : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
h : f n = true
h3 : g n = true
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
i : ℕ
hn : k ∣ i
⊢ ((ofPowerSeries (q ^ k)) f) (q ^ i) = (algebraMap R R) ((PowerSeries.coeff (i / k)) f)

pp: case neg
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
i : ℕ
hn : ¬k ∣ i
⊢ ((ofPowerSeries (q ^ k)) f) (q ^ i) = 0

Tactic:
· obtain ⟨j, rfl⟩ := hn
        rw [pow_mul, ofPowerSeries_apply_pow (one_lt_pow' hq hk)]
        simp [hk]

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
i : ℕ
hn : ¬k ∣ i
⊢ ((ofPowerSeries (q ^ k)) f) (q ^ i) = 0
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

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

Tactic:
· simp_rw [ofPowerSeries_apply hp.one_lt]
      rw [Function.extend_apply', Function.extend_apply' _ _ _ hn,
        Pi.zero_apply, Pi.zero_apply, mul_zero]
      contrapose! hn
      obtain ⟨j, hj⟩ := hn
      obtain ⟨v, -, rfl⟩ := (Nat.dvd_prime_pow hp).mp (Dvd.intro_left _ hj.symm)
      exact ⟨v, rfl⟩

Goal state after:
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: case inr.inl
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ≥0
hc : 1 < ‖c‖
h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0
this : NontriviallyNormedField 𝕜 := { toNormedField := inst✝², non_trivial := ⋯ }
hr : 0 < r
hx : ‖x‖ = 0
⊢ egauge 𝕜 (ball 0 ↑r) x ≤ ‖c‖ₑ * ‖x‖ₑ / ↑r

Tactic:
have hx' : ‖x‖ₑ = 0 := by simpa [enorm, ← coe_nnnorm, NNReal.coe_eq_zero] using hx

Goal state after:
case inr.inl
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ≥0
hc : 1 < ‖c‖
h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0
this : NontriviallyNormedField 𝕜 := { toNormedField := inst✝², non_trivial := ⋯ }
hr : 0 < r
hx : ‖x‖ = 0
hx' : ‖x‖ₑ = 0
⊢ egauge 𝕜 (ball 0 ↑r) x ≤ ‖c‖ₑ * ‖x‖ₑ / ↑r
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)
⊢ subst P.substInv P = X

Tactic:
ext n
  have := coeff_subst_sum_C_substInvFun_mul_X_pow_sub_X P hP n
  rw [map_sub, sub_eq_zero] at this
  rw [← this, coeff_subst', coeff_subst']
  · congr! 3 with m
    generalize hB : (∑ i : Fin (n + 1), C (substInvFun P ↑i) * X ^ i.1) = B
    have : X ^ (n + 1) ∣ mk (substInvFun P) - B := by
      rw [X_pow_dvd_iff]
      intro m hm
      simp +contextual [← hB, coeff_X_pow, Finset.sum_eq_single (⟨m, hm⟩ : Fin (n + 1)),
        Fin.ext_iff, @eq_comm _ m]
    obtain ⟨Q, hQ⟩ := this.trans (sub_dvd_pow_sub_pow _ _ m)
    simp [substInv, sub_eq_iff_eq_add.mp hQ, coeff_X_pow_mul']
  · simp [HasSubst, X, zero_pow_eq, C, substInvFun]
  · simp [HasSubst, ← constantCoeff.eq_def, substInvFun, substInv]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b ∈ antidiagonal e
hb' : b ≠ (single 0 (e 0), single 1 (e 1))
hmul_ne_zero : ¬(MvPowerSeries.coeff b.1) (subst X₀ f) * (MvPowerSeries.coeff b.2) (subst X₁ f) = 0
h0 : b.1 = single 0 (b.1 0) ∧ ¬(coeff (b.1 0)) f = 0
h1 : b.2 = single 1 (b.2 1) ∧ ¬(coeff (b.2 1)) f = 0
⊢ single 0 (b.1 0) = (single 0 ((single 0 (b.1 0) + b.2) 0), single 1 ((single 0 (b.1 0) + b.2) 1)).1 ∧
    b.2 = (single 0 ((single 0 (b.1 0) + b.2) 0), single 1 ((single 0 (b.1 0) + b.2) 1)).2

Tactic:
h1.1

Goal state after:
R : Type u_2
inst✝ : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b ∈ antidiagonal e
hb' : b ≠ (single 0 (e 0), single 1 (e 1))
hmul_ne_zero : ¬(MvPowerSeries.coeff b.1) (subst X₀ f) * (MvPowerSeries.coeff b.2) (subst X₁ f) = 0
h0 : b.1 = single 0 (b.1 0) ∧ ¬(coeff (b.1 0)) f = 0
h1 : b.2 = single 1 (b.2 1) ∧ ¬(coeff (b.2 1)) f = 0
⊢ single 0 (b.1 0) =
      (single 0 ((single 0 (b.1 0) + single 1 (b.2 1)) 0), single 1 ((single 0 (b.1 0) + single 1 (b.2 1)) 1)).1 ∧
    single 1 (b.2 1) =
      (single 0 ((single 0 (b.1 0) + single 1 (b.2 1)) 0), single 1 ((single 0 (b.1 0) + single 1 (b.2 1)) 1)).2
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst✝³ : (i : ι) → AddCommGroup (E i)
inst✝² : (i : ι) → Module 𝕜 (E i)
inst✝¹ : (i : ι) → TopologicalSpace (E i)
inst✝ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =o[𝕜; l] g
this :
  (𝓝 0).HasBasis (fun If ↦ If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ 𝓝 0 ∧ Balanced 𝕜 (If.2 i)) fun If ↦
    If.1.pi fun i ↦ id (If.2 i)
⊢ ∀ (a : Set ι) (b : (i : ι) → Set (E i)),
    (a.Finite ∧ (∀ x ∈ a, b x ∈ 𝓝 0) ∧ ∀ x ∈ a, Balanced 𝕜 (b x)) →
      ∃ j ∈ 𝓝 0,
        ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, (egauge 𝕜 (a.pi fun i ↦ b i) fun i ↦ f i x) ≤ ↑ε * egauge 𝕜 j (g x)

Tactic:
rintro I U ⟨hIf, hU, Ub⟩

Goal state after:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst✝³ : (i : ι) → AddCommGroup (E i)
inst✝² : (i : ι) → Module 𝕜 (E i)
inst✝¹ : (i : ι) → TopologicalSpace (E i)
inst✝ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =o[𝕜; l] g
this :
  (𝓝 0).HasBasis (fun If ↦ If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ 𝓝 0 ∧ Balanced 𝕜 (If.2 i)) fun If ↦
    If.1.pi fun i ↦ id (If.2 i)
I : Set ι
U : (i : ι) → Set (E i)
hIf : I.Finite
hU : ∀ x ∈ I, U x ∈ 𝓝 0
Ub : ∀ x ∈ I, Balanced 𝕜 (U x)
⊢ ∃ j ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, (egauge 𝕜 (I.pi fun i ↦ U i) fun i ↦ f i x) ≤ ↑ε * egauge 𝕜 j (g x)
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst✝³ : (i : ι) → AddCommGroup (E i)
inst✝² : (i : ι) → Module 𝕜 (E i)
inst✝¹ : (i : ι) → TopologicalSpace (E i)
inst✝ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =O[𝕜; l] g
this :
  (𝓝 0).HasBasis (fun If ↦ If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ 𝓝 0 ∧ Balanced 𝕜 (If.2 i)) fun If ↦
    If.1.pi fun i ↦ id (If.2 i)
⊢ ∀ (a : Set ι) (b : (i : ι) → Set (E i)),
    (a.Finite ∧ (∀ x ∈ a, b x ∈ 𝓝 0) ∧ ∀ x ∈ a, Balanced 𝕜 (b x)) →
      ∃ j ∈ 𝓝 0, ∀ᶠ (x : α) in l, (egauge 𝕜 (a.pi fun i ↦ b i) fun i ↦ f i x) ≤ egauge 𝕜 j (g x)

Tactic:
rintro I U ⟨hIf, hU, Ub⟩

Goal state after:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst✝³ : (i : ι) → AddCommGroup (E i)
inst✝² : (i : ι) → Module 𝕜 (E i)
inst✝¹ : (i : ι) → TopologicalSpace (E i)
inst✝ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =O[𝕜; l] g
this :
  (𝓝 0).HasBasis (fun If ↦ If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ 𝓝 0 ∧ Balanced 𝕜 (If.2 i)) fun If ↦
    If.1.pi fun i ↦ id (If.2 i)
I : Set ι
U : (i : ι) → Set (E i)
hIf : I.Finite
hU : ∀ x ∈ I, U x ∈ 𝓝 0
Ub : ∀ x ∈ I, Balanced 𝕜 (U x)
⊢ ∃ j ∈ 𝓝 0, ∀ᶠ (x : α) in l, (egauge 𝕜 (I.pi fun i ↦ U i) fun i ↦ f i x) ≤ egauge 𝕜 j (g x)
Module: Mathlib.Analysis.Analytic.ChangeOrigin

Goal state before:
pp: 𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0
n : ℕ
s : Finset (Fin n)
⊢ (fun s ↦ ⟨s.fst + s.snd.fst, ↑s.snd.snd⟩)
      ((fun s ↦ ⟨s.fst - s.snd.card, ⟨s.snd.card, ⟨Finset.map (finCongr ⋯).toEmbedding s.snd, ⋯⟩⟩⟩) ⟨n, s⟩) =
    ⟨n, s⟩

Tactic:
simp [tsub_add_cancel_of_le (card_finset_fin_le s), finCongr_eq_equivCast]

Goal state after:
Module: Mathlib.Analysis.Analytic.ChangeOrigin

Goal state before:
pp: 𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0
_h0 : 0 < r
hr : ↑‖x‖₊ + ↑r < p.radius
hr' : ↑‖x‖₊ < p.radius
⊢ Summable fun n ↦ ‖p.changeOrigin x n‖₊ * r ^ n

Tactic:
have (k : ℕ) :
      ‖p.changeOrigin x k‖₊ * r ^ k ≤
        (∑' s : Σ l : ℕ, { s : Finset (Fin (k + l)) // s.card = l }, ‖p (k + s.1)‖₊ * ‖x‖₊ ^ s.1) *
          r ^ k := by
    gcongr; exact p.nnnorm_changeOrigin_le k hr'

Goal state after:
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0
_h0 : 0 < r
hr : ↑‖x‖₊ + ↑r < p.radius
hr' : ↑‖x‖₊ < p.radius
this :
  ∀ (k : ℕ),
    ‖p.changeOrigin x k‖₊ * r ^ k ≤ (∑' (s : (l : ℕ) × { s // s.card = l }), ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst) * r ^ k
⊢ Summable fun n ↦ ‖p.changeOrigin x n‖₊ * r ^ n
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: 𝕜 : 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 (E →L[𝕜] F)
z : F
⊢ (p.unshift z).radius = p.radius

Tactic:
rw [← radius_shift, unshift_shift]

Goal state after:
Module: Mathlib.Analysis.Analytic.OfScalars

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
c : ℕ → 𝕜
inst✝ : T2Space E
x : E
⊢ ofScalarsSum c (MulOpposite.op x) = MulOpposite.op (ofScalarsSum c x)

Tactic:
simp [ofScalars_sum_eq, ← MulOpposite.op_pow, ← MulOpposite.op_smul, tsum_op]

Goal state after: