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

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
⊢ (W'.map f).a₁ * (⇑f ∘ P) y * (⇑f ∘ P) z -
      (3 * (⇑f ∘ P) x ^ 2 + 2 * (W'.map f).a₂ * (⇑f ∘ P) x * (⇑f ∘ P) z ^ 2 + (W'.map f).a₄ * (⇑f ∘ P) z ^ 4) =
    f (W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4))

Tactic:
map_simp

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

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
⊢ (⇑f ∘ P) z * ((⇑f ∘ P) y - (-(⇑f ∘ P) y - (W'.map f).a₁ * (⇑f ∘ P) x * (⇑f ∘ P) z - (W'.map f).a₃ * (⇑f ∘ P) z ^ 3)) =
    f (P z * (P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3)))

Tactic:
map_simp

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

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
⊢ f (W'.dblU P) ^ 2 - (W'.map f).a₁ * f (W'.dblU P) * (⇑f ∘ P) z * ((⇑f ∘ P) y - f (W'.negY P)) -
        (W'.map f).a₂ * (⇑f ∘ P) z ^ 2 * ((⇑f ∘ P) y - f (W'.negY P)) ^ 2 -
      2 * (⇑f ∘ P) x * ((⇑f ∘ P) y - f (W'.negY P)) ^ 2 =
    f
      (W'.dblU P ^ 2 - W'.a₁ * W'.dblU P * P z * (P y - W'.negY P) - W'.a₂ * P z ^ 2 * (P y - W'.negY P) ^ 2 -
        2 * P x * (P y - W'.negY P) ^ 2)

Tactic:
map_simp

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

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
⊢ -f (W'.negDblY P) - (W'.map f).a₁ * f (W'.dblX P) * f (W'.dblZ P) - (W'.map f).a₃ * f (W'.dblZ P) ^ 3 =
    f (-W'.negDblY P - W'.a₁ * W'.dblX P * W'.dblZ P - W'.a₃ * W'.dblZ P ^ 3)

Tactic:
map_simp

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

Goal state before:
pp: F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
⊢ -(((⇑f ∘ P) y * (⇑f ∘ Q) z ^ 3 - (⇑f ∘ Q) y * (⇑f ∘ P) z ^ 3) / ((⇑f ∘ P) z * (⇑f ∘ Q) z)) =
    f (-((P y * Q z ^ 3 - Q y * P z ^ 3) / (P z * Q z)))

Tactic:
map_simp

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

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
P Q : Fin 3 → R
⊢ (⇑f ∘ P) x * (⇑f ∘ Q) z ^ 2 - (⇑f ∘ Q) x * (⇑f ∘ P) z ^ 2 = f (P x * Q z ^ 2 - Q x * P z ^ 2)

Tactic:
map_simp

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

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Jacobian R
f : R →+* S
P Q : Fin 3 → R
⊢ (⇑f ∘ P) x * (⇑f ∘ Q) x ^ 2 * (⇑f ∘ P) z ^ 2 - 2 * (⇑f ∘ P) y * (⇑f ∘ Q) y * (⇑f ∘ P) z * (⇑f ∘ Q) z +
                      (⇑f ∘ P) x ^ 2 * (⇑f ∘ Q) x * (⇑f ∘ Q) z ^ 2 -
                    (W'.map f).a₁ * (⇑f ∘ P) x * (⇑f ∘ Q) y * (⇑f ∘ P) z ^ 2 * (⇑f ∘ Q) z -
                  (W'.map f).a₁ * (⇑f ∘ P) y * (⇑f ∘ Q) x * (⇑f ∘ P) z * (⇑f ∘ Q) z ^ 2 +
                2 * (W'.map f).a₂ * (⇑f ∘ P) x * (⇑f ∘ Q) x * (⇑f ∘ P) z ^ 2 * (⇑f ∘ Q) z ^ 2 -
              (W'.map f).a₃ * (⇑f ∘ Q) y * (⇑f ∘ P) z ^ 4 * (⇑f ∘ Q) z -
            (W'.map f).a₃ * (⇑f ∘ P) y * (⇑f ∘ P) z * (⇑f ∘ Q) z ^ 4 +
          (W'.map f).a₄ * (⇑f ∘ Q) x * (⇑f ∘ P) z ^ 4 * (⇑f ∘ Q) z ^ 2 +
        (W'.map f).a₄ * (⇑f ∘ P) x * (⇑f ∘ P) z ^ 2 * (⇑f ∘ Q) z ^ 4 +
      2 * (W'.map f).a₆ * (⇑f ∘ P) z ^ 4 * (⇑f ∘ Q) z ^ 4 =
    f
      (P x * Q x ^ 2 * P z ^ 2 - 2 * P y * Q y * P z * Q z + P x ^ 2 * Q x * Q z ^ 2 -
                      W'.a₁ * P x * Q y * P z ^ 2 * Q z -
                    W'.a₁ * P y * Q x * P z * Q z ^ 2 +
                  2 * W'.a₂ * P x * Q x * P z ^ 2 * Q z ^ 2 -
                W'.a₃ * Q y * P z ^ 4 * Q z -
              W'.a₃ * P y * P z * Q z ^ 4 +
            W'.a₄ * Q x * P z ^ 4 * Q z ^ 2 +
          W'.a₄ * P x * P z ^ 2 * Q z ^ 4 +
        2 * W'.a₆ * P z ^ 4 * Q z ^ 4)

Tactic:
map_simp

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

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Jacobian R
f : R →+* S
P Q : Fin 3 → R
⊢ -(⇑f ∘ P) y * (⇑f ∘ Q) x ^ 3 * (⇑f ∘ P) z ^ 3 + 2 * (⇑f ∘ P) y * (⇑f ∘ Q) y ^ 2 * (⇑f ∘ P) z ^ 3 -
                                        3 * (⇑f ∘ P) x ^ 2 * (⇑f ∘ Q) x * (⇑f ∘ Q) y * (⇑f ∘ P) z ^ 2 * (⇑f ∘ Q) z +
                                      3 * (⇑f ∘ P) x * (⇑f ∘ P) y * (⇑f ∘ Q) x ^ 2 * (⇑f ∘ P) z * (⇑f ∘ Q) z ^ 2 +
                                    (⇑f ∘ P) x ^ 3 * (⇑f ∘ Q) y * (⇑f ∘ Q) z ^ 3 -
                                  2 * (⇑f ∘ P) y ^ 2 * (⇑f ∘ Q) y * (⇑f ∘ Q) z ^ 3 +
                                (W'.map f).a₁ * (⇑f ∘ P) x * (⇑f ∘ Q) y ^ 2 * (⇑f ∘ P) z ^ 4 +
                              (W'.map f).a₁ * (⇑f ∘ P) y * (⇑f ∘ Q) x * (⇑f ∘ Q) y * (⇑f ∘ P) z ^ 3 * (⇑f ∘ Q) z -
                            (W'.map f).a₁ * (⇑f ∘ P) x * (⇑f ∘ P) y * (⇑f ∘ Q) y * (⇑f ∘ P) z * (⇑f ∘ Q) z ^ 3 -
                          (W'.map f).a₁ * (⇑f ∘ P) y ^ 2 * (⇑f ∘ Q) x * (⇑f ∘ Q) z ^ 4 -
                        2 * (W'.map f).a₂ * (⇑f ∘ P) x * (⇑f ∘ Q) x * (⇑f ∘ Q) y * (⇑f ∘ P) z ^ 4 * (⇑f ∘ Q) z +
                      2 * (W'.map f).a₂ * (⇑f ∘ P) x * (⇑f ∘ P) y * (⇑f ∘ Q) x * (⇑f ∘ P) z * (⇑f ∘ Q) z ^ 4 +
                    (W'.map f).a₃ * (⇑f ∘ Q) y ^ 2 * (⇑f ∘ P) z ^ 6 -
                  (W'.map f).a₃ * (⇑f ∘ P) y ^ 2 * (⇑f ∘ Q) z ^ 6 -
                (W'.map f).a₄ * (⇑f ∘ Q) x * (⇑f ∘ Q) y * (⇑f ∘ P) z ^ 6 * (⇑f ∘ Q) z -
              (W'.map f).a₄ * (⇑f ∘ P) x * (⇑f ∘ Q) y * (⇑f ∘ P) z ^ 4 * (⇑f ∘ Q) z ^ 3 +
            (W'.map f).a₄ * (⇑f ∘ P) y * (⇑f ∘ Q) x * (⇑f ∘ P) z ^ 3 * (⇑f ∘ Q) z ^ 4 +
          (W'.map f).a₄ * (⇑f ∘ P) x * (⇑f ∘ P) y * (⇑f ∘ P) z * (⇑f ∘ Q) z ^ 6 -
        2 * (W'.map f).a₆ * (⇑f ∘ Q) y * (⇑f ∘ P) z ^ 6 * (⇑f ∘ Q) z ^ 3 +
      2 * (W'.map f).a₆ * (⇑f ∘ P) y * (⇑f ∘ P) z ^ 3 * (⇑f ∘ Q) z ^ 6 =
    f
      (-P y * Q x ^ 3 * P z ^ 3 + 2 * P y * Q y ^ 2 * P z ^ 3 - 3 * P x ^ 2 * Q x * Q y * P z ^ 2 * Q z +
                                        3 * P x * P y * Q x ^ 2 * P z * Q z ^ 2 +
                                      P x ^ 3 * Q y * Q z ^ 3 -
                                    2 * P y ^ 2 * Q y * Q z ^ 3 +
                                  W'.a₁ * P x * Q y ^ 2 * P z ^ 4 +
                                W'.a₁ * P y * Q x * Q y * P z ^ 3 * Q z -
                              W'.a₁ * P x * P y * Q y * P z * Q z ^ 3 -
                            W'.a₁ * P y ^ 2 * Q x * Q z ^ 4 -
                          2 * W'.a₂ * P x * Q x * Q y * P z ^ 4 * Q z +
                        2 * W'.a₂ * P x * P y * Q x * P z * Q z ^ 4 +
                      W'.a₃ * Q y ^ 2 * P z ^ 6 -
                    W'.a₃ * P y ^ 2 * Q z ^ 6 -
                  W'.a₄ * Q x * Q y * P z ^ 6 * Q z -
                W'.a₄ * P x * Q y * P z ^ 4 * Q z ^ 3 +
              W'.a₄ * P y * Q x * P z ^ 3 * Q z ^ 4 +
            W'.a₄ * P x * P y * P z * Q z ^ 6 -
          2 * W'.a₆ * Q y * P z ^ 6 * Q z ^ 3 +
        2 * W'.a₆ * P y * P z ^ 3 * Q z ^ 6)

Tactic:
map_simp

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

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Jacobian R
f : R →+* S
P Q : Fin 3 → R
⊢ -f (W'.negAddY P Q) - (W'.map f).a₁ * f (W'.addX P Q) * f (addZ P Q) - (W'.map f).a₃ * f (addZ P Q) ^ 3 =
    f (-W'.negAddY P Q - W'.a₁ * W'.addX P Q * addZ P Q - W'.a₃ * addZ P Q ^ 3)

Tactic:
map_simp

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

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
γ : (ofClass v).ValueGroup₀
hγ : γ ≠ 0
⊢ {x | v.restrict x < γ} ∈ 𝓝 0

Tactic:
Valued.mem_nhds_zero

Goal state after:
case inl
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
γ : (ofClass v).ValueGroup₀
hγ : γ ≠ 0
⊢ ∃ γ_1, {x | v.restrict x < ↑γ_1} ⊆ {x | v.restrict x < γ}
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
hsurj : Function.Surjective ⇑v
γ : Γ₀
hγ : γ ≠ 0
⊢ {x | v x < γ} ∈ 𝓝 0

Tactic:
Valued.mem_nhds_zero

Goal state after:
case inl
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
hsurj : Function.Surjective ⇑v
γ : Γ₀
hγ : γ ≠ 0
⊢ ∃ γ_1, {x | v.restrict x < ↑γ_1} ⊆ {x | v x < γ}
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case mp.inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
ha✝ : a ≠ 1
ha : a < 1
⊢ Function.Injective fun x ↦ a ^ x

pp: case mp.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
ha✝ : a ≠ 1
ha : 1 < a
⊢ Function.Injective fun x ↦ a ^ x

Tactic:
· exact (zpow_right_strictAnti ha).injective

Goal state after:
case mp.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
ha✝ : a ≠ 1
ha : 1 < a
⊢ Function.Injective fun x ↦ a ^ x
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: e : ℤ ≃+o ℤᵒᵈ
⊢ e.toAddEquiv =
    { toAddEquiv := (AddEquiv.neg ℤ).trans { toEquiv := toDual, map_add' := ⋯ },
        map_le_map_iff' := @instUniqueOrderAddMonoidIsoIntOrderDual._proof_1 }.toAddEquiv

Tactic:
simp only [OrderAddMonoidIso.toAddEquiv_eq_coe]

Goal state after:
e : ℤ ≃+o ℤᵒᵈ
⊢ ↑e = (AddEquiv.neg ℤ).trans { toEquiv := toDual, map_add' := ⋯ }
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

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

Goal state after:
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 Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
x : hat K
⊢ (fun x ↦ x * x₀⁻¹) ((fun x ↦ x * x₀) x) = x

Tactic:
simp only [mul_assoc, mul_inv_cancel₀ h, mul_one]

Goal state after:
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 ℤ)) ↔ Nonempty (Gˣ ≃*o Multiplicative ℤ)

Tactic:
refine Nonempty.congr ?_ ?_ <;> intro f

Goal state after:
case refine_1
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : G ≃*o WithZero (Multiplicative ℤ)
⊢ Gˣ ≃*o Multiplicative ℤ

case refine_2
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
⊢ 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 Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
nhds_right : (fun x ↦ x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : v.restrict z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑a = (fun x ↦ x * x₀) y
this : ↑z₀⁻¹ = (↑z₀)⁻¹
⊢ y * (x₀ * x₀⁻¹) * y₀⁻¹ ∈ V

Tactic:
mul_inv_cancel₀ h,

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
nhds_right : (fun x ↦ x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : v.restrict z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑a = (fun x ↦ x * x₀) y
this : ↑z₀⁻¹ = (↑z₀)⁻¹
⊢ y * 1 * y₀⁻¹ ∈ V
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_2
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
g : G
⊢ ({x | x ≤ g}.WellFoundedOn fun x1 x2 ↦ x1 > x2) ↔ Nonempty (G ≃*o Multiplicative ℤ)

Tactic:
← wellFoundedOn_setOfPred_le_lt_iff_nonempty_discrete (g := g⁻¹)

Goal state after:
G : Type u_2
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
g : G
⊢ ({x | x ≤ g}.WellFoundedOn fun x1 x2 ↦ x1 > x2) ↔ {x | g⁻¹ ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : k - n = m
h₃ : ¬k = m + n
⊢ a * b = 0

Tactic:
← h₂,

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : k - n = m
h₃ : ¬k = k - n + n
⊢ a * b = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a b : R
⊢ rescale (a * b) = (rescale b).comp (rescale a)

Tactic:
by
  ext
  simp [← rescale_rescale]

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) (φ ^ k) = ∑ l ∈ (range k).finsuppAntidiag n, ∏ i ∈ range k, (coeff (l i)) φ

Tactic:
← h₂,

Goal state after:
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 ℕ φ j) = ∑ l ∈ (range k).finsuppAntidiag n, ∏ i ∈ range k, (coeff (l i)) φ
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
x : K
⊢ (valuation K v) x = (v.intValuation.extendToLocalization ⋯ K) x

Tactic:
valuation

Goal state after:
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
x : K
⊢ (v.intValuation.extendToLocalization ⋯ K) x = (v.intValuation.extendToLocalization ⋯ K) x
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' - 1) * constantCoeff φ

Tactic:
2

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 φ
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
a b : R
hb : b ≠ 0
h : b ∈ v.asIdeal → a ∉ v.asIdeal
hv : b ∈ v.asIdeal
ha₀ : a ≠ 0
hva : (valuation K v) ↑a ≠ 0
hvb : (valuation K v) ↑b ≠ 0
⊢ log 1 < ((valuation K v) ↑a).log - ((valuation K v) ↑b).log

Tactic:
WithZero.log_one,

Goal state after:
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
a b : R
hb : b ≠ 0
h : b ∈ v.asIdeal → a ∉ v.asIdeal
hv : b ∈ v.asIdeal
ha₀ : a ≠ 0
hva : (valuation K v) ↑a ≠ 0
hvb : (valuation K v) ↑b ≠ 0
⊢ 0 < ((valuation K v) ↑a).log - ((valuation K v) ↑b).log
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R[X]
h : ↑x = ↑y
n✝ : ℕ
⊢ x.coeff n✝ = y.coeff n✝

Tactic:
simp_rw [← coeff_coe, h]

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
⊢ (coeff d) (f ^ n) = 0

Tactic:
by
  classical
  rw [coeff_pow]
  apply sum_eq_zero
  intro k hk
  rw [mem_finsuppAntidiag] at hk
  set s := {i ∈ range n | k i = 0} with hs_def
  have hs : s ⊆ range n := filter_subset _ _
  have hs' (i : ℕ) (hi : i ∈ s) : coeff (k i) f = constantCoeff f := by
    simp only [hs_def, mem_filter] at hi
    rw [hi.2, coeff_zero_eq_constantCoeff]
  have hs'' (i : ℕ) (hi : i ∈ s) : k i = 0 := by
    simp only [hs_def, mem_filter] at hi
    rw [hi.2]
  rw [← prod_sdiff (s₁ := s) (filter_subset _ _)]
  apply mul_eq_zero_of_right
  rw [prod_congr rfl hs', prod_const]
  suffices m ≤ #s by
    obtain ⟨m', hm'⟩ := Nat.exists_eq_add_of_le this
    rw [hm', pow_add, hf, zero_mul]
  rw [← Nat.add_le_add_iff_right, add_comm #s,
    Finset.card_sdiff_add_card_eq_card (filter_subset _ _), card_range]
  apply le_trans _ hn
  simp only [add_comm m, Nat.add_le_add_iff_right, ← hk.1,
    ← sum_sdiff (hs), sum_eq_zero (s := s) hs'', add_zero]
  rw [← hs_def]
  convert! Finset.card_nsmul_le_sum (range n \ s) (fun x ↦ degree (k x)) 1 _
  · simp only [smul_eq_mul, mul_one]
  · simp only [degree_eq_weight_one, map_sum]
  · simp only [hs_def, mem_filter, mem_sdiff, mem_range, not_and, and_imp]
    intro i hi hi'
    rw [← not_lt, Nat.lt_one_iff, degree_eq_zero_iff]
    exact hi' hi

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x y : MvPolynomial σ R
h : ↑x = ↑y
m✝ : σ →₀ ℕ
⊢ coeff m✝ x = coeff m✝ y

Tactic:
simp_rw [← coeff_coe, h]

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

Goal state before:
pp: case neg
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) < ↑γ
⊢ ∃ y, v.intValuation (b - y * a) < ↑γ

Tactic:
apply Exists.imp (fun _ h ↦ lt_of_le_of_lt h hnγ)

Goal state after:
case neg
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) < ↑γ
⊢ ∃ a_1, v.intValuation (b - a_1 * a) ≤ exp (-↑n)
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑((weight w) d) < weightedOrder w f + weightedOrder w g
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal d
⊢ (coeff (i, j).1) f * (coeff (i, j).2) g = 0

Tactic:
by_cases! hi : weight w i < f.weightedOrder w

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑((weight w) d) < weightedOrder w f + weightedOrder w g
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal d
hi : ↑((weight w) i) < weightedOrder w f
⊢ (coeff (i, j).1) f * (coeff (i, j).2) g = 0

case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑((weight w) d) < weightedOrder w f + weightedOrder w g
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal d
hi : weightedOrder w f ≤ ↑((weight w) i)
⊢ (coeff (i, j).1) f * (coeff (i, j).2) g = 0
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 * (truncTotal n) p ^ 1) = (coeff x) (p ^ k * p ^ 1)

Tactic:
pow_one,

Goal state after:
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 * (truncTotal n) p) = (coeff x) (p ^ k * p)
Module: Mathlib.Topology.Algebra.TopologicallyNilpotent

Goal state before:
pp: R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : Ring R
inst✝ : IsLinearTopology R R
a b : R
hb : IsTopologicallyNilpotent b
hab : Commute a b
⊢ IsTopologicallyNilpotent (a * b)

Tactic:
by
  simp_rw [IsTopologicallyNilpotent, hab.mul_pow]
  exact IsLinearTopology.tendsto_mul_zero_of_right _ _ hb

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

Goal state before:
pp: case refine_2.refine_1
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
s : Set (adicCompletion K v)
x✝ : ∃ γ, {x | (valuation K v).restrict x < ↑γ} ⊆ s
γ : (ofClass (valuation K v)).ValueGroup₀ˣ
hγ : {x | (valuation K v).restrict x < ↑γ} ⊆ s
⊢ {y | Valued.v.restrict y < ↑((Units.mapEquiv (valueGroupOrderIso K v).toMulEquiv) γ)} ∈ 𝓝 0

Tactic:
Valued.mem_nhds_zero

Goal state after:
case refine_2.refine_1
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
s : Set (adicCompletion K v)
x✝ : ∃ γ, {x | (valuation K v).restrict x < ↑γ} ⊆ s
γ : (ofClass (valuation K v)).ValueGroup₀ˣ
hγ : {x | (valuation K v).restrict x < ↑γ} ⊆ s
⊢ ∃ γ_1,
    {x | Valued.v.restrict x < ↑γ_1} ⊆
      {y | Valued.v.restrict y < ↑((Units.mapEquiv (valueGroupOrderIso K v).toMulEquiv) γ)}
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : ↑p ≤ weightedOrder w f
hg : ↑q ≤ weightedOrder w g
d : σ →₀ ℕ
hd : ¬(weight w) d = p + q
⊢ 0 = (coeff d) ((weightedHomogeneousComponent w p) f * (weightedHomogeneousComponent w q) g)

Tactic:
symm
    apply IsWeightedHomogeneous.coeff_eq_zero _ hd
    exact IsWeightedHomogeneous.mul
      (isWeightedHomogeneous_weightedHomogeneousComponent w f p)
      (isWeightedHomogeneous_weightedHomogeneousComponent w g q)

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

Goal state before:
pp: case neg
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.toNat + 1) * ψ
this : (coeff n) φ = (coeff n) (ψ * X ^ (φ.order.toNat + 1))
h✝ : ¬1 = 0
⊢ ↑n < ↑(φ.order.toNat + 1)

Tactic:
rw [← hn, ENat.natCast_lt_natCast]

Goal state after:
case neg
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.toNat + 1) * ψ
this : (coeff n) φ = (coeff n) (ψ * X ^ (φ.order.toNat + 1))
h✝ : ¬1 = 0
⊢ φ.order.toNat < φ.order.toNat + 1