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

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

Tactic:
exact mem_span_singleton'.2 ⟨z, by rw [mul_assoc, mul_comm y]⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.negAddY P Q = (-addU P Q) ^ 3

Tactic:
by
  rw [addU, neg_neg, div_pow, ← negAddY_of_X_eq' hP hQ hx,
    mul_div_cancel_right₀ _ <| pow_ne_zero 3 <| mul_ne_zero hPz hQz]

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

Goal state before:
pp: R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
h : v.IsEquiv w
h_val : Valued.v.IsEquiv Valued.v
⊢ UniformContinuous ⇑(RingHom.id R)

Tactic:
have h_res : v.restrict.IsEquiv w.restrict := h_val.restrict

Goal state after:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
h : v.IsEquiv w
h_val : Valued.v.IsEquiv Valued.v
h_res : v.restrict.IsEquiv w.restrict
⊢ UniformContinuous ⇑(RingHom.id R)
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case h.e_a
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
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
H : (maximalIdeal A).intValuation π ^ n / (maximalIdeal A).intValuation π ^ m ≤ 1
h_mn : m ≤ n
⊢ (algebraMap A K) π ^ (n - m) * ((algebraMap A K) ↑w)⁻¹ =
    (algebraMap A K) π ^ n / ((algebraMap A K) ↑w * (algebraMap A K) π ^ m)

Tactic:
rw [div_eq_mul_inv, mul_inv, mul_comm ((algebraMap A _) ↑w)⁻¹ _, ←
      mul_assoc _ _ ((algebraMap A _) ↑w)⁻¹]

Goal state after:
case h.e_a
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
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
H : (maximalIdeal A).intValuation π ^ n / (maximalIdeal A).intValuation π ^ m ≤ 1
h_mn : m ≤ n
⊢ (algebraMap A K) π ^ (n - m) * ((algebraMap A K) ↑w)⁻¹ =
    (algebraMap A K) π ^ n * ((algebraMap A K) π ^ m)⁻¹ * ((algebraMap A K) ↑w)⁻¹
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : ¬x = 1
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
hxc : closure {x} = closure {x'}
hyc : closure {y} = closure {y'}
Hx : ∀ (z : ↥(closure {x})), z ∈ zpowers ⟨x', ⋯⟩
⊢ ∀ (a : G') (b : a ∈ closure {y}), ⟨a, b⟩ ∈ zpowers ⟨y', ⋯⟩

Tactic:
hyc,

Goal state after:
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : ¬x = 1
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
hxc : closure {x} = closure {x'}
hyc : closure {y} = closure {y'}
Hx : ∀ (z : ↥(closure {x})), z ∈ zpowers ⟨x', ⋯⟩
⊢ ∀ (a : G') (b : a ∈ closure {y'}), ⟨a, ⋯⟩ ∈ zpowers ⟨y', ⋯⟩
Module: Mathlib.GroupTheory.ArchimedeanDensely

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

Tactic:
· rwa [mabs_inv]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

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

Tactic:
wlog ha : 1 ≤ a generalizing a
    · convert! @this (a⁻¹) ?_ (by simpa using le_of_not_ge ha) using 4
      · simp
      · rwa [mabs_inv]
    rw [mabs, sup_eq_left.mpr ((inv_le_one'.mpr ha).trans ha)] at h
    rcases h with ⟨rfl, h⟩
    refine ⟨?_, ?_⟩
    · simp [h]
    · intro x
      simp only [mem_closure_singleton, mem_ofPred_eq, and_imp, forall_exists_index]
      rintro k rfl hk
      rw [← zpow_one b, ← zpow_mul, one_mul, zpow_le_zpow_iff_right h, ← zero_add 1,
          ← Int.lt_iff_add_one_le]
      contrapose! hk
      rw [← Left.one_le_inv_iff, ← zpow_neg]
      exact one_le_zpow ha (by simp [hk])

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

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

Tactic:
obtain ⟨y, hy⟩ := exists_ne (0 : G)

Goal state after:
case pos
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
⊢ False
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a : R
⊢ (if 0 = 0 then a else 0) = a

Tactic:
if_pos rfl

Goal state after:
R : Type u_1
inst✝ : Semiring R
a : R
⊢ a = a
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ (if 1 = 1 then 1 else 0) = 1

Tactic:
if_pos rfl

Goal state after:
R : Type u_1
inst✝ : Semiring R
⊢ 1 = 1
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (coeff n) (φ₁ * (φ₂ + φ₃)) = (coeff n) (φ₁ * φ₂ + φ₁ * φ₃)

Tactic:
by
    classical simp only [coeff_mul, mul_add, Finset.sum_add_distrib, map_add]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {1})).factors)) = 1

Tactic:
Ideal.span_singleton_one,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ exp (-↑((Associates.mk v.asIdeal).count (Associates.mk ⊤).factors)) = 1
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
a b : R
h : C a = C b
⊢ (coeff 0) (C b) = b

Tactic:
coeff_zero_C

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
a b : R
h : C a = C b
⊢ b = b
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case mp.hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m j : σ →₀ ℕ
hij : (single s n, j).1 + (single s n, j).2 = m
⊢ n ≤ m s

Tactic:
rw [← hij, Finsupp.add_apply, Finsupp.single_eq_same]

Goal state after:
case mp.hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m j : σ →₀ ℕ
hij : (single s n, j).1 + (single s n, j).2 = m
⊢ n ≤ n + (single s n, j).2 s
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : 1 ≤ n'
| constantCoeff φ ^ n' * (coeff 1) φ + constantCoeff φ ^ (n' - 1 + 1) * ↑n' * (coeff 1) φ =
    (↑n' + 1) * (coeff 1) φ * constantCoeff φ ^ n'

Tactic:
enter [1, 2, 1, 1]

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : 1 ≤ n'
| constantCoeff φ ^ (n' - 1 + 1)
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✝ = ↑(C (φ.coeff x✝)) * ↑X ^ x✝

Tactic:
coe_C,

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ : R[X]
x✝ : ℕ
a✝ : x✝ ∈ Finset.range (φ.natDegree + 1)
⊢ PowerSeries.C (φ.coeff x✝) * PowerSeries.X ^ x✝ = PowerSeries.C (φ.coeff x✝) * ↑X ^ x✝
Module: Mathlib.RingTheory.MvPowerSeries.Basic

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

Tactic:
← MvPowerSeries.smul_eq_C_mul,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
r : R
⊢ (MvPowerSeries.monomial e) (r • 1) = r • e.prod fun s e ↦ MvPowerSeries.X s ^ e
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra A R
e : σ →₀ ℕ
a✝ : σ → A
a : A
f : MvPowerSeries σ R
⊢ a • f = MvPowerSeries.C ((algebraMap A R) a) * f

Tactic:
← MvPowerSeries.smul_eq_C_mul,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra A R
e : σ →₀ ℕ
a✝ : σ → A
a : A
f : MvPowerSeries σ R
⊢ a • f = (algebraMap A R) a • f
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
a b : R
hv : v.intValuation b ≤ v.intValuation a
γ : Multiplicative ℤ
ha : ¬a = 0
hvaz : v.intValuation a ≠ 0
hγz : ↑γ ≠ 0
n : ℕ
hna : exp (-↑n) < v.intValuation a
hnγ : exp (-↑n) < ↑γ
hvn : emultiplicity v.asIdeal (Ideal.span {a}) ≤ ↑n
⊢ b ∈ v.asIdeal ^ multiplicity v.asIdeal (Ideal.span {a})

Tactic:
rwa [← intValuation_le_pow_iff_mem, ← v.intValuation_eq_exp_neg_multiplicity ha]

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

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

Tactic:
by_cases h : x.degree < n

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

case neg
σ : 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
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: case ind.a.e'_6
σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPowerSeries σ R
k : ℕ
ih : ∀ m ≤ k, ∀ {x : σ →₀ ℕ}, degree x < n → MvPolynomial.coeff x ((truncTotal n) p ^ m) = (coeff x) (p ^ m)
x : σ →₀ ℕ
h : degree x < n
x✝ : (σ →₀ ℕ) × (σ →₀ ℕ)
a✝ : x✝ ∈ antidiagonal x
⊢ MvPolynomial.coeff x✝.2 ((truncTotal n) p) = (coeff x✝.2) p

Tactic:
exact coeff_truncTotal _ (by grind [mem_antidiagonal])

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
p : ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ ((coeff d) fun d ↦ if (weight w) d = p then (coeff d) (f + g) else 0) =
    (coeff d)
      ((fun d ↦ if (weight w) d = p then (coeff d) f else 0) + fun d ↦ if (weight w) d = p then (coeff d) g else 0)

Tactic:
simp only [map_add, coeff_apply]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
p : ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ (if (weight w) d = p then f d + g d else 0) =
    (if (weight w) d = p then f d else 0) + if (weight w) d = p then g d else 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝⁸ : Field K
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
v : HeightOneSpectrum R
inst✝⁴ : Algebra S K
S₀ : Type u_4
inst✝³ : CommSemiring S₀
inst✝² : Algebra S₀ S
inst✝¹ : Algebra S₀ K
inst✝ : IsScalarTower S₀ S K
x : S₀
⊢ (algebraMap S₀ (valuation K v).Completion) x = (algebraMap S (valuation K v).Completion) ((algebraMap S₀ S) x)

Tactic:
by
    exact congrArg (UniformSpace.Completion.coeRingHom (α := WithVal (v.valuation K)))
      (IsScalarTower.algebraMap_apply S₀ S (WithVal (v.valuation K)) x)

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

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
⊢ basis σ R (J, d) ≤ basis σ R (K, e) → J ≤ K ∧ e ≤ d

pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
⊢ J ≤ K ∧ e ≤ d → basis σ R (J, d) ≤ basis σ R (K, e)

Tactic:
· simp only [basis, TwoSidedIdeal.le_iff, TwoSidedIdeal.coe_mk', ofPred_subset_ofPred]
    intro h
    constructor
    · intro x hx
      have (d' : _) : coeff d' (C (σ := σ) x) ∈ J := by
        rw [coeff_C]; split_ifs <;> [exact hx; exact J.zero_mem]
      simpa using h (C x) (fun _ _ ↦ this _) _ zero_le
    · by_contra h'
      apply hK
      rw [eq_top_iff]
      intro x _
      have (d') (hd'_le : d' ≤ d) : coeff d' (monomial e x) ∈ J := by
        rw [coeff_monomial]
        split_ifs with hd' <;> [exact (h' (hd' ▸ hd'_le)).elim; exact J.zero_mem]
      simpa using h (monomial e x) this _ le_rfl

Goal state after:
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
⊢ J ≤ K ∧ e ≤ d → basis σ R (J, d) ≤ basis σ R (K, e)
Module: Mathlib.RingTheory.MvPowerSeries.Evaluation

Goal state before:
pp: case neg
σ : 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✝⁶ : IsTopologicalSemiring R
inst✝⁵ : IsUniformAddGroup R
inst✝⁴ : IsUniformAddGroup S
inst✝³ : CompleteSpace S
inst✝² : T2Space S
inst✝¹ : IsTopologicalRing S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁹.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑φ
ha : HasEval a
f : MvPowerSeries σ R
h : ¬∃ p, ↑p = f
⊢ ⋯.extend (MvPolynomial.eval₂ φ a) f = ⋯.extend (MvPolynomial.eval₂ φ a) f

Tactic:
· rw [← eval₂Hom_eq_extend hφ ha]

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✝⁶ : IsTopologicalSemiring R
inst✝⁵ : IsUniformAddGroup R
inst✝⁴ : IsUniformAddGroup S
inst✝³ : CompleteSpace S
inst✝² : T2Space S
inst✝¹ : IsTopologicalRing S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁹.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑φ
ha : HasEval a
⊢ UniformContinuous (eval₂ φ a)

Tactic:
by
  rw [← coe_eval₂Hom hφ ha]
  exact uniformContinuous_uniformly_extend
    toMvPowerSeries_isUniformInducing
    denseRange_toMvPowerSeries
    (toMvPowerSeries_uniformContinuous hφ ha)

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
S : Type u_2
inst✝⁹ : CommRing S
φ : R →+* S
a : S
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformSpace S
inst✝⁶ : IsUniformAddGroup R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : IsUniformAddGroup S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
inst✝¹ : IsTopologicalRing S
inst✝ : IsLinearTopology S S
hφ : Continuous ⇑φ
ha : HasEval a
f : R⟦X⟧
this : HasSum (fun d ↦ φ ((MvPowerSeries.coeff d) f) * d.prod fun s e ↦ a ^ e) (MvPowerSeries.eval₂ φ (fun x ↦ a) f)
d : Unit →₀ ℕ
hd : d ∉ Set.range (Finsupp.single ())
⊢ (φ ((MvPowerSeries.coeff d) f) * d.prod fun s e ↦ a ^ e) = 0

Tactic:
exact False.elim (hd ⟨d (), by ext; simp⟩)

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

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
f : A⟦X⟧
hf : HasSubst f
n k : ℕ
hk : MvPowerSeries.constantCoeff f ^ k = 0
n' : ℕ
hn' : n' ≤ n
m : ℕ
hm : k * (n + 1) + m ∈ Set.Ici (k * (n + 1))
⊢ ↑n' < (f ^ (k * (n + 1))).order + (f ^ m).order

Tactic:
pow_mul,

Goal state after:
A : Type u_1
inst✝ : CommRing A
f : A⟦X⟧
hf : HasSubst f
n k : ℕ
hk : MvPowerSeries.constantCoeff f ^ k = 0
n' : ℕ
hn' : n' ≤ n
m : ℕ
hm : k * (n + 1) + m ∈ Set.Ici (k * (n + 1))
⊢ ↑n' < ((f ^ k) ^ (n + 1)).order + (f ^ m).order
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
j : ℕ
⊢ ((ofPowerSeries (q ^ k)) f) (q ^ (k * j)) = (algebraMap R R) ((PowerSeries.coeff (k * j / k)) f)

Tactic:
pow_mul,

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
j : ℕ
⊢ ((ofPowerSeries (q ^ k)) f) ((q ^ k) ^ j) = (algebraMap R R) ((PowerSeries.coeff (k * j / k)) f)
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: case succ.succ
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
⊢ (coeff (n + 1 + 1)) (subst (∑ i, C (P.substInvFun ↑i) * X ^ ↑i) P - X) = 0

Tactic:
rw [Fin.sum_univ_castSucc]

Goal state after:
case succ.succ
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
⊢ (coeff (n + 1 + 1))
      (subst
          (∑ i, C (P.substInvFun ↑i.castSucc) * X ^ ↑i.castSucc +
            C (P.substInvFun ↑(Fin.last (n + 2))) * X ^ ↑(Fin.last (n + 2)))
          P -
        X) =
    0
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 ι
hv : t ⊆ v
hu : ∀ i ∈ u \ t, i ∈ s
⊢ ((∏ x ∈ u \ t, f x) * ∏ x ∈ t, f x) n = ((∏ x ∈ v \ t, f x) * ∏ x ∈ t, f x) n

Tactic:
replace hv : ∀ i ∈ v \ t, i ∈ s := by
    intro i hi
    rw [Finset.mem_sdiff, Set.Finite.mem_toFinset, Set.notMem_compl_iff] at hi
    exact hi.2

Goal state after:
ι : 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
⊢ ((∏ x ∈ u \ t, f x) * ∏ x ∈ t, f x) n = ((∏ x ∈ v \ t, f x) * ∏ x ∈ t, f x) n
Module: Mathlib.Analysis.Convex.EGauge

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

Tactic:
rcases exists_enorm_lt 𝕜 hr₀.ne' with ⟨c₀, hc₀, hc₀r⟩

Goal state after:
case inl.inr
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
U : (i : ι) → Set (E i)
x : (i : ι) → E i
r : ℝ≥0∞
c : ι → 𝕜
hr₀ : 0 < r
hI : ∅.Finite
hU : ∀ i ∈ ∅, Balanced 𝕜 (U i)
hI₀ : ∅ = univ ∨ (∃ i ∈ ∅, x i ≠ 0) ∨ (𝓝[≠] 0).NeBot
hr : ⨆ i ∈ ∅, egauge 𝕜 (U i) (x i) < r
hc : ∀ i ∈ ∅, x i ∈ c i • U i
hcr : ∀ i ∈ ∅, ‖c i‖ₑ < r
hbot : (𝓝[≠] 0).NeBot
c₀ : 𝕜
hc₀ : c₀ ≠ 0
hc₀r : ‖c₀‖ₑ < r
⊢ ∃ c₀, (c₀ ≠ 0 ∨ ∅ = univ) ∧ (∀ i ∈ ∅, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r
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
⊢ b.1 = (single 0 (e 0), single 1 (e 1)).1 ∧ b.2 = (single 0 (e 0), single 1 (e 1)).2

Tactic:
← mem_antidiagonal.mp hb,

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
⊢ b.1 = (single 0 ((b.1 + b.2) 0), single 1 ((b.1 + b.2) 1)).1 ∧
    b.2 = (single 0 ((b.1 + b.2) 0), single 1 ((b.1 + b.2) 1)).2
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
⊢ b.1 = (single 0 ((b.1 + b.2) 0), single 1 ((b.1 + b.2) 1)).1 ∧
    b.2 = (single 0 ((b.1 + b.2) 0), single 1 ((b.1 + b.2) 1)).2

Tactic:
h0.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) + 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
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 σ
  let R : 𝕜 →SL[σ'] 𝕜 := ⟨σ'.toSemilinearMap, σ'.isometry.continuous⟩
  have hR (k : 𝕜) : R k = σ' k := rfl
  rw [hasDerivAt_iff_hasFDerivAt]
  convert! HasFDerivAt.comp_semilinear L R (f' := toSpanSingleton 𝕜 f') ?_
  · ext
    simp [R]
  · rwa [← hasDerivAt_iff_hasFDerivAt, hR, RingHomInvPair.comp_apply_eq]

Goal state after: