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

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
inst✝ : c.pt.IsQuasiAffine
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : U ∈ (D.obj i).affineOpens
hxU : (c.π.app i) x ∈ ↑U
j : I
r : ↑Γ(D.obj j, ⊤)
hr : IsAffineOpen (c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r))
hxr : x ∈ ↑(c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r))
hrU : ↑(c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r)) ⊆ ↑(c.π.app i ⁻¹ᵁ U)
k : I
fki : k ⟶ i
fkj : k ⟶ j
l : I
flk : l ⟶ k
hl :
  D.map flk ⁻¹ᵁ (D.obj k).basicOpen ((ConcreteCategory.hom (Hom.appTop (D.map fkj))) r) ≤ D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ U
⊢ (D.obj l).basicOpen ((ConcreteCategory.hom (Hom.appTop (D.map (flk ≫ fkj)))) r) =
    D.map (flk ≫ fki) ⁻¹ᵁ U ⊓ (D.obj l).basicOpen ((ConcreteCategory.hom (Hom.appTop (D.map (flk ≫ fkj)))) r)

Tactic:
eq_comm,

Goal state after:
I : Type u
inst✝⁵ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
inst✝ : c.pt.IsQuasiAffine
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : U ∈ (D.obj i).affineOpens
hxU : (c.π.app i) x ∈ ↑U
j : I
r : ↑Γ(D.obj j, ⊤)
hr : IsAffineOpen (c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r))
hxr : x ∈ ↑(c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r))
hrU : ↑(c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r)) ⊆ ↑(c.π.app i ⁻¹ᵁ U)
k : I
fki : k ⟶ i
fkj : k ⟶ j
l : I
flk : l ⟶ k
hl :
  D.map flk ⁻¹ᵁ (D.obj k).basicOpen ((ConcreteCategory.hom (Hom.appTop (D.map fkj))) r) ≤ D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ U
⊢ D.map (flk ≫ fki) ⁻¹ᵁ U ⊓ (D.obj l).basicOpen ((ConcreteCategory.hom (Hom.appTop (D.map (flk ≫ fkj)))) r) =
    (D.obj l).basicOpen ((ConcreteCategory.hom (Hom.appTop (D.map (flk ≫ fkj)))) r)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ W.Ψ (-n) = -W.Ψ n

Tactic:
simp_rw [Ψ, preΨ_neg, C_neg, neg_mul, even_neg]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
X : Scheme
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : IsAffine X
inst✝² : ∀ (i : I), IsAffine (D.obj i)
a : c.pt ⟶ X
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
f : X ⟶ Spec R
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : IsAffine (Spec R)
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
⊢ ∃ i g, c.π.app i ≫ g = a ∧ g ≫ f = t.app i

Tactic:
wlog hX : ∃ S, X = Spec S generalizing X

Goal state after:
case inr
I : Type u
inst✝⁵ : Category.{u, u} I
X : Scheme
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : IsAffine X
inst✝² : ∀ (i : I), IsAffine (D.obj i)
a : c.pt ⟶ X
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
f : X ⟶ Spec R
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : IsAffine (Spec R)
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
this :
  ∀ {X : Scheme} [IsAffine X] (a : c.pt ⟶ X) (f : X ⟶ Spec R) [LocallyOfFinitePresentation f],
    c.π ≫ t = (Functor.const I).map (a ≫ f) → (∃ S, X = Spec S) → ∃ i g, c.π.app i ≫ g = a ∧ g ≫ f = t.app i
hX : ¬∃ S, X = Spec S
⊢ ∃ i g, c.π.app i ≫ g = a ∧ g ≫ f = t.app i

I : Type u
inst✝⁵ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ (i : I), IsAffine (D.obj i)
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
inst✝² : IsAffine (Spec R)
X : Scheme
inst✝¹ : IsAffine X
a : c.pt ⟶ X
f : X ⟶ Spec R
inst✝ : LocallyOfFinitePresentation f
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
hX : ∃ S, X = Spec S
⊢ ∃ i g, c.π.app i ≫ g = a ∧ g ≫ f = t.app i
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ (i : I), IsAffine (D.obj i)
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
inst✝² : IsAffine (Spec R)
S : CommRingCat
inst✝¹ : IsAffine (Spec S)
a : c.pt ⟶ Spec S
φ : R ⟶ S
inst✝ : LocallyOfFinitePresentation (Spec.map φ)
ha : c.π ≫ t = (Functor.const I).map (a ≫ Spec.map φ)
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), IsAffine (D.obj i)]
    (t : D ⟶ (Functor.const I).obj (Spec R)) (a : c.pt ⟶ Spec S),
    c.π ≫ t = (Functor.const I).map (a ≫ Spec.map φ) →
      (∃ D', D = D' ⋙ Scheme.Spec) → ∃ i g, c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
hD : ¬∃ D', D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
i : I
⊢ IsIso (e.app i)

Tactic:
dsimp [e]

Goal state after:
I : Type u
inst✝⁵ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ (i : I), IsAffine (D.obj i)
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
inst✝² : IsAffine (Spec R)
S : CommRingCat
inst✝¹ : IsAffine (Spec S)
a : c.pt ⟶ Spec S
φ : R ⟶ S
inst✝ : LocallyOfFinitePresentation (Spec.map φ)
ha : c.π ≫ t = (Functor.const I).map (a ≫ Spec.map φ)
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), IsAffine (D.obj i)]
    (t : D ⟶ (Functor.const I).obj (Spec R)) (a : c.pt ⟶ Spec S),
    c.π ≫ t = (Functor.const I).map (a ≫ Spec.map φ) →
      (∃ D', D = D' ⋙ Scheme.Spec) → ∃ i g, c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
hD : ¬∃ D', D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
i : I
⊢ IsIso (D.obj i).toSpecΓ
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP F 2
⊢ W.j ≠ 0

Tactic:
by
  rw [j_of_isCharTwoJNeZeroNF_of_char_two, div_ne_zero_iff]
  have h := W.Δ'.ne_zero
  rw [coe_Δ', Δ_of_isCharTwoJNeZeroNF_of_char_two] at h
  exact ⟨one_ne_zero, h⟩

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

Goal state before:
pp: case neg
R : Type u_1
inst✝⁴ : CommRing R
F : Type u_2
inst✝³ : Field F
W✝ : WeierstrassCurve R
inst✝² : CharP R 2
inst✝¹ : CharP F 2
W : WeierstrassCurve F
inst✝ : DecidableEq F
ha₁ : ¬W.a₁ = 0
⊢ (W.toCharTwoNF • W).IsCharTwoNF

Tactic:
rw [toCharTwoNF, dif_neg ha₁]
    have := W.toCharTwoJNeZeroNF_spec ha₁
    infer_instance

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
h : P ≈ Q
⊢ P x * Q z ^ 2 = Q x * P z ^ 2

Tactic:
by
  rcases h with ⟨u, rfl⟩
  simp only [Units.smul_def, smul_fin3_ext]
  ring1

Goal state after:
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
inst✝² : CharP F 3
inst✝¹ : E.IsCharThreeJNeZeroNF
inst✝ : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
⊢ ∃ C, C • E = E'

Tactic:
have h := E'.Δ'.ne_zero

Goal state after:
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsCharThreeJNeZeroNF
inst✝ : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
h : ↑E'.Δ' ≠ 0
⊢ ∃ C, C • E = E'
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
h : P ≈ Q
⊢ P y * Q z ^ 3 = Q y * P z ^ 3

Tactic:
by
  rcases h with ⟨u, rfl⟩
  simp only [Units.smul_def, smul_fin3_ext]
  ring1

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

Goal state before:
pp: case inr
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
heq : E.j = E'.j
h✝¹ : E.IsShortNF
this : ∀ (E' : WeierstrassCurve F) [inst : E'.IsElliptic], E.j = E'.j → E'.IsShortNF → ∃ C, C • E = E'
h✝ : ¬E'.IsShortNF
C : VariableChange F
hE' : (C • E').IsShortNF
⊢ ∃ C, C • E = E'

Tactic:
← variableChange_j E' C

Goal state after:
case inr
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
this : ∀ (E' : WeierstrassCurve F) [inst : E'.IsElliptic], E.j = E'.j → E'.IsShortNF → ∃ C, C • E = E'
h✝ : ¬E'.IsShortNF
C : VariableChange F
heq : E.j = (C • E').j
hE' : (C • E').IsShortNF
⊢ ∃ C, C • E = E'
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case inl
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
h : ↑(2 * n) ≠ 0
⊢ (W.preΨ' (2 * n)).coeff (((2 * n) ^ 2 - if Even (2 * n) then 4 else 1) / 2) ≠ 0

Tactic:
rw [coeff_preΨ', if_pos <| even_two_mul n, n.mul_div_cancel_left two_pos]

Goal state after:
case inl
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
h : ↑(2 * n) ≠ 0
⊢ ↑n ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : Nontrivial R
⊢ W'.Nonsingular ![1, 1, 0]

Tactic:
simp only [nonsingular_of_Z_eq_zero, equation_zero, true_and, fin3_def_ext, ← not_and_or]

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : Nontrivial R
⊢ ¬(3 * 1 ^ 2 = 0 ∧ 2 * 1 = 0 ∧ W'.a₁ * 1 * 1 = 0)
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: K : Type u_2
inst✝¹ : DivisionRing K
inst✝ : ValuativeRel K
a : K
⊢ a =ᵥ 0 ↔ 0 = a

Tactic:
eq_comm,

Goal state after:
K : Type u_2
inst✝¹ : DivisionRing K
inst✝ : ValuativeRel K
a : K
⊢ a =ᵥ 0 ↔ a = 0
Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = span {x}
y : R
hy : Submodule.colon I ↑(span {a}) = span {y}
i : R
hi : i ∈ I
⊢ i ∈ span {x * y}

Tactic:
have hisup : i ∈ I ⊔ span {a} := mem_sup_left hi

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = span {x}
y : R
hy : Submodule.colon I ↑(span {a}) = span {y}
i : R
hi : i ∈ I
hisup : i ∈ I ⊔ span {a}
⊢ i ∈ span {x * y}
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝ : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v.IsUniformizer π
⊢ 0 < v π

Tactic:
IsUniformizer.iff

Goal state after:
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝ : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v π = ↑(IsRankOneDiscrete.generator v)
⊢ 0 < v π
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
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
⊢ v (y - x) * ((v y)⁻¹ * (v y)⁻¹) = v (y - x) * (v y * v y)⁻¹

Tactic:
mul_inv_rev

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 x = v y
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
⊢ v (y - x) * ((v y)⁻¹ * (v y)⁻¹) = v (y - x) * ((v y)⁻¹ * (v y)⁻¹)
Module: Mathlib.Order.Interval.Finset.DenselyOrdered

Goal state before:
pp: X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
⊢ DenselyOrdered ↑s ↔ s.Subsingleton

Tactic:
by
  refine ⟨fun H ↦ ?_, fun h ↦ h.denselyOrdered⟩
  rw [← Set.subsingleton_coe, ← not_nontrivial_iff_subsingleton, nontrivial_iff_lt]
  suffices DenselyOrdered (WithBot.some ⁻¹' s) by
    rintro ⟨x, y, H⟩
    rw [_root_.denselyOrdered_set_iff_subsingleton] at this
    obtain ⟨z, hz, hz'⟩ := exists_between H
    have hz0 : (⊥ : WithBot X) < z := by simp [(Subtype.coe_lt_coe.mpr hz).trans_le']
    replace hz' : WithBot.unbot z.val hz0.ne' < WithBot.unbot y (hz0.trans hz').ne' := by
      rwa [← WithBot.coe_lt_coe, WithBot.coe_unbot, WithBot.coe_unbot]
    refine absurd (this ?_ ?_) hz'.ne <;>
    simp
  constructor
  simp only [Subtype.exists, Set.mem_preimage, Subtype.forall, Subtype.mk_lt_mk, exists_and_right,
    exists_prop]
  intro x hx y hy hxy
  have : (⟨_, hx⟩ : s) < ⟨_, hy⟩ := by simp [hxy]
  obtain ⟨z, hz, hz'⟩ := exists_between this
  simp only [← Subtype.coe_lt_coe] at hz hz'
  refine ⟨WithBot.unbot z (hz.trans_le' (by simp)).ne', ⟨?_, ?_⟩, ?_⟩
  · simp
  · rw [← WithBot.coe_lt_coe]
    simp [hz.trans_le]
  · rw [← WithBot.coe_lt_coe]
    simp [hz'.trans_le']

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₀), γ₀ ≠ 0 → ∀ᶠ (x : K) in 𝓝 0, v.restrict x < γ₀

Tactic:
intro γ hγ

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
⊢ ∀ᶠ (x : K) in 𝓝 0, 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
⊢ ∀ (γ₀ : Γ₀), γ₀ ≠ 0 → ∀ᶠ (x : K) in 𝓝 0, v x < γ₀

Tactic:
intro γ hγ

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
⊢ ∀ᶠ (x : K) in 𝓝 0, v x < γ
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
this : closure {a} = closure {b}
ha : a ∈ closure {b}
⊢ b = |a|ₘ ∧ 1 < b

Tactic:
rw [mem_closure_singleton] at ha

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}
ha : ∃ n, b ^ n = a
⊢ 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: α : Type u_2
β : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : PartialOrder α
inst✝² : CommMonoid β
inst✝¹ : PartialOrder β
e : α ≃*o β
inst✝ : MulArchimedean α
x y : β
hxy : 1 < e.symm y
⊢ ∃ n, x ≤ y ^ n

Tactic:
refine (MulArchimedean.arch (e.symm x) hxy).imp ?_

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : PartialOrder α
inst✝² : CommMonoid β
inst✝¹ : PartialOrder β
e : α ≃*o β
inst✝ : MulArchimedean α
x y : β
hxy : 1 < e.symm y
⊢ ∀ (a : ℕ), e.symm x ≤ e.symm y ^ a → x ≤ y ^ a
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : DecidableEq σ
n : σ →₀ ℕ
⊢ monomial n = LinearMap.single R (fun x ↦ R) n

Tactic:
monomial

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : DecidableEq σ
n : σ →₀ ℕ
⊢ LinearMap.single R (fun x ↦ R) n = LinearMap.single R (fun x ↦ R) n
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
⊢ (coeff n) (C a) = if n = 0 then a else 0

Tactic:
rw [← monomial_zero_eq_C_apply, coeff_monomial]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
n : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
inst✝ : DecidableEq σ
⊢ antidiagonal n = antidiagonal n

Tactic:
rw [Subsingleton.elim (Classical.decEq σ) ‹DecidableEq σ›]

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⟧
huv : (map f) u = (map f) v
k : ℕ
⊢ f ((coeff k) u) = f ((coeff k) v)

Tactic:
rw [← PowerSeries.coeff_map, ← PowerSeries.coeff_map, huv]

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 ^ 0 = 1

Tactic:
pow_zero a

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
hr : r = 0
⊢ v.intValuation r ≤ exp (-↑n) ↔ v.asIdeal ^ n ∣ Ideal.span {r}

Tactic:
simp_rw [hr, Valuation.map_zero, Ideal.dvd_span_singleton, zero_le, Submodule.zero_mem]

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

Goal state before:
pp: case pos
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 = γ → ∃ a, v a = γ}

Tactic:
simp [H]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
⊢ MvPolynomial.coeff m ((trunc R n) φ) = if m < n then (coeff m) φ else 0

Tactic:
simpa using! coeff_truncFinset (s := Iio n) (x := m) φ

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
S : Type u_3
inst✝⁸ : Field K
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
v : HeightOneSpectrum R
inst✝⁴ : Algebra S K
S₀ : Type u_4
inst✝³ : CommSemiring S₀
inst✝² : Algebra S₀ S
inst✝¹ : Algebra S₀ K
inst✝ : IsScalarTower S₀ S K
x : S₀
⊢ ((algebraMap S₀ (adicCompletion K v)) x).toCompletion =
    ((algebraMap S (adicCompletion K v)) ((algebraMap S₀ S) x)).toCompletion

Tactic:
rw [algebraMap_adicCompletion_toCompletion, algebraMap_adicCompletion_toCompletion,
      IsScalarTower.algebraMap_apply S₀ S ((v.valuation K).Completion)]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : ↑n < ψ.order
this : (coeff n) (φ * ψ) = ∑ p ∈ antidiagonal n, 0
⊢ (coeff n) (φ * ψ) = 0

Tactic:
rw [this, Finset.sum_const_zero]

Goal state after:
Module: Mathlib.Analysis.Complex.Cardinality

Goal state before:
pp: ⊢ ¬Set.univ.Countable

Tactic:
rw [← le_aleph0_iff_set_countable, not_le, Cardinal.mk_univ_complex]

Goal state after:
⊢ ℵ₀ < 𝔠
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: s : ℂ
⊢ LSeriesSummable 0 s

Tactic:
by
  simp [LSeriesSummable, funext (term_def 0 s), summable_zero]

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

Goal state before:
pp: case neg.hb
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
i : ℕ
hn : ¬k ∣ i
⊢ ¬∃ a, k * a = i

Tactic:
eq_comm,

Goal state after:
case neg.hb
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
i : ℕ
hn : ¬k ∣ i
⊢ ¬∃ a, i = k * a
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : f =O[atTop] fun n ↦ ↑n ^ (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖↑x_1 ^ (x - 1)‖
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ‖f b‖ ≤ C * ‖↑b ^ (x - 1)‖
⊢ LSeriesSummable f s

Tactic:
let C' := max C (max' (insert 0 (image (fun n : ℕ ↦ ‖f n‖ / (n : ℝ) ^ (x - 1)) (range m)))
    (insert_nonempty 0 _))

Goal state after:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : f =O[atTop] fun n ↦ ↑n ^ (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖↑x_1 ^ (x - 1)‖
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ‖f b‖ ≤ C * ‖↑b ^ (x - 1)‖
C' : ℝ := max C ((insert 0 (image (fun n ↦ ‖f n‖ / ↑n ^ (x - 1)) (range m))).max' ⋯)
⊢ LSeriesSummable f s
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
f : MvPowerSeries σ R
inst✝ : Finite τ
x : σ → ℕ
k : ℕ
ha : HasSubst a
h : ∀ (i : σ), constantCoeff (a i) = 0
hx : ∀ (i : σ), k ≤ x i
⊢ (truncTotal k) (subst a f) =
    (truncTotal k) (∑ i ∈ range k, subst (fun i ↦ ↑((truncTotal (x i)) (a i))) ((homogeneousComponent i) f))

Tactic:
truncTotal_subst_eq_truncTotal_subst_truncTotal_of_le ha hx

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
f : MvPowerSeries σ R
inst✝ : Finite τ
x : σ → ℕ
k : ℕ
ha : HasSubst a
h : ∀ (i : σ), constantCoeff (a i) = 0
hx : ∀ (i : σ), k ≤ x i
⊢ (truncTotal k) (subst (fun i ↦ ↑((truncTotal (x i)) (a i))) f) =
    (truncTotal k) (∑ i ∈ range k, subst (fun i ↦ ↑((truncTotal (x i)) (a i))) ((homogeneousComponent i) f))
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
f : E → F
x : E
s : Set E
hf : Injective ⇑(fderivWithin 𝕜 f s x)
a✝ : Nontrivial E
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
contrapose hf

Goal state after:
𝕜 : 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 : E → F
x : E
s : Set E
a✝ : Nontrivial E
hf : ¬DifferentiableWithinAt 𝕜 f s x
⊢ ¬Injective ⇑(fderivWithin 𝕜 f s x)