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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
⊢ W.Nonsingular (W.neg P)

Tactic:
by
  by_cases hPz : P z = 0
  · simp only [neg_of_Z_eq_zero hP hPz, nonsingular_smul _
        ((isUnit_Y_of_Z_eq_zero hP hPz).div <| isUnit_X_of_Z_eq_zero hP hPz).neg, nonsingular_zero]
  · simp only [neg_of_Z_ne_zero hPz, nonsingular_smul _ <| Ne.isUnit hPz,
      nonsingular_neg_of_Z_ne_zero hP hPz]

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

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.negAddY P (W'.neg P) + -2 * P z ^ 3 * (P y - W'.negY P) * 0 -
      (W'.dblZ P ^ 3 +
        -2 * P z ^ 3 * (P y - W'.negY P) *
          (P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
            (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6))) =
    0

Tactic:
rw [negAddY, neg_X, neg_Y, neg_Z, dblZ, negY]; ring1

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
⊢ ∀ (x₀ : A) {U : Set A}, U ∈ {U | ∃ i, U = ↑(B i)} → ∃ V ∈ {U | ∃ i, U = ↑(B i)}, V ⊆ (fun x ↦ x₀ * x) ⁻¹' U

Tactic:
rintro x₀ _ ⟨i, rfl⟩
    obtain ⟨k, hk⟩ := hB.leftMul x₀ i
    use B k
    constructor
    · use k
    · exact hk

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
B : ι → Submodule R M
hB : BR.SubmodulesBasis B
x✝ : TopologicalSpace R := BR.topology
this : TopologicalSpace R := BR.topology
m : M
i : ι
V : Set R
V_in : V ∈ BR
hV : V ⊆ (fun x ↦ x • m) ⁻¹' ↑(B i)
⊢ ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i

Tactic:
exact mem_of_superset (BR.toAddGroupFilterBasis.mem_nhds_zero V_in) hV

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
⊢ ∀ {x y z : R × ↥(posSubmonoid R)},
    (match x with
      | (x, s) =>
        match y with
        | (y, t) => x * ↑t ≤ᵥ y * ↑s ∧ y * ↑s ≤ᵥ x * ↑t) →
      (match y with
        | (x, s) =>
          match z with
          | (y, t) => x * ↑t ≤ᵥ y * ↑s ∧ y * ↑s ≤ᵥ x * ↑t) →
        match x with
        | (x, s) =>
          match z with
          | (y, t) => x * ↑t ≤ᵥ y * ↑s ∧ y * ↑s ≤ᵥ x * ↑t

Tactic:
by
      rintro ⟨r, u⟩ ⟨s, v⟩ ⟨t, w⟩ ⟨h1, h2⟩ ⟨h3, h4⟩
      constructor
      · have := mul_vle_mul h1 (vle_refl ↑w)
        grw [veq_mul_right_comm (x := s)] at this
        have := vle_trans this (mul_vle_mul h3 (vle_refl _))
        grw [veq_mul_right_comm r, veq_mul_right_comm t] at this
        simpa using this
      · have := mul_vle_mul h4 (vle_refl ↑u)
        grw [veq_mul_right_comm s] at this
        have := vle_trans this (mul_vle_mul h2 (vle_refl _))
        grw [veq_mul_right_comm t, veq_mul_right_comm r] at this
        simpa using this

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ a : R
x : ↥(posSubmonoid R)
ha : 0 < ValueGroupWithZero.mk a x
b : R
y : ↥(posSubmonoid R)
c : R
z : ↥(posSubmonoid R)
hbc : ValueGroupWithZero.mk b y < ValueGroupWithZero.mk c z
⊢ a * ↑x * (b * ↑z) <ᵥ a * c * (↑x * ↑y)

Tactic:
veq_mul_mul_mul_comm _ c

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ a : R
x : ↥(posSubmonoid R)
ha : 0 < ValueGroupWithZero.mk a x
b : R
y : ↥(posSubmonoid R)
c : R
z : ↥(posSubmonoid R)
hbc : ValueGroupWithZero.mk b y < ValueGroupWithZero.mk c z
⊢ a * ↑x * (b * ↑z) <ᵥ a * ↑x * (c * ↑y)
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : Ring B
inst✝⁴ : ValuativeRel A
inst✝³ : ValuativeRel B
inst✝² : Algebra A B
inst✝¹ : ValuativeExtension A B
inst✝ : IsRankLeOne B
f : ValueGroupWithZero B →*₀ NNReal
hf : StrictMono ⇑f
⊢ IsRankLeOne A

Tactic:
exact ⟨⟨f.comp (mapValueGroupWithZero _ _), hf.comp mapValueGroupWithZero_strictMono⟩⟩

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
H : ∀ (P : Ideal R), P.IsPrime → Submodule.IsPrincipal P
⊢ IsPrincipalIdealRing R

Tactic:
by
  refine ⟨isOka_isPrincipal.forall_of_forall_prime (fun I hI ↦ exists_maximal_not_isPrincipal ?_) H⟩
  rw [isPrincipalIdealRing_iff, not_forall]
  exact ⟨I, hI⟩

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

Goal state before:
pp: case hH.ofNat
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✝
π : A
hπ : v π = (exp 1)⁻¹
n : ℕ
h : Units.mk0 (exp 1)⁻¹ ⋯ ^ Int.ofNat n = n✝
⊢ ∃ a,
    ¬(MonoidWithZeroHom.ofClass v) a = 0 ∧
      ∃ x, (MonoidWithZeroHom.ofClass v) a * ↑(Units.mk0 (exp 1)⁻¹ ⋯ ^ Int.ofNat n) = (MonoidWithZeroHom.ofClass v) x

Tactic:
| ofNat n =>

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 Γ₀
hv : Valued K Γ₀
x : K
h : x ≠ 0
v_ne : v.restrict x ≠ 0
⊢ v x ≠ 0

Tactic:
simpa [restrict₀_apply] using v_ne

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

Goal state before:
pp: case h.left
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
H₀ : ∀ x ∈ M₀, ↑γ₀ ≤ v.restrict x
γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
H₁ : ∀ x ∈ M₁, ∀ y ∈ M₁, v.restrict (y - x) < ↑(min (γ * γ₀ * γ₀) γ₀)
⊢ (fun x ↦ x⁻¹) '' (M₀ ∩ M₁) ∈ map (fun x ↦ x⁻¹) F

pp: case h.right
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
H₀ : ∀ x ∈ M₀, ↑γ₀ ≤ v.restrict x
γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
H₁ : ∀ x ∈ M₁, ∀ y ∈ M₁, v.restrict (y - x) < ↑(min (γ * γ₀ * γ₀) γ₀)
⊢ ∀ x ∈ (fun x ↦ x⁻¹) '' (M₀ ∩ M₁), ∀ y ∈ (fun x ↦ x⁻¹) '' (M₀ ∩ M₁), v.restrict (y - x) < ↑γ

Tactic:
· rw [mem_map]
        apply mem_of_superset (Filter.inter_mem M₀_in M₁_in)
        exact subset_preimage_image _ _

Goal state after:
case h.right
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
H₀ : ∀ x ∈ M₀, ↑γ₀ ≤ v.restrict x
γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
H₁ : ∀ x ∈ M₁, ∀ y ∈ M₁, v.restrict (y - x) < ↑(min (γ * γ₀ * γ₀) γ₀)
⊢ ∀ x ∈ (fun x ↦ x⁻¹) '' (M₀ ∩ M₁), ∀ y ∈ (fun x ↦ x⁻¹) '' (M₀ ∩ M₁), v.restrict (y - x) < ↑γ
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case h.a₁
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
h₁ : ∃ r₁, (algebraMap R K) r₁ = W.a₁
h₂ : ∃ r₂, (algebraMap R K) r₂ = W.a₂
h₃ : ∃ r₃, (algebraMap R K) r₃ = W.a₃
h₄ : ∃ r₄, (algebraMap R K) r₄ = W.a₄
h₆ : ∃ r₆, (algebraMap R K) r₆ = W.a₆
⊢ W.a₁ = (algebraMap R K) h₁.choose

Tactic:
apply h₁.choose_spec.symm

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
⊢ Nonempty (G ≃*o Multiplicative ℤ) ↔ ¬DenselyOrdered G

Tactic:
let e : G ≃o Additive G := .refl G
  rw [← OrderAddMonoidIso.toMultiplicativeRight.nonempty_congr,
    LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered,
    denselyOrdered_iff_of_orderIsoClass e]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_5
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
h : {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
a✝¹ : G₀
a✝ : g ≤ a✝¹
⊢ ¬a✝¹ = 0 →
    ∀ (b : G₀),
      g ≤ b → ¬b = 0 → a✝¹ < b → (if h : a✝¹ = 0 then 1 else Units.mk0 a✝¹ h) < if h : b = 0 then 1 else Units.mk0 b h

Tactic:
ha0

Goal state after:
case refine_5
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
h : {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
a✝¹ : G₀
a✝ : g ≤ a✝¹
ha0 : ¬a✝¹ = 0
⊢ ∀ (b : G₀),
    g ≤ b → ¬b = 0 → a✝¹ < b → (if h : a✝¹ = 0 then 1 else Units.mk0 a✝¹ h) < if h : b = 0 then 1 else Units.mk0 b h
Module: Mathlib.RingTheory.PowerSeries.Basic

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

Tactic:
intro n

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) (φ * X) = (coeff n) (ψ * X)
n : ℕ
⊢ (coeff n) φ = (coeff n) ψ
Module: Mathlib.RingTheory.PowerSeries.Basic

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

Tactic:
intro n

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) (X * φ) = (coeff n) (X * ψ)
n : ℕ
⊢ (coeff n) φ = (coeff n) ψ
Module: Mathlib.RingTheory.PowerSeries.Basic

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

Tactic:
intro n

Goal state after:
R : Type u_1
inst✝ : Semiring R
k : ℕ
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) (φ * X ^ k) = (coeff n) (ψ * X ^ k)
n : ℕ
⊢ (coeff n) φ = (coeff n) ψ
Module: Mathlib.RingTheory.PowerSeries.Basic

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

Tactic:
intro n

Goal state after:
R : Type u_1
inst✝ : Semiring R
k : ℕ
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) (X ^ k * φ) = (coeff n) (X ^ k * ψ)
n : ℕ
⊢ (coeff n) φ = (coeff n) ψ
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
s : σ
h : single s 1 ≤ 0
⊢ False

Tactic:
simpa using h s

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
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)
    ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)
h_dvd_x : x ∈ v.asIdeal ^ nmin
h_dvd_y : y ∈ v.asIdeal ^ nmin
⊢ x + y ∈ v.asIdeal ^ nmin

Tactic:
exact Ideal.add_mem (v.asIdeal ^ nmin) h_dvd_x h_dvd_y

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

Goal state before:
pp: case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff (l i)) (f i)
d : σ →₀ ℕ
⊢ ∑ p ∈ antidiagonal d, (coeff p.1) (f a) * (coeff p.2) (∏ x ∈ s, f x) =
    ∑ x ∈ antidiagonal d,
      ∑ i ∈ Finset.map { toFun := fun f ↦ (↑f).update a x.1, inj' := ⋯ } (s.finsuppAntidiag x.2).attach,
        ∏ i_1 ∈ insert a s, (coeff (i i_1)) (f i_1)

Tactic:
apply Finset.sum_congr rfl
      simp only [mem_antidiagonal, sum_map, Function.Embedding.coeFn_mk, coe_update, Prod.forall]
      rintro u v rfl
      rw [ih, Finset.mul_sum, ← Finset.sum_attach]
      apply Finset.sum_congr rfl
      simp only [mem_attach, Finset.prod_insert ha, Function.update_self, forall_true_left,
        Subtype.forall]
      rintro x -
      rw [Finset.prod_congr rfl]
      intro i hi
      rw [Function.update_of_ne]
      exact ne_of_mem_of_not_mem hi ha

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
⊢ (coeff 1) (φ ^ (n' + 1)) = ↑(n' + 1) * (coeff 1) φ * constantCoeff φ ^ (n' + 1 - 1)

Tactic:
have h₁ (m : ℕ) : φ ^ (m + 1) = φ ^ m * φ := by exact rfl
      have h₂ : Finset.antidiagonal 1 = {(0, 1), (1, 0)} := by exact rfl
      rw [h₁, coeff_mul, h₂, Finset.sum_insert, Finset.sum_singleton]
      · simp only [coeff_zero_eq_constantCoeff, map_pow, Nat.cast_add, Nat.cast_one,
          add_tsub_cancel_right]
        have h₀ : n' = 0 ∨ 1 ≤ n' := by lia
        rcases h₀ with h' | h'
        · by_contra h''
          rw [h'] at h''
          simp only [pow_zero, one_mul, coeff_one, one_ne_zero, ↓reduceIte, zero_mul, add_zero,
            mul_one] at h''
          norm_num at h''
        · rw [ih]
          · conv => lhs; arg 2; rw [mul_comm, ← mul_assoc]
            move_mul [← constantCoeff φ ^ (n' - 1)]
            conv => enter [1, 2, 1, 1, 2]; rw [← pow_one (a := constantCoeff φ)]
            rw [← pow_add (a := constantCoeff φ)]
            conv => enter [1, 2, 1, 1]; rw [Nat.sub_add_cancel h']
            ring
          exact h'
      · decide

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

Goal state before:
pp: case neg.left
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ∃ d_1, (coeff d_1) ((monomial d) a) ≠ 0 ∧ (weight w) d_1 = (weight w) d

pp: case neg.right
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ∀ (d_1 : σ →₀ ℕ), (weight w) d_1 < (weight w) d → (coeff d_1) ((monomial d) a) = 0

Tactic:
· use d
      simp only [coeff_monomial_same, ne_eq, h, not_false_eq_true, and_self]

Goal state after:
case neg.right
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ∀ (d_1 : σ →₀ ℕ), (weight w) d_1 < (weight w) d → (coeff d_1) ((monomial d) a) = 0
Module: Mathlib.Data.Finsupp.Interval

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Zero α
f✝ : ι →₀ α
i✝ : ι
a : α
f : ι →₀ α
i : ι
⊢ i ∈ f.support ↔ {f i} ≠ 0

Tactic:
by
    rw [← not_iff_not, notMem_support_iff, not_ne_iff]
    exact singleton_injective.eq_iff.symm

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
x : σ →₀ ℕ
r : R
h : x ∈ s
⊢ (truncFinset R s) ((monomial x) r) = (MvPolynomial.monomial x) r

Tactic:
classical
  ext
  grind [coeff_monomial, MvPolynomial.coeff_monomial]

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

Goal state before:
pp: σ : Type u_1
w : σ → ℕ
R : Type u_3
inst✝ : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w g
⊢ (coeff d) (f * (1 - g)) = (coeff d) f

Tactic:
by
  simp only [mul_sub, mul_one, map_sub, sub_eq_self]
  apply coeff_eq_zero_of_lt_weightedOrder w
  exact lt_of_lt_of_le (lt_of_lt_of_le h le_add_self) (le_weightedOrder_mul w)

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

Goal state before:
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:
if_neg 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) = 0
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: ⊢ ∀ (n : ℕ), ∀ᶠ (a : ℕ) in atTop, ↑n < ↑a

Tactic:
intro n

Goal state after:
n : ℕ
⊢ ∀ᶠ (a : ℕ) in atTop, ↑n < ↑a
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: case ind
σ : 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
⊢ MvPolynomial.coeff x ((truncTotal n) p ^ k.succ) = (coeff x) (p ^ k.succ)

Tactic:
simp_rw [Nat.succ_eq_add_one, pow_add, pow_one, MvPolynomial.coeff_mul, coeff_mul]
    congr! 2 with _ _
    · exact ih _ k.le_refl (by grind [mem_antidiagonal])
    · 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_3
inst✝ : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑((weight fun x ↦ 1) d) < g.order
⊢ (coeff d) ((1 - g) * f) = (coeff d) f

Tactic:
exact coeff_mul_right_one_sub_of_lt_weightedOrder _ h

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace R
inst✝² : DecidableEq σ
inst✝¹ : CommSemiring R
inst✝ : Nonempty σ
f : MvPowerSeries σ R
d : σ →₀ ℕ
s : σ
h✝ : True
⊢ ∀ i ≥ d + Finsupp.single s 1, (coeff d) ↑((trunc R i) f) = (coeff d) f

Tactic:
intro n

Goal state after:
σ : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace R
inst✝² : DecidableEq σ
inst✝¹ : CommSemiring R
inst✝ : Nonempty σ
f : MvPowerSeries σ R
d : σ →₀ ℕ
s : σ
h✝ : True
n : σ →₀ ℕ
⊢ n ≥ d + Finsupp.single s 1 → (coeff d) ↑((trunc R n) f) = (coeff d) f
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
⊢ ∀ (i : ℕ), ↑i < φ.order + ψ.order → (coeff i) (φ * ψ) = 0

Tactic:
intro n

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
⊢ ↑n < φ.order + ψ.order → (coeff n) (φ * ψ) = 0
Module: Mathlib.RingTheory.PowerSeries.PiTopology

Goal state before:
pp: R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
⊢ Summable f ↔ ∀ (d : ℕ), Summable fun i ↦ (coeff d) (f i)

Tactic:
simp_rw [Summable, hasSum_iff_hasSum_coeff]
  constructor
  · rintro ⟨a, h⟩ n
    exact ⟨coeff n a, h n⟩
  · intro h
    choose a h using h
    exact ⟨mk a, by simpa using h⟩

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

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
h : Tendsto (fun i ↦ (f i).order) atTop (𝓝 ⊤)
hempty : Nonempty ι
⊢ ∀ (d : ℕ), Summable fun i ↦ (coeff d) (f i)

Tactic:
intro n

Goal state after:
case inr
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
h : Tendsto (fun i ↦ (f i).order) atTop (𝓝 ⊤)
hempty : Nonempty ι
n : ℕ
⊢ Summable fun i ↦ (coeff n) (f i)
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R⟦X⟧
h : f ≠ 0 ∧ g ≠ 0
⊢ f.divXPowOrder * g.divXPowOrder * X ^ (g.order.toNat + f.order.toNat) =
    X ^ (f.order.toNat + g.order.toNat) * (f.divXPowOrder * g.divXPowOrder)

Tactic:
by
        rw [X_pow_mul, add_comm]

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

Goal state before:
pp: case h
σ : Type u_1
R : Type u_3
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsLinearTopology R R
f : MvPowerSeries σ R
d : σ →₀ ℕ
I : Ideal R
hI : ↑I ∈ 𝓝 0
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → constantCoeff ((map (Ideal.Quotient.mk I)) f) ^ b = 0
⊢ ∀ (b : ℕ), N + Finsupp.degree d ≤ b → (coeff d) ((map (Ideal.Quotient.mk I)) (f ^ b)) = 0

Tactic:
intro n

Goal state after:
case h
σ : Type u_1
R : Type u_3
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsLinearTopology R R
f : MvPowerSeries σ R
d : σ →₀ ℕ
I : Ideal R
hI : ↑I ∈ 𝓝 0
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → constantCoeff ((map (Ideal.Quotient.mk I)) f) ^ b = 0
n : ℕ
⊢ N + Finsupp.degree d ≤ n → (coeff d) ((map (Ideal.Quotient.mk I)) (f ^ n)) = 0
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
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ha : HasEval a
r : R
⊢ eval₂ (algebraMap R S) a (C r) = (algebraMap R S) r

Tactic:
eval₂_C

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✝⁸ : IsTopologicalSemiring R
inst✝⁷ : IsUniformAddGroup R
inst✝⁶ : IsUniformAddGroup S
inst✝⁵ : CompleteSpace S
inst✝⁴ : T2Space S
inst✝³ : IsTopologicalRing S
inst✝² : IsLinearTopology S S
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ha : HasEval a
r : R
⊢ (algebraMap R S) r = (algebraMap R S) r
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝⁶ : CommRing R
τ : Type u_4
S : Type u_5
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
a : σ → MvPowerSeries τ S
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
ha : HasSubst a
⊢ ⇑(substAlgHom ha) = ⇑(aeval ⋯)

Tactic:
simp only [substAlgHom, coe_aeval ha.hasEval]

Goal state after:
σ : 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
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
ha : HasSubst a
⊢ ⇑(aeval ⋯) = eval₂ (algebraMap R (MvPowerSeries τ S)) a
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ ∀ (b : ℕ), cantorFunctionAux c f b = 0 ∨ cantorFunctionAux c f b = c ^ b

Tactic:
intro n

Goal state after:
c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
⊢ cantorFunctionAux c f n = 0 ∨ cantorFunctionAux c f n = c ^ n
Module: Mathlib.Analysis.Real.Cardinality

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

Tactic:
intro n

Goal state after:
c : ℝ
f g : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
n : ℕ
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n ↦ rec false (fun x x_1 ↦ true) n
⊢ ∀ (n : ℕ), f n = true → f_max n = true

Tactic:
intro n

Goal state after:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n ↦ rec false (fun x x_1 ↦ true) n
n : ℕ
⊢ f n = true → f_max n = true
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n ↦ rec false (fun x x_1 ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n ↦ rec true (fun x x_1 ↦ false) n
⊢ ∀ (n : ℕ), g_min n = true → g n = true

Tactic:
intro n

Goal state after:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n ↦ rec false (fun x x_1 ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n ↦ rec true (fun x x_1 ↦ false) n
n : ℕ
⊢ g_min n = true → g n = true