mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case odd
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
k : ℤ
m✝ : ℕ
ih : ∀ k_1 < 2 * (m✝ + 1) + 1, f (complEDS' b c d k k_1) = complEDS' (f b) (f c) (f d) k k_1
⊢ f (complEDS' b c d k (2 * (m✝ + 1) + 1)) = complEDS' (f b) (f c) (f d) k (2 * (m✝ + 1) + 1)

Tactic:
simp only [complEDS'_even, complEDS'_odd, map_normEDS, map_complEDS₂, map_pow, map_mul, map_sub]

Goal state after:
case odd
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
k : ℤ
m✝ : ℕ
ih : ∀ k_1 < 2 * (m✝ + 1) + 1, f (complEDS' b c d k k_1) = complEDS' (f b) (f c) (f d) k k_1
⊢ f (complEDS' b c d k (m✝ + 1)) ^ 2 * normEDS (f b) (f c) (f d) ((↑m✝ + 2) * k + 1) *
        normEDS (f b) (f c) (f d) ((↑m✝ + 2) * k - 1) -
      f (complEDS' b c d k (m✝ + 2)) ^ 2 * normEDS (f b) (f c) (f d) ((↑m✝ + 1) * k + 1) *
        normEDS (f b) (f c) (f d) ((↑m✝ + 1) * k - 1) =
    complEDS' (f b) (f c) (f d) k (m✝ + 1) ^ 2 * normEDS (f b) (f c) (f d) ((↑m✝ + 2) * k + 1) *
        normEDS (f b) (f c) (f d) ((↑m✝ + 2) * k - 1) -
      complEDS' (f b) (f c) (f d) k (m✝ + 2) ^ 2 * normEDS (f b) (f c) (f d) ((↑m✝ + 1) * k + 1) *
        normEDS (f b) (f c) (f d) ((↑m✝ + 1) * k - 1)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ 1 + 4 * W.a₂ = 1

Tactic:
linear_combination 2 * W.a₂ * CharP.cast_eq_zero R 2

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

Goal state before:
pp: case a₂
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
ha₁ : W.a₁ = 0
⊢ 1 ^ 2 * (W.a₂ - 0 * W.a₁ + 3 * W.a₂ - 0 ^ 2) = 0

Tactic:
linear_combination 2 * W.a₂ * CharP.cast_eq_zero R 2

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
S : Type s
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
n : Fin 3
⊢ (⇑f ∘ (u • P)) n = (f u • ⇑f ∘ P) n

Tactic:
fin_cases n <;> simp only [smul_fin3, comp_fin3] <;> map_simp

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
Q : Fin 3 → R
u : Rˣ
⊢ W'.Equation ((fun m ↦ m • Q) u) ↔ W'.Equation Q

Tactic:
exact equation_smul Q u.isUnit

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : 0 = P x ^ 3 ∧ (3 * P x ^ 2 ≠ 0 ∨ 2 * 0 ≠ 0 ∨ W'.a₁ * P x * 0 ≠ 0)
hPz : P z = 0
hPx : P x ≠ 0
hPy : P y = 0
⊢ False

Tactic:
exact hPx <| eq_zero_of_pow_eq_zero hP.left.symm

Goal state after:
Module: Mathlib.Data.Int.WithZero

Goal state before:
pp: case neg.e_a.e_6
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : ¬x * y = 0
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑(unzero hxy) = x * y

Tactic:
coe_unzero hxy

Goal state after:
case neg.e_a.e_6
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : ¬x * y = 0
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y = x * y
Module: Mathlib.Data.Int.WithZero

Goal state before:
pp: case neg
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he0 : e ≠ 0
he1 : e ≠ 1
hm : ¬m = 0
h1 : (toNNReal he0) m = 1
⊢ m = 1

Tactic:
rw [toNNReal_neg_apply he0 hm, zpow_eq_one_iff_right₀ _root_.zero_le he1, toAdd_eq_zero] at h1

Goal state after:
case neg
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he0 : e ≠ 0
he1 : e ≠ 1
hm : ¬m = 0
h1 : unzero hm = 1
⊢ m = 1
Module: Mathlib.Data.Int.WithZero

Goal state before:
pp: e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he : 1 < e
⊢ (toNNReal ⋯) m < 1 ↔ m < 1

Tactic:
rw [← (toNNReal_strictMono he).lt_iff_lt, map_one]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z = 0
⊢ W'.add P Q = -(Q x * P z) • P

Tactic:
by
  rw [add_of_not_equiv <| not_equiv_of_Z_eq_zero_right hPz hQz, addXYZ_of_Z_eq_zero_right hQ hQz]

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

Goal state before:
pp: case pos
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q

pp: case neg
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q

Tactic:
· rw [toAffine_of_Z_eq_zero hPz, zero_add]
    by_cases hQz : Q z = 0
    · rw [add_of_Z_eq_zero hP hQ hPz hQz, toAffine_smul _ <| (isUnit_X_of_Z_eq_zero hP hPz).pow 2,
        toAffine_zero, toAffine_of_Z_eq_zero hQz]
    · rw [add_of_Z_eq_zero_left hP.left hPz hQz,
        toAffine_smul _ <| (isUnit_X_of_Z_eq_zero hP hPz).mul <| Ne.isUnit hQz]

Goal state after:
case neg
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: K : Type u
inst✝² : DivisionRing K
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : MulArchimedean Γ₀
v : Valuation K Γ₀
x : K
hx : v x ≠ 0
r : Γ₀ˣ
hr : ↑r ≠ 0
h : ∀ (x : K), v x ≠ 0 → ↑r < v x
H : Units.mk0 (v x) hx < 1
k : ℕ
hk : Units.mk0 (v x) hx ^ k < r
⊢ v (x ^ k) ≠ 0

Tactic:
simp [hx]

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

Goal state before:
pp: K : Type u
inst✝² : DivisionRing K
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : MulArchimedean Γ₀
v : Valuation K Γ₀
x : K
hx : v x ≠ 0
r : Γ₀ˣ
hr : ↑r ≠ 0
h : ∀ (x : K), v x ≠ 0 → ↑r < v x
H : (Units.mk0 (v x) hx)⁻¹ < 1
k : ℕ
hk : (Units.mk0 (v x) hx)⁻¹ ^ k < r
⊢ v (x ^ (-↑k)) ≠ 0

Tactic:
simp [hx]

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

Goal state before:
pp: α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ✝ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
γ : Γ₀
h : γ ≠ 0
⊢ Tendsto Inv.inv (pure γ) (𝓝 γ⁻¹)

Tactic:
exact pure_le_nhds γ⁻¹

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
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 _ y]

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
⊢ ↑⟨x, hx⟩ * ↑t ≤ᵥ y * ↑s
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: K : Type u_1
inst✝⁹ : Field K
inst✝⁸ : UniformSpace K
L✝ : Type u_2
inst✝⁷ : Field L✝
inst✝⁶ : UniformSpace L✝
inst✝⁵ : CompletableTopField L✝
L : Type u_3
inst✝⁴ : Field L
inst✝³ : UniformSpace L
inst✝² : IsTopologicalDivisionRing L
inst✝¹ : T0Space L
inst✝ : CompleteSpace L
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
⊢ Cauchy (map (fun x ↦ x⁻¹) F)

Tactic:
by
    have : NeBot F := cau_F.1
    rcases CompleteSpace.complete cau_F with ⟨x, hx⟩
    have hx' : x ≠ 0 := by
      rintro rfl
      rw [inf_eq_right.mpr hx] at hF
      exact cau_F.1.ne hF
    exact Filter.Tendsto.cauchy_map <|
      calc
        map (fun x => x⁻¹) F ≤ map (fun x => x⁻¹) (𝓝 x) := map_mono hx
        _ ≤ 𝓝 x⁻¹ := continuousAt_inv₀ hx'

Goal state after:
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
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 - ↑m) ≤ ↑(ofAdd 0)
v_π_lt_one : (maximalIdeal A).intValuation π < 1
v_π_ne_zero : (maximalIdeal A).intValuation π ≠ 0
⊢ ↑m ≤ ↑n

Tactic:
rwa [← sub_nonneg, ← zpow_le_one_iff_right_of_lt_one₀ (zero_lt_iff.mpr v_π_ne_zero)
        v_π_lt_one]

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

Goal state before:
pp: case pos
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsDiscreteValuationRing A
x : A
hx : x = 0
⊢ (maximalIdeal A).intValuation x = (ENat.recTopCoe 0 (fun x ↦ ↑(ofAdd ↑x)) ((addVal A) x))⁻¹

Tactic:
simp [hx]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: e : ℤ ≃+ ℤ
this : e 1 = 1 ∨ -e 1 = 1
⊢ e = AddEquiv.refl ℤ ∨ e = AddEquiv.neg ℤ

Tactic:
simpa [AddEquiv.ext_int_iff, neg_eq_iff_eq_neg]

Goal state after:
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✝ : ↥(closure {y})
⊢ 1 ∈ closure {x}

Tactic:
simp [hx]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

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

Tactic:
have := Subgroup.cyclic_of_min h

Goal state after:
case mp
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a b : G
h : IsLeast {y | y ∈ closure {a} ∧ 1 < y} b
this : closure {a} = closure {b}
⊢ b = |a|ₘ ∧ 1 < b
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : (ofClass v).ValueGroup₀ := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := extensionValuation x
hγ₀_def : γ₀ = extensionValuation x
heq : γ₀ = embedding γ₀'
this : γ₀ ≠ 0 → (x ∈ closure (Completion.coe' '' {x | v x < ↑γ}) ↔ γ₀ < ↑γ)
h : γ₀ ≠ 0
⊢ x ∈ closure (Completion.coe' '' {x | v x < ↑γ}) ↔ x ∈ {x | extensionValuation x < ↑γ}

Tactic:
· exact this h

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
⊢ ({x | x ≤ g}.WellFoundedOn fun x1 x2 ↦ x1 > x2) ↔ Nonempty (G₀ ≃*o WithZero (Multiplicative ℤ))

Tactic:
have hg' : g⁻¹ ≠ 0 := by simp [hg]

Goal state after:
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
⊢ ({x | x ≤ g}.WellFoundedOn fun x1 x2 ↦ x1 > x2) ↔ Nonempty (G₀ ≃*o WithZero (Multiplicative ℤ))
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 Γ₀
⊢ extensionValuation.restrict ↑⋯.choose = 1

Tactic:
apply_fun embedding using embedding_injective
    simpa using (restrict₀_surjective (.ofClass hv.v) 1).choose_spec

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

Goal state before:
pp: case h₀
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ ∀ b ∈ antidiagonal (d + n), b ≠ (d, n) → (coeff b.1) p * (coeff b.2) (X ^ n) = 0

pp: case h₁
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (d, n) ∉ antidiagonal (d + n) → (coeff (d, n).1) p * (coeff (d, n).2) (X ^ n) = 0

Tactic:
· rintro ⟨i, j⟩ h1 h2
    rw [coeff_X_pow, if_neg, mul_zero]
    rintro rfl
    apply h2
    rw [mem_antidiagonal, add_right_cancel_iff] at h1
    subst h1
    rfl

Goal state after:
case h₁
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (d, n) ∉ antidiagonal (d + n) → (coeff (d, n).1) p * (coeff (d, n).2) (X ^ n) = 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

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

Tactic:
Associates.count_mul (Associates.mk_ne_zero'.mpr hx) (Associates.mk_ne_zero'.mpr hy)
          v.associates_irreducible,

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
⊢ exp
      (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors +
            (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)) =
    exp
      (-(↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors) +
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)))
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : DecidableEq σ
s t : σ
⊢ (coeff (single t 1)) (X s) = if t = s then 1 else 0

Tactic:
by
  simp only [coeff_X, single_left_inj (one_ne_zero : (1 : ℕ) ≠ 0)]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
f g : R⟦X⟧
⊢ (mk fun n ↦ a ^ n * (coeff n) (f * g)) = (mk fun n ↦ a ^ n * (coeff n) f) * mk fun n ↦ a ^ n * (coeff n) g

Tactic:
by
    ext
    rw [PowerSeries.coeff_mul, PowerSeries.coeff_mk, PowerSeries.coeff_mul, Finset.mul_sum]
    apply sum_congr rfl
    simp only [coeff_mk, Prod.forall, mem_antidiagonal]
    intro b c H
    rw [← H, pow_add, mul_mul_mul_comm]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
S : Type u_3
inst✝³ : CommSemiring A
inst✝² : Algebra A R
inst✝¹ : CommSemiring S
inst✝ : Algebra A S
φ : R →ₐ[A] S
a : A
f : R⟦X⟧
⊢ (rescale ((algebraMap A S) a)) ((map ↑φ) f) = (map ↑φ) ((rescale ((algebraMap A R) a)) f)

Tactic:
by
  convert! rescale_map (φ : R →+* S) _ _
  simp

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

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
k n : ℕ
φ : R⟦X⟧
h₁ : ∀ (i : ℕ), Function.const ℕ φ i = φ
h₂ : ∀ (i : ℕ), ∏ j ∈ range i, Function.const ℕ φ j = φ ^ i
⊢ (coeff n) (∏ j ∈ range k, Function.const ℕ (Function.const ℕ φ k) j) =
    ∑ l ∈ (range k).finsuppAntidiag n, ∏ i ∈ range k, (coeff (l i)) (Function.const ℕ φ k)

Tactic:
apply coeff_prod (f := Function.const ℕ φ) (d := n) (s := range k)

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : (i, j).1 = single s n
⊢ False

Tactic:
apply H

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : (i, j).1 = single s n
⊢ m - single s n + single s n = m
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
γ : (ofClass v).ValueGroup₀ˣ
hx0 : ¬x = 0
y : K := ⋯.choose
hy_def : y = ⋯.choose
⊢ ↑⟨Units.mk0 ((ofClass extensionValuation) x) ⋯, ⋯⟩ < valueGroup₀_equiv_extensionValuation ↑γ ↔ extension x < ↑γ

Tactic:
have hy := (restrict₀_surjective (.ofClass hv.v) γ).choose_spec

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
γ : (ofClass v).ValueGroup₀ˣ
hx0 : ¬x = 0
y : K := ⋯.choose
hy_def : y = ⋯.choose
hy : (restrict₀ (ofClass v)) ⋯.choose = ↑γ
⊢ ↑⟨Units.mk0 ((ofClass extensionValuation) x) ⋯, ⋯⟩ < valueGroup₀_equiv_extensionValuation ↑γ ↔ extension 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) = r • e.prod fun s e ↦ MvPowerSeries.X s ^ e

Tactic:
LinearMap.CompatibleSMul.map_smul,

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

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

pp: 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

Tactic:
· rw [if_pos h, coeff_truncTotal _ h]

Goal state after:
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.Topology.Instances.ENat

Goal state before:
pp: x : ℕ∞
s : Set ℕ∞
hx : x ≠ ⊤
⊢ s ∈ 𝓝 x ↔ x ∈ s

Tactic:
simp [hx]

Goal state after:
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
n : (WithZero (Multiplicative ℤ))ˣ
x✝ : ∃ a, ¬(valuation K v) a = 0 ∧ ∃ x, (valuation K v) a * ↑n = (valuation K v) x
a : K
ha0 : ¬(valuation K v) a = 0
x : K
hx : (valuation K v) a * ↑n = (valuation K v) x
⊢ ¬Valued.v { toCompletion := ↑((WithVal.equiv (valuation K v)).symm a) } = 0

Tactic:
by simpa using ha0

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Continuum

Goal state before:
pp: ⊢ ℵ_ 1 ≤ 𝔠

Tactic:
rw [← succ_aleph0]

Goal state after:
⊢ Order.succ ℵ₀ ≤ 𝔠
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case inr
s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
n : ℕ
hn : n ≠ 0
⊢ term f s n = f n / ↑n ^ s

Tactic:
· rw [term_of_ne_zero hn]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (n : ℕ), ∀ᶠ (i : ι) in cofinite, (f i) n = 1 n
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
⊢ ∀ (i : ℕ),
    Tendsto (fun p ↦ ((DFunLike.coe ∘ fun s ↦ ∏ b ∈ s, f b) p.1, (DFunLike.coe ∘ fun s ↦ ∏ b ∈ s, f b) p.2))
      (atTop ×ˢ atTop) (comap (fun a ↦ (a.1 i, a.2 i)) (𝓟 SetRel.id))

Tactic:
tendsto_comap_iff,

Goal state after:
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (n : ℕ), ∀ᶠ (i : ι) in cofinite, (f i) n = 1 n
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
⊢ ∀ (i : ℕ),
    Tendsto
      ((fun a ↦ (a.1 i, a.2 i)) ∘ fun p ↦
        ((DFunLike.coe ∘ fun s ↦ ∏ b ∈ s, f b) p.1, (DFunLike.coe ∘ fun s ↦ ∏ b ∈ s, f b) p.2))
      (atTop ×ˢ atTop) (𝓟 SetRel.id)
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
x : E
⊢ egauge 𝕜 s x / ‖c‖ₑ ≤ egauge 𝕜 (c • s) x

Tactic:
le_egauge_iff,

Goal state after:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
x : E
⊢ ∀ (c_1 : 𝕜), x ∈ c_1 • c • s → egauge 𝕜 s x / ‖c‖ₑ ≤ ‖c_1‖ₑ
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: case succ.zero.ha
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
⊢ ∀ (x : ℕ), x ≠ 1 → (coeff x) P • (coeff (0 + 1)) ((∑ i, C (P.substInvFun ↑i) * X ^ ↑i) ^ x) = 0

Tactic:
· rintro (_ | _ | _) _ <;> simp_all [substInvFun, mul_pow, coeff_mul_X_pow']

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

Goal state before:
pp: R : Type u
E : Type v
inst✝² : AddCommGroup E
inst✝¹ : SMul R E
inst✝ : TopologicalSpace E
s : Set E
x y : E
α : Type u_1
l : Filter α
c : α → R
d : α → E
hd₀ : Tendsto d l (𝓝 0)
hds✝ : ∃ᶠ (n : α) in l, x + d n ∈ s
hds : (l ⊓ 𝓟 {x_1 | x + d x_1 ∈ s}).NeBot
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
this : Tendsto (fun n ↦ c n • d n) (l ⊓ 𝓟 {y | x + d y ∈ s}) (⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0)
⊢ y ∈ tangentConeAt R s x

Tactic:
tangentConeAt_def

Goal state after:
R : Type u
E : Type v
inst✝² : AddCommGroup E
inst✝¹ : SMul R E
inst✝ : TopologicalSpace E
s : Set E
x y : E
α : Type u_1
l : Filter α
c : α → R
d : α → E
hd₀ : Tendsto d l (𝓝 0)
hds✝ : ∃ᶠ (n : α) in l, x + d n ∈ s
hds : (l ⊓ 𝓟 {x_1 | x + d x_1 ∈ s}).NeBot
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
this : Tendsto (fun n ↦ c n • d n) (l ⊓ 𝓟 {y | x + d y ∈ s}) (⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0)
⊢ y ∈ {y | ClusterPt y (⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0)}
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
𝕜' : Type u_3
inst✝³ : Monoid 𝕜'
inst✝² : SMul 𝕜 𝕜'
inst✝¹ : MulAction 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
y : E
hy : ClusterPt y (⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0)
⊢ (⊤ • 1) • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0 ≤ ⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0

Tactic:
grw [le_top (a := ⊤ • 1)]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f f₁ : E → F
x : E
s : Set E
hs : f₁ =ᶠ[𝓝[insert x s] x] f
⊢ fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x

Tactic:
apply Filter.EventuallyEq.fderivWithin_eq (nhdsWithin_mono _ (subset_insert x s) hs)
  exact (mem_of_mem_nhdsWithin (mem_insert x s) hs :)

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
c : F
⊢ (fderiv 𝕜 fun x ↦ c) = 0

Tactic:
by
  rw [← fderivWithin_univ, fderivWithin_fun_const]

Goal state after: