mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: case a₃
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : 2 * 2 = 1
this✝ : Invertible 2 := ⋯
W' : WeierstrassCurve F := ⋯
this : W'.IsCharNeTwoNF
⊢ ({ u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 } • W').a₃ = 0

pp: case a₄
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : 2 * 2 = 1
this✝ : Invertible 2 := ⋯
W' : WeierstrassCurve F := ⋯
this : W'.IsCharNeTwoNF
⊢ ({ u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 } • W').a₄ = 0

Tactic:
· simp [variableChange_a₃]

Goal state after:
case a₄
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : 2 * 2 = 1
this✝ : Invertible 2 := ⋯
W' : WeierstrassCurve F := ⋯
this : W'.IsCharNeTwoNF
⊢ ({ u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 } • W').a₄ = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hz : P z = Q z
hQz : Q z ∈ nonZeroDivisors R
⊢ P ≈ Q ↔ P = Q

Tactic:
refine ⟨?_, Quotient.exact.comp <| congrArg _⟩

Goal state after:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hz : P z = Q z
hQz : Q z ∈ nonZeroDivisors R
⊢ P ≈ Q → P = Q
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case of_j_eq_zero
F : Type u_1
inst✝⁵ : Field F
inst✝⁴ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝³ : E.IsElliptic
inst✝² : E'.IsElliptic
inst✝¹ : CharP F 3
heq : E.j = E'.j
C : VariableChange F
inst✝ : (C • E).IsShortNF
⊢ ∃ C, C • E = E'

Tactic:
· obtain ⟨C', _ | _⟩ := E'.exists_variableChange_isCharThreeNF
    · have h := (C' • E').j_ne_zero_of_isCharThreeJNeZeroNF_of_char_three
      rw [variableChange_j, ← heq, ← variableChange_j E C, j_of_isShortNF_of_char_three] at h
      exact False.elim (h rfl)
    · obtain ⟨C'', hC⟩ := exists_variableChange_of_char_three_of_j_eq_zero (C • E) (C' • E')
      use C'⁻¹ * C'' * C
      rw [mul_smul, mul_smul, hC, ← mul_smul, inv_mul_cancel, one_smul]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ (eval P) W'.polynomialY = 2 * P y + W'.a₁ * P x * P z + W'.a₃ * P z ^ 3

Tactic:
rw [polynomialY_eq]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ (eval P) (C 2 * Y + C W'.a₁ * X * Z + C W'.a₃ * Z ^ 3) = 2 * P y + W'.a₁ * P x * P z + W'.a₃ * P z ^ 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x / P z ^ 2 = Q x / Q z ^ 2
hy : ¬P y / P z ^ 3 = W.toAffine.negY (Q x / Q z ^ 2) (Q y / Q z ^ 3)
⊢ W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3) = -W.dblU P / W.dblZ P

Tactic:
rw [Affine.slope_of_Y_ne hx <| negY_of_Z_ne_zero hQz ▸ hy, ← negY_of_Z_ne_zero hPz, dblU_eq, dblZ]

Goal state after:
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x / P z ^ 2 = Q x / Q z ^ 2
hy : ¬P y / P z ^ 3 = W.toAffine.negY (Q x / Q z ^ 2) (Q y / Q z ^ 3)
⊢ (3 * (P x / P z ^ 2) ^ 2 + 2 * W.toAffine.a₂ * (P x / P z ^ 2) + W.toAffine.a₄ - W.toAffine.a₁ * (P y / P z ^ 3)) /
      (P y / P z ^ 3 - W.negY P / P z ^ 3) =
    -(W.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W.a₂ * P x * P z ^ 2 + W.a₄ * P z ^ 4)) / (P z * (P y - W.negY P))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
h : ¬P ≈ Q
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ W'.add (u • P) (v • Q) = (u * v) ^ 2 • W'.add P Q

Tactic:
rw [add_of_not_equiv <| h.comp (smul_equiv_smul P Q hu hv).mp, addXYZ_smul, add_of_not_equiv h]

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

Goal state before:
pp: case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ γ₀ : (ofClass v).ValueGroup₀ˣ
h : γ₀ * γ₀ ≤ γ
r : R
r_in : v.restrict r < ↑γ₀
s : R
s_in : v.restrict s < ↑γ₀
⊢ v.restrict (r * s) < ↑γ

Tactic:
calc
        v.restrict (r * s) = v.restrict r * v.restrict s := Valuation.map_mul _ _ _
        _ < γ₀.1 * γ₀.1 := by gcongr <;> exact zero_le
        _ ≤ γ := mod_cast h

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

Goal state before:
pp: R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Jacobian R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (W'⁄B).neg (⇑↑f ∘ P) = ⇑↑f ∘ (W'⁄A).neg P

Tactic:
← WeierstrassCurve.Jacobian.map_neg,

Goal state after:
R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Jacobian R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (W'⁄B).neg (⇑↑f ∘ P) = ((W'⁄A).map ↑f).neg (⇑↑f ∘ P)
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:
pp: Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
⊢ update pure 0 (pure 0 ⊔ ⨅ γ, ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ)) = update pure 0 (⨅ γ, ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ))

Tactic:
sup_of_le_right

Goal state after:
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
⊢ update pure 0 (⨅ γ, ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ)) = update pure 0 (⨅ γ, ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ))

Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
⊢ pure 0 ≤ ⨅ γ, ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ)
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case neg.h₁
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
hx : ¬x ≤ᵥ 0
hy : ¬y ≤ᵥ 0
⊢ ↑s * ↑⟨y, hy⟩ ≤ᵥ ↑t * ↑⟨x, hx⟩

pp: case h₂
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
hx : ¬x ≤ᵥ 0
hy : ¬y ≤ᵥ 0
⊢ ↑t * ↑⟨x, hx⟩ ≤ᵥ ↑s * ↑⟨y, hy⟩

Tactic:
· grw [veq_mul_comm, veq_mul_comm _ x]
        simpa using h₂

Goal state after:
case h₂
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
hx : ¬x ≤ᵥ 0
hy : ¬y ≤ᵥ 0
⊢ ↑t * ↑⟨x, hx⟩ ≤ᵥ ↑s * ↑⟨y, hy⟩
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x ↦ ↑x⁻¹) = (fun y ↦ ↑y) ∘ fun x ↦ x⁻¹
⊢ Cauchy (map (fun y ↦ ↑y) (map (fun x ↦ x⁻¹) (Filter.comap coe' (𝓝 y))))

Tactic:
apply Cauchy.map _ (Completion.uniformContinuous_coe K)

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x ↦ ↑x⁻¹) = (fun y ↦ ↑y) ∘ fun x ↦ x⁻¹
⊢ Cauchy (map (fun x ↦ x⁻¹) (Filter.comap coe' (𝓝 y)))
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: case hH
A : Type u_2
inst✝ : Ring A
v : Valuation A (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
n : (WithZero (Multiplicative ℤ))ˣ
hπ : (exp 1)⁻¹ ∈ range ⇑v
x✝ : ∃ k, Units.mk0 (exp 1)⁻¹ ⋯ ^ k = n
k : ℤ
h : Units.mk0 (exp 1)⁻¹ ⋯ ^ k = n
⊢ ∃ a,
    ¬(MonoidWithZeroHom.ofClass v) a = 0 ∧ ∃ x, (MonoidWithZeroHom.ofClass v) a * ↑n = (MonoidWithZeroHom.ofClass v) x

Tactic:
rw [← h]

Goal state after:
case hH
A : Type u_2
inst✝ : Ring A
v : Valuation A (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
n : (WithZero (Multiplicative ℤ))ˣ
hπ : (exp 1)⁻¹ ∈ range ⇑v
x✝ : ∃ k, Units.mk0 (exp 1)⁻¹ ⋯ ^ k = n
k : ℤ
h : Units.mk0 (exp 1)⁻¹ ⋯ ^ k = n
⊢ ∃ a,
    ¬(MonoidWithZeroHom.ofClass v) a = 0 ∧
      ∃ x, (MonoidWithZeroHom.ofClass v) a * ↑(Units.mk0 (exp 1)⁻¹ ⋯ ^ k) = (MonoidWithZeroHom.ofClass v) x
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
⊢ Nonempty (G ≃*o WithZero (Multiplicative ℤ)) ∨ DenselyOrdered Gˣ

Tactic:
refine (LinearOrderedCommGroup.discrete_or_denselyOrdered Gˣ).imp_left ?_

Goal state after:
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
⊢ Nonempty (Gˣ ≃*o Multiplicative ℤ) → Nonempty (G ≃*o WithZero (Multiplicative ℤ))
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
C : VariableChange K
hC : MaximalFor (fun C ↦ IsIntegral R (C • W)) (fun C ↦ valuation_Δ_aux R (C • W)) C
j : VariableChange K
hj : IsIntegral R ((j • C) • W)
h : (fun C ↦ valuation_Δ_aux R (C • W)) C ≤ (fun C ↦ valuation_Δ_aux R (C • W)) (j • C) →
  (fun C ↦ valuation_Δ_aux R (C • W)) (j • C) ≤ (fun C ↦ valuation_Δ_aux R (C • W)) C :=
  hC.right hj
⊢ valuation_Δ_aux R (C • W) ≤ valuation_Δ_aux R (j • C • W) → valuation_Δ_aux R (j • C • W) ≤ valuation_Δ_aux R (C • W)

Tactic:
rw [← smul_assoc]

Goal state after:
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
C : VariableChange K
hC : MaximalFor (fun C ↦ IsIntegral R (C • W)) (fun C ↦ valuation_Δ_aux R (C • W)) C
j : VariableChange K
hj : IsIntegral R ((j • C) • W)
h : (fun C ↦ valuation_Δ_aux R (C • W)) C ≤ (fun C ↦ valuation_Δ_aux R (C • W)) (j • C) →
  (fun C ↦ valuation_Δ_aux R (C • W)) (j • C) ≤ (fun C ↦ valuation_Δ_aux R (C • W)) C :=
  hC.right hj
⊢ valuation_Δ_aux R (C • W) ≤ valuation_Δ_aux R ((j • C) • W) →
    valuation_Δ_aux R ((j • C) • W) ≤ valuation_Δ_aux R (C • W)
Module: Mathlib.RingTheory.MvPowerSeries.Basic

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

Tactic:
dsimp only [coeff, MvPowerSeries]
  rw [monomial_def, LinearMap.proj_apply (i := m), LinearMap.single_apply, Pi.single_apply]

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

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

Tactic:
classical
  have :
    ∀ p ∈ antidiagonal m,
      coeff (p : (σ →₀ ℕ) × (σ →₀ ℕ)).1 φ * coeff p.2 (monomial n a) ≠ 0 → p.2 = n :=
    fun p _ hp => eq_of_coeff_monomial_ne_zero (right_ne_zero_of_mul hp)
  rw [coeff_mul, ← Finset.sum_filter_of_ne this, Finset.HasAntidiagonal.filter_snd_eq_antidiagonal
    _ n, Finset.sum_ite_index]
  simp only [Finset.sum_singleton, coeff_monomial_same, Finset.sum_empty]

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

Goal state before:
pp: case inr.succ
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)}
⊢ constantCoeff φ ^ n' * (coeff 1) φ + (coeff 1) (φ ^ n') * constantCoeff φ =
    (↑n' + 1) * (coeff 1) φ * constantCoeff φ ^ n'

Tactic:
have h₀ : n' = 0 ∨ 1 ≤ n' := by lia

Goal state after:
case inr.succ
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₀ : n' = 0 ∨ 1 ≤ n'
⊢ constantCoeff φ ^ n' * (coeff 1) φ + (coeff 1) (φ ^ n') * constantCoeff φ =
    (↑n' + 1) * (coeff 1) φ * constantCoeff φ ^ n'
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case right
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff d) f ≠ 0
hd : (weight w) d = n
⊢ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff d) (f + g) = 0

Tactic:
intro b hb
    suffices weight w b < weightedOrder w f by
      rw [(coeff _).map_add, coeff_eq_zero_of_lt_weightedOrder w this,
        coeff_eq_zero_of_lt_weightedOrder w (lt_trans this H), add_zero]
    rw [← hn, Nat.cast_lt]
    exact hb

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

Goal state before:
pp: case refine_1
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
p : MvPolynomial σ R
h : (truncFinset R s) ↑p = p
⊢ p.support ⊆ s

Tactic:
rw [← h]

Goal state after:
case refine_1
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
p : MvPolynomial σ R
h : (truncFinset R s) ↑p = p
⊢ ((truncFinset R s) ↑p).support ⊆ s
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
p : ℕ
d : σ →₀ ℕ
f : MvPowerSeries σ R
⊢ (coeff d) ((homogeneousComponent p) f) = if degree d = p then (coeff d) f else 0

Tactic:
rw [degree_eq_weight_one]
  exact coeff_weightedHomogeneousComponent 1 p d f

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

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

Tactic:
trunc_mul_trunc

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
⊢ (trunc n) (f * g) = (trunc n) (f * g)
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
⊢ cantorFunction c f = cantorFunction c g → f = g

Tactic:
hfg

Goal state after:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
hfg : cantorFunction c f = cantorFunction c g
⊢ f = g
Module: Mathlib.Analysis.Complex.Cardinality

Goal state before:
pp: ⊢ #ℝ * #ℝ = 𝔠

Tactic:
mk_real,

Goal state after:
⊢ 𝔠 * 𝔠 = 𝔠
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
h : f =ᶠ[cofinite] g
hf : LSeriesSummable f s
this : term f s =ᶠ[cofinite] term g s
n : ℕ
hn : term g s n = term f s n
⊢ ‖term g s n‖ ≤ ‖term f s n‖

Tactic:
simp [hn]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
n : ℕ
hn : n ≠ 0
⊢ constantCoeff (X ^ n) = 0

Tactic:
simp [hn]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : ¬1 < q
hn : n = 1
⊢ ((algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff (f + g))) n =
    ((algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff f) +
        (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff g))
      n

Tactic:
simp [hn]

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 : ¬n = 1
⊢ ((algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff (f + g))) n =
    ((algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff f) +
        (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff g))
      n

Tactic:
simp [hn]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
q : ℕ
x : R
n : ℕ
hq : 1 < q
hn : n = 1
⊢ q ^ 0 = n

Tactic:
simp [hn]

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)
this : Set.Finite.toFinset h2 ⊆ Set.Finite.toFinset h1
aux : ∀ {n : σ →₀ ℕ}, (coeff d) (n.prod fun s e ↦ a s ^ e) ≠ 0 → Finsupp.degree n ≤ Finsupp.degree d
⊢ ∀ (x : σ →₀ ℕ), ¬(coeff x) f • (coeff d) (x.prod fun s e ↦ a s ^ e) = 0 → Finsupp.degree x < k

Tactic:
grind [right_ne_zero_of_smul]

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
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
U : Set E
V : Set F
hU : Balanced 𝕜 U
hV : Balanced 𝕜 V
a : E
b : F
r : ℝ≥0∞
x : 𝕜
hx : a ∈ x • U
hxr : ‖x‖ₑ < r
y : 𝕜
hy : b ∈ y • V
hyr : ‖y‖ₑ < r
⊢ ∃ c, (a, b) ∈ (c • U) ×ˢ (c • V) ∧ ‖c‖ₑ < r

Tactic:
cases le_total ‖x‖ ‖y‖ with
  | inl hle => exact ⟨y, ⟨hU.smul_mono hle hx, hy⟩, hyr⟩
  | inr hle => exact ⟨x, ⟨hx, hV.smul_mono hle hy⟩, hxr⟩

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

Goal state before:
pp: case hf
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
k : R
i : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = X * B
hB' : constantCoeff (X * B) = 0
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst (X * B) P) = k
⊢ (i ∈ Function.support fun d ↦ (coeff d) P * (coeff (n + 1 + 1)) ((X * B) ^ d)) → i ∈ Set.Iio (n + 3)

Tactic:
simp +contextual [mul_pow, coeff_X_pow_mul', Nat.lt_succ_iff]

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)
n : ℕ
⊢ (coeff n) (subst (∑ i, C (P.substInvFun ↑i) * X ^ ↑i) P - X) = 0

Tactic:
by
  obtain (_ | _ | n) := n
  · rw [map_sub, coeff_subst']
    · simp +contextual [finsum_eq_single (a := 0), substInvFun, zero_pow_eq, hP]
    · simp [substInvFun, HasSubst]
  · rw [map_sub, coeff_subst']
    · rw [finsum_eq_single (a := 1)]
      · simp [substInvFun]
      · rintro (_ | _ | _) _ <;> simp_all [substInvFun, mul_pow, coeff_mul_X_pow']
    · simp [HasSubst, X, substInvFun]
  · rw [Fin.sum_univ_castSucc]
    simp only [Fin.val_castSucc, Fin.val_last, map_sub, substInvFun]
    generalize hB : ∑ i : Fin (n + 2), C (substInvFun P i) * X ^ i.1 = B
    have hB' : B.constantCoeff = 0 := by simp [← hB, zero_pow_eq, substInvFun]
    simp only [neg_mul, map_neg, map_mul, coeff_X, Nat.add_eq_right, Nat.add_eq_zero_iff,
      one_ne_zero, and_false, ↓reduceIte, sub_zero]
    rw [coeff_subst']
    · simp only [smul_eq_mul, ← map_mul]
      generalize hk : ⅟(P.coeff 1) * coeff (n + 1 + 1) (subst B P) = k
      trans ∑ᶠ d, P.coeff d * (coeff (n + 1 + 1) (B ^ d) - if d = 1 then k else 0)
      · refine finsum_congr fun i ↦ ?_
        · congr 1
          obtain (_ | _ | i) := i
          · simp
          · simp [← sub_eq_add_neg]
          · simp only [add_assoc, Nat.reduceAdd]
            rw [add_comm B, add_pow, map_sum, Finset.sum_eq_single (a := 0)]
            · simp
            · rintro (_ | _ | j) hj hj'
              · simp at hj'
              · simp [mul_comm (C k), hB', mul_assoc, coeff_X_pow_mul']
              · rw [← neg_mul, mul_pow, ← pow_mul, mul_comm (_ ^ _)]
                simp [mul_assoc, coeff_X_pow_mul']
            · simp
      · simp_rw [mul_sub]
        rw [finsum_sub_distrib]
        · simp only [mul_ite, mul_zero]
          nth_rw 2 [finsum_eq_single (a := 1)]
          · simp only [↓reduceIte, ← hk, mul_invOf_cancel_left', sub_eq_zero]
            rw [coeff_subst']
            · rfl
            · simp [HasSubst, ← PowerSeries.constantCoeff.eq_def, hB']
          · simp +contextual
        · refine .subset (Set.finite_Iio (n + 3)) fun i ↦ ?_
          obtain ⟨B, rfl⟩ : X ∣ B := by rwa [X_dvd_iff]
          simp +contextual [mul_pow, coeff_X_pow_mul', Nat.lt_succ_iff]
        · exact .subset (Set.finite_singleton 1) (fun _ ↦ by simp +contextual)
    · simp [HasSubst, ← PowerSeries.constantCoeff.eq_def, hB']

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : SMul 𝕜 E
inst✝¹ : TopologicalSpace E
s : Set E
x : E
inst✝ : ContinuousAdd E
y : E
hy : y ∈ tangentConeAt 𝕜 s x
ι : Type (max u_1 u_2)
l : Filter ι
hl : l.NeBot
d : ι → E
hd : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x + d n ∈ s
⊢ x ∈ closure[inst✝¹] s

Tactic:
refine mem_closure_of_tendsto ?_ hds

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : SMul 𝕜 E
inst✝¹ : TopologicalSpace E
s : Set E
x : E
inst✝ : ContinuousAdd E
y : E
hy : y ∈ tangentConeAt 𝕜 s x
ι : Type (max u_1 u_2)
l : Filter ι
hl : l.NeBot
d : ι → E
hd : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x + d n ∈ s
⊢ Tendsto (fun x_1 ↦ x + d x_1) l (𝓝 x)
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
hx : ¬AccPt x (𝓟 s)
y : E
hy : y ∈ tangentConeAt 𝕜 s x
ι : Type (max u_1 u_2)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x + d n ∈ s
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
H₁ : Tendsto (fun x_1 ↦ x + d x_1) l (𝓝 x)
H₂ : ∀ᶠ (n : ι) in l, d n = 0
n : ι
hn : d n = 0
⊢ c n • d n = 0

Tactic:
simp [hn]

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

Goal state before:
pp: case refine_1
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
ιE : Sort u_7
ιF : Sort u_8
pE : ιE → Prop
pF : ιF → Prop
sE : ιE → Set E
sF : ιF → Set F
hE : (𝓝 0).HasBasis pE sE
hF : (𝓝 0).HasBasis pF sF
s t : Set E
hsub : s ⊆ t
V : Set F
hV₀ : V ∈ 𝓝 0
hV : (fun x ↦ egauge 𝕜 s (f x)) ≤ᶠ[l] fun x ↦ egauge 𝕜 V (g x)
⊢ ∃ V ∈ 𝓝 0, (fun x ↦ egauge 𝕜 t (f x)) ≤ᶠ[l] fun x ↦ egauge 𝕜 V (g x)

Tactic:
exact ⟨V, hV₀, hV.mono fun x ↦ le_trans <| egauge_anti _ hsub _⟩

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : TopologicalSpace F
inst✝¹ : Module 𝕜 F
f : α → E
g : α → F
inst✝ : TopologicalSpace α
x : α
s : Set α
h : f x = 0
⊢ f =o[𝕜; 𝓝[insert x s] x] g ↔ f =o[𝕜; 𝓝[s] x] g

Tactic:
rw [nhdsWithin_insert, isLittleOTVS_sup, and_iff_right]
  exact .congr' (.zero g _) h.symm .rfl

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ derivWithin f s x = 0

Tactic:
by
  rw [derivWithin, fderivWithin_zero_of_notMem_closure h, zero_apply]

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f' : F
hf' : f' ≠ 0
⊢ Topology.IsInducing ⇑(toSpanSingleton 𝕜 f')

Tactic:
refine AntilipschitzWith.isInducing (K := ‖f'‖₊⁻¹) ?_ (map_continuous _)
  simp [antilipschitzWith_iff_le_mul_dist, dist_eq_norm, ← sub_smul, norm_smul, field]

Goal state after: