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

Goal state before:
pp: F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := invertibleOfNonzero hchar2
this : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
h : E'.a₆ = 0
⊢ False

Tactic:
h,

Goal state after:
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := invertibleOfNonzero hchar2
this : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : E.a₄ ^ 3 * 0 ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
h : E'.a₆ = 0
⊢ False
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
a b : R
⊢ W'.toAffine.Equation a b ∧
      (W'.a₁ * b * 1 - (3 * a ^ 2 + 2 * W'.a₂ * a * 1 ^ 2 + W'.a₄ * 1 ^ 4) ≠ 0 ∨
        2 * b + W'.a₁ * a * 1 + W'.a₃ * 1 ^ 3 ≠ 0 ∨
          W'.a₁ * a * b + 3 * W'.a₃ * b * 1 ^ 2 - (2 * W'.a₂ * a ^ 2 * 1 + 4 * W'.a₄ * a * 1 ^ 3 + 6 * W'.a₆ * 1 ^ 5) ≠
            0) ↔
    W'.toAffine.Equation a b ∧
      (W'.toAffine.a₁ * b - (3 * a ^ 2 + 2 * W'.toAffine.a₂ * a + W'.toAffine.a₄) ≠ 0 ∨
        2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃ ≠ 0)

Tactic:
Affine.equation_iff',

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
a b : R
⊢ b ^ 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
          (a ^ 3 + W'.toAffine.a₂ * a ^ 2 + W'.toAffine.a₄ * a + W'.toAffine.a₆) =
        0 ∧
      (W'.a₁ * b * 1 - (3 * a ^ 2 + 2 * W'.a₂ * a * 1 ^ 2 + W'.a₄ * 1 ^ 4) ≠ 0 ∨
        2 * b + W'.a₁ * a * 1 + W'.a₃ * 1 ^ 3 ≠ 0 ∨
          W'.a₁ * a * b + 3 * W'.a₃ * b * 1 ^ 2 - (2 * W'.a₂ * a ^ 2 * 1 + 4 * W'.a₄ * a * 1 ^ 3 + 6 * W'.a₆ * 1 ^ 5) ≠
            0) ↔
    b ^ 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
          (a ^ 3 + W'.toAffine.a₂ * a ^ 2 + W'.toAffine.a₄ * a + W'.toAffine.a₆) =
        0 ∧
      (W'.toAffine.a₁ * b - (3 * a ^ 2 + 2 * W'.toAffine.a₂ * a + W'.toAffine.a₄) ≠ 0 ∨
        2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃ ≠ 0)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type s
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
h : W'.Equation P
⊢ f ((eval P) W'.polynomial) = 0

Tactic:
h,

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type s
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
h : W'.Equation P
⊢ f 0 = 0
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case refine_1
I : Type u
inst✝⁵ : Category.{u, u} I
S X✝ : Scheme
D✝ : I ⥤ Scheme
t : D✝ ⟶ (Functor.const I).obj S
f : X✝ ⟶ S
c✝ : Cone D✝
hc✝ : IsLimit c✝
D : I ⥤ Over S
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (Over.Hom.left (D.map f))
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i).left
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i).left
X : Over S
inst✝ : LocallyOfFinitePresentation X.hom
c : Cocone D.op
hc : IsColimit c
this✝¹ : ∀ (i : I), CompactSpace ↥((D ⋙ Over.forget S).obj i)
this✝ : ∀ (i : I), QuasiSeparatedSpace ↥((D ⋙ Over.forget S).obj i)
this : ∀ {i j : I} (f : i ⟶ j), IsAffineHom ((D ⋙ Over.forget S).map f)
⊢ ∀ (j : Iᵒᵖ) (x x' : (D.op ⋙ yoneda.obj X).obj j),
    ((D.op ⋙ yoneda.obj X).coconeTypesEquiv.symm ((yoneda.obj X).mapCocone c)).ι j x =
        ((D.op ⋙ yoneda.obj X).coconeTypesEquiv.symm ((yoneda.obj X).mapCocone c)).ι j x' →
      ∃ k f,
        (ConcreteCategory.hom ((D.op ⋙ yoneda.obj X).map f)) x = (ConcreteCategory.hom ((D.op ⋙ yoneda.obj X).map f)) x'

Tactic:
intro k

Goal state after:
case refine_1
I : Type u
inst✝⁵ : Category.{u, u} I
S X✝ : Scheme
D✝ : I ⥤ Scheme
t : D✝ ⟶ (Functor.const I).obj S
f : X✝ ⟶ S
c✝ : Cone D✝
hc✝ : IsLimit c✝
D : I ⥤ Over S
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (Over.Hom.left (D.map f))
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i).left
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i).left
X : Over S
inst✝ : LocallyOfFinitePresentation X.hom
c : Cocone D.op
hc : IsColimit c
this✝¹ : ∀ (i : I), CompactSpace ↥((D ⋙ Over.forget S).obj i)
this✝ : ∀ (i : I), QuasiSeparatedSpace ↥((D ⋙ Over.forget S).obj i)
this : ∀ {i j : I} (f : i ⟶ j), IsAffineHom ((D ⋙ Over.forget S).map f)
k : Iᵒᵖ
⊢ ∀ (x x' : (D.op ⋙ yoneda.obj X).obj k),
    ((D.op ⋙ yoneda.obj X).coconeTypesEquiv.symm ((yoneda.obj X).mapCocone c)).ι k x =
        ((D.op ⋙ yoneda.obj X).coconeTypesEquiv.symm ((yoneda.obj X).mapCocone c)).ι k x' →
      ∃ k_1 f,
        (ConcreteCategory.hom ((D.op ⋙ yoneda.obj X).map f)) x = (ConcreteCategory.hom ((D.op ⋙ yoneda.obj X).map f)) x'
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ ![W'.dblZ P ^ 2, -W'.dblZ P ^ 3, 0] =
    ![(-W'.dblZ P) ^ 2 * ![1, 1, 0] x, (-W'.dblZ P) ^ 3 * ![1, 1, 0] y, -W'.dblZ P * ![1, 1, 0] z]

Tactic:
simp +decide [fin3_def_ext, Odd.neg_pow]

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
⊢ ∀ {U : Set A}, U ∈ {U | ∃ i, U = ↑(B i)} → 0 ∈ U

Tactic:
rintro _ ⟨i, rfl⟩
    exact (B i).zero_mem

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
⊢ ∀ {U : Set A}, U ∈ {U | ∃ i, U = ↑(B i)} → 0 ∈ U

Tactic:
by
    rintro _ ⟨i, rfl⟩
    exact (B i).zero_mem

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
⊢ ∀ {U : Set M}, U ∈ {U | ∃ i, U = ↑(B i)} → 0 ∈ U

Tactic:
rintro _ ⟨i, rfl⟩
    exact (B i).zero_mem

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
⊢ ∀ {U : Set M}, U ∈ {U | ∃ i, U = ↑(B i)} → 0 ∈ U

Tactic:
by
    rintro _ ⟨i, rfl⟩
    exact (B i).zero_mem

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

Goal state before:
pp: case left
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : r * ↑v ≤ᵥ s * ↑u
h2 : s * ↑u ≤ᵥ r * ↑v
h3 : s * ↑w ≤ᵥ t * ↑v
h4 : t * ↑v ≤ᵥ s * ↑w
this✝ : r * ↑v * ↑w ≤ᵥ s * ↑w * ↑u
this : r * ↑v * ↑w ≤ᵥ t * ↑v * ↑u
⊢ r * ↑w ≤ᵥ t * ↑u

Tactic:
grw [veq_mul_right_comm r, veq_mul_right_comm t] at this

Goal state after:
case left
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : r * ↑v ≤ᵥ s * ↑u
h2 : s * ↑u ≤ᵥ r * ↑v
h3 : s * ↑w ≤ᵥ t * ↑v
h4 : t * ↑v ≤ᵥ s * ↑w
this✝ : r * ↑v * ↑w ≤ᵥ s * ↑w * ↑u
this : r * ↑w * ↑v ≤ᵥ t * ↑u * ↑v
⊢ r * ↑w ≤ᵥ t * ↑u
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:
pp: case inl.inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
hy : y ≠ 0
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 0 ×ˢ 𝓝 y) (𝓝 0)

Tactic:
nhds_of_ne_zero hy,

Goal state after:
case inl.inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
hy : y ≠ 0
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 0 ×ˢ pure y) (𝓝 0)
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:
pp: case inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
hx : x ≠ 0
hy : y ≠ 0
⊢ Tendsto (fun p ↦ p.1 * p.2) (pure x ×ˢ 𝓝 y) (𝓝 ((x, y).1 * (x, y).2))

Tactic:
nhds_of_ne_zero hy,

Goal state after:
case inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
hx : x ≠ 0
hy : y ≠ 0
⊢ Tendsto (fun p ↦ p.1 * p.2) (pure x ×ˢ pure y) (𝓝 ((x, y).1 * (x, y).2))
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: case pos
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : IsTopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : x = 0
⊢ (↑x)⁻¹ = ↑x⁻¹

Tactic:
h,

Goal state after:
case pos
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : IsTopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : x = 0
⊢ (↑0)⁻¹ = ↑0⁻¹
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a / (valuation R) ↑r < (valuation R) b / (valuation R) ↑s
⊢ (embed v) ((valuation R) a / (valuation R) ↑r) < (embed v) ((valuation R) b / (valuation R) ↑s)

Tactic:
rw [← embedding_strictMono.lt_iff_lt]

Goal state after:
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a / (valuation R) ↑r < (valuation R) b / (valuation R) ↑s
⊢ embedding ((embed v) ((valuation R) a / (valuation R) ↑r)) <
    embedding ((embed v) ((valuation R) b / (valuation R) ↑s))
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝¹ : Field K
v : Valuation K Γ
inst✝ : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : maximalIdeal ↥v.valuationSubring = span {r}
h : r = 0
⊢ False

Tactic:
h,

Goal state after:
Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝¹ : Field K
v : Valuation K Γ
inst✝ : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : maximalIdeal ↥v.valuationSubring = span {0}
h : r = 0
⊢ False
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h✝ : v (x - y) < min (↑γ * (v y * v y)) (v y)
hyp1 : v (x - y) < ↑γ * (v y * v y)
hyp1' : v (x - y) * (v y * v y)⁻¹ < ↑γ
hyp2 : v (x - y) < v y
key : v x = v y
h : x = 0
⊢ y = 0

Tactic:
h,

Goal state after:
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h✝ : v (x - y) < min (↑γ * (v y * v y)) (v y)
hyp1 : v (x - y) < ↑γ * (v y * v y)
hyp1' : v (x - y) * (v y * v y)⁻¹ < ↑γ
hyp2 : v (x - y) < v y
key : v 0 = v y
h : x = 0
⊢ y = 0
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
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:
· rintro _ ⟨x, ⟨x_in₀, x_in₁⟩, rfl⟩ _ ⟨y, ⟨_, y_in₁⟩, rfl⟩
        simp only
        specialize H₁ x x_in₁ y y_in₁
        replace x_in₀ := H₀ x x_in₀
        clear H₀
        apply Valuation.inversion_estimate
        · have : (v.restrict x) ≠ 0 := by
            intro h
            rw [h] at x_in₀
            simp at x_in₀
          exact (Valuation.ne_zero_iff _).mp this
        · refine lt_of_lt_of_le H₁ ?_
          grw [Units.min_val, mul_assoc, Units.val_mul, Units.val_mul, x_in₀]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
y : G
hy : y ≠ 0
hy' : 0 < y
⊢ False

Tactic:
obtain ⟨⟨z, hz⟩, hz', hz''⟩ := h ({x | ⟨0, le_rfl⟩ < x}) ⟨⟨y, hy'.le⟩, hy'⟩

Goal state after:
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
y : G
hy : y ≠ 0
hy' : 0 < y
z : G
hz : z ∈ {x | 0 ≤ x}
hz' : ⟨z, hz⟩ ∈ {x | ⟨0, ⋯⟩ < x}
hz'' : ∀ x ∈ {x | ⟨0, ⋯⟩ < x}, ¬x < ⟨z, hz⟩
⊢ False
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_2
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : ({x | x ≤ g} \ {0}).WellFoundedOn fun x1 x2 ↦ x1 > x2
a : G₀
ha : g⁻¹ ≤ a
b : G₀
x✝ : g⁻¹ ≤ b
⊢ 0 < a

Tactic:
contrapose! ha

Goal state after:
case refine_2
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : ({x | x ≤ g} \ {0}).WellFoundedOn fun x1 x2 ↦ x1 > x2
a b : G₀
x✝ : g⁻¹ ≤ b
ha : a ≤ 0
⊢ a < g⁻¹
Module: Mathlib.Order.Northcott

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
h' : β → γ
inst✝² : Preorder β
inst✝¹ : LE γ
inst✝ : Northcott h
H : ∀ (c : γ), BddAbove (h' ⁻¹' {x | x ≤ c})
c : γ
⊢ {a | (h' ∘ h) a ≤ c}.Finite

Tactic:
obtain ⟨b, hb⟩ := bddAbove_def.mp (H c)

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
h' : β → γ
inst✝² : Preorder β
inst✝¹ : LE γ
inst✝ : Northcott h
H : ∀ (c : γ), BddAbove (h' ⁻¹' {x | x ≤ c})
c : γ
b : β
hb : ∀ y ∈ h' ⁻¹' {x | x ≤ c}, y ≤ b
⊢ {a | (h' ∘ h) a ≤ c}.Finite
Module: Mathlib.RingTheory.MvPowerSeries.Basic

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

Tactic:
by classical simp [coeff_mul]

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

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

Tactic:
by classical simp [coeff_mul]

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

Goal state before:
pp: S : Type u_2
T : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* T
hf : Function.Injective ⇑f
u v : S⟦X⟧
⊢ (map f) u = (map f) v → u = v

Tactic:
huv

Goal state after:
S : Type u_2
T : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* T
hf : Function.Injective ⇑f
u v : S⟦X⟧
huv : (map f) u = (map f) v
⊢ u = v
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: S : Type u_2
T : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* T
hf : Function.Injective ⇑f
u v : S⟦X⟧
huv : (map f) u = (map f) v
k : ℕ
⊢ (coeff k) ((map f) u) = (coeff k) ((map f) v)

Tactic:
huv

Goal state after:
S : Type u_2
T : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* T
hf : Function.Injective ⇑f
u v : S⟦X⟧
huv : (map f) u = (map f) v
k : ℕ
⊢ (coeff k) ((map f) v) = (coeff k) ((map f) v)
Module: Mathlib.RingTheory.MvPowerSeries.Basic

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

pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
a b : R
h : C a = C b
⊢ Type ?u.17

Tactic:
h,

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ ψ : MvPowerSeries σ R
⊢ (coeff 0) (φ * ψ) = (coeff 0) φ * (coeff 0) ψ

Tactic:
by classical simp [coeff_mul]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
a : R
n✝ : ℕ
h : n✝ = 0
⊢ a ^ n✝ = 1

Tactic:
h,

Goal state after:
case pos
R : Type u_1
inst✝ : CommSemiring R
a : R
n✝ : ℕ
h : n✝ = 0
⊢ a ^ 0 = 1
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
g : S →+* T
φ ψ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ f ((coeff n) (φ * ψ)) = (coeff n) ((fun n ↦ f ((coeff n) φ)) * fun n ↦ f ((coeff n) ψ))

Tactic:
rw [coeff_mul, map_sum, coeff_mul]
        apply Finset.sum_congr rfl
        rintro ⟨i, j⟩ _; rw [f.map_mul]; rfl

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : DivisionSemiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
φ : MvPowerSeries σ R
f : R →+* S
⊢ (map f) φ = 0 ↔ φ = 0

Tactic:
by
  simp only [MvPowerSeries.ext_iff]
  congr! with n
  simp

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

Goal state before:
pp: case neg
σ : 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
⊢ (coeff m) φ = (coeff m) (X s ^ n * fun m ↦ (coeff (m + single s n)) φ)

Tactic:
h,

Goal state after:
case neg
σ : 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
⊢ 0 = (coeff m) (X s ^ n * fun m ↦ (coeff (m + single s n)) φ)

case neg.a
σ : 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
⊢ m s < n
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
⊢ ∀ x ∈ (range n).finsuppAntidiag d, ∏ i ∈ range n, (coeff (x i)) f = 0

Tactic:
intro k

Goal state after:
σ : 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
k : ℕ →₀ σ →₀ ℕ
⊢ k ∈ (range n).finsuppAntidiag d → ∏ i ∈ range n, (coeff (k i)) f = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case inr
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
φ : R⟦X⟧
hn : n > 0
⊢ (coeff 1) (φ ^ n) = ↑n * (coeff 1) φ * constantCoeff φ ^ (n - 1)

Tactic:
induction n with
  | zero => lia
  | succ n' ih =>
      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.PowerSeries.Basic

Goal state before:
pp: A : Type u_2
inst✝ : CommRing A
⊢ (rescale (-1)) X = -X

Tactic:
rw [rescale_X, map_neg, map_one, neg_one_mul]

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : a = 0
⊢ weightedOrder w ((monomial d) a) = ⊤

Tactic:
h,

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : a = 0
⊢ weightedOrder w ((monomial d) 0) = ⊤
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 Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
H : ¬∃ x, v x = γ
⊢ IsClosed {a | ¬v a = γ}

Tactic:
rcases eq_or_ne γ 0 with rfl | hγ

Goal state after:
case neg.inl
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective ⇑v
H : ¬∃ x, v x = 0
⊢ IsClosed {a | ¬v a = 0}

case neg.inr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
H : ¬∃ x, v x = γ
hγ : γ ≠ 0
⊢ IsClosed {a | ¬v a = γ}
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 Γ₀
⊢ Function.Surjective ⇑v ↔ Function.Surjective ⇑v

Tactic:
by
  constructor <;> intro h γ <;> obtain ⟨a, ha⟩ := h γ
  · induction a using Completion.induction_on
    · by_cases H : ∃ x : K, (v : K → Γ₀) x = γ
      · simp [H]
      · simp only [H, imp_false]
        rcases eq_or_ne γ 0 with rfl | hγ
        · simp at H
        · obtain ⟨r, hr⟩ := h γ
          have hr' : restrict₀ (.ofClass (valuedCompletion (K := K)).v) r ≠ 0 := by
            rw [ne_eq, ← embedding_inj, embedding_restrict₀ r]
            simpa [hr]
          convert! isClosed_univ.sdiff (isOpen_sphere (hat K) hr') using 1
          ext x
          simp [← hr, ← v.restrict_def, v.restrict_inj]
    · exact ⟨_, by simpa using ha⟩
  · exact ⟨a, by simp [ha]⟩

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

Goal state before:
pp: σ : Type u_1
R✝ : Type u_2
S : Type u_3
inst✝¹ : CommSemiring R✝
s✝ : Finset (σ →₀ ℕ)
R : Type u_4
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
x✝¹ : R
x✝ : MvPowerSeries σ R
⊢ ∑ x ∈ s, (MvPolynomial.monomial x) ((coeff x) (x✝¹ • x✝)) =
    (RingHom.id R) x✝¹ • ∑ x ∈ s, (MvPolynomial.monomial x) ((coeff x) x✝)

Tactic:
ext
    simp [MvPolynomial.coeff, single, MvPolynomial.monomial]

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring R'
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Module R' M
inst✝³ : SMulCommClass R R' M
inst✝² : TopologicalSpace M
inst✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
I : Submodule R M
hI : ↑I ∈ 𝓝 0
J : Submodule R' M
hJ : ↑J ∈ 𝓝 0
J_sub_I : ↑J ⊆ ↑I
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • ↑I ⊆ ↑I
hR'J : uR' • ↑J ⊆ ↑J
hRJ : uR • ↑J ⊆ ↑I
S : Set M := ↑J ∪ uR • ↑J
S_sub_I : S ⊆ ↑I
⊢ uR • S = uR • ↑J ∪ (uR * uR) • ↑J

Tactic:
simp_rw [S, smul_union, mul_smul]

Goal state after: