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

Goal state before:
pp: case intro.refine_1
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)
J : Type u_1
inst✝ : Finite J
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
j : J → I
V : (k : J) → (D.obj (j k)).Opens
hV : ∀ (k : J), IsAffineOpen (V k)
hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k
val✝ : Fintype J
i : I
fi : (k : J) → i ⟶ j k
k : I
fkj : k ⟶ i
e : D.map fkj ⁻¹ᵁ ⨆ k, D.map (fi k) ⁻¹ᵁ V k = ⊤
⊢ IsOpenCover fun x ↦ D.map (fkj ≫ fi x) ⁻¹ᵁ V x

Tactic:
refine top_le_iff.mp (e.symm.trans_le ?_)
    simp_rw [Hom.preimage_iSup, ← Hom.comp_preimage, ← D.map_comp]
    simp

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

Goal state before:
pp: case neg.some.some.inl
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dp ≤ dq + 1
⊢ (p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree =
    max (2 • some dp) (2 • some dq + 3)

pp: case neg.some.some.inr
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ (p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree =
    max (2 • some dp) (2 • some dq + 3)

Tactic:
· convert!
            (degree_sub_eq_right_of_degree_lt <|
                  (degree_sub_le _ _).trans_lt <|
                    max_lt_iff.mpr ⟨hdp.trans_lt _, hdpq.trans_lt _⟩).trans
              (max_eq_right_of_lt _).symm <;> rw [hdq] <;>
                exact WithBot.coe_lt_coe.mpr <| by dsimp; linarith only [hpq]

Goal state after:
case neg.some.some.inr
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ (p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree =
    max (2 • some dp) (2 • some dq + 3)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Affine F
x₁ y₁ x₂ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
H : some x₁ y₁ h₁ = some x₂ y₂ h₂ ∨ some x₁ y₁ h₁ = -some x₂ y₂ h₂
⊢ x₁ = x₂

Tactic:
grind [neg_some]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ ((mk W) (C (W.preΨ n)) ^ 2 * if Even n then (mk W) (C W.Ψ₂Sq) else 1) =
    (mk W) (C (W.preΨ n ^ 2)) * if Even n then (mk W) (C W.Ψ₂Sq) else 1

Tactic:
map_pow

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
inst✝⁴ : IsCofiltered I
R : CommRingCat
inst✝³ : IsAffine (Spec R)
S : CommRingCat
inst✝² : IsAffine (Spec S)
φ : R ⟶ S
inst✝¹ : LocallyOfFinitePresentation (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst✝ : ∀ (i : I), IsAffine ((D ⋙ Scheme.Spec).obj i)
t : D ⋙ Scheme.Spec ⟶ (Functor.const I).obj (Spec R)
a : c.pt ⟶ Spec S
ha : c.π ≫ t = (Functor.const I).map (a ≫ Spec.map φ)
e : ((Functor.const Iᵒᵖ).obj R).rightOp ⋙ Scheme.Spec ≅ (Functor.const I).obj (Spec R) :=
  NatIso.ofComponents (fun x ↦ Iso.refl ((((Functor.const Iᵒᵖ).obj R).rightOp ⋙ Scheme.Spec).obj x)) ⋯
x✝¹ x✝ : Iᵒᵖ
f : x✝¹ ⟶ x✝
⊢ Spec.map (((Functor.const Iᵒᵖ).obj R).map f ≫ Spec.preimage (t.app (Opposite.unop x✝))) =
    Spec.map (Spec.preimage (t.app (Opposite.unop x✝¹)) ≫ D.leftOp.map f)

Tactic:
simpa using! (t.naturality f.unop).symm

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ W.b₂ ^ 2 = 1

Tactic:
b₂_of_isCharTwoJNeZeroNF_of_char_two

Goal state after:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ 1 ^ 2 = 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ -W.b₂ ^ 3 - 864 * W.a₆ = 1

Tactic:
b₂_of_isCharTwoJNeZeroNF_of_char_two

Goal state after:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ -1 ^ 3 - 864 * W.a₆ = 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: F : Type u_2
inst✝² : Field F
W : WeierstrassCurve F
inst✝¹ : W.IsElliptic
inst✝ : W.IsCharTwoJEqZeroNF
h : -(64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2) ≠ 0
⊢ W.c₄ ^ 3 / W.Δ = 110592 * W.a₄ ^ 3 / (64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2)

Tactic:
c₄_of_isCharTwoJEqZeroNF,

Goal state after:
F : Type u_2
inst✝² : Field F
W : WeierstrassCurve F
inst✝¹ : W.IsElliptic
inst✝ : W.IsCharTwoJEqZeroNF
h : -(64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2) ≠ 0
⊢ (-48 * W.a₄) ^ 3 / W.Δ = 110592 * W.a₄ ^ 3 / (64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2)
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: 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
inst✝⁴ : IsCofiltered I
inst✝³ : LocallyOfFinitePresentation f
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)
a : c.pt ⟶ X
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
𝒰 : IsOpenCover fun V ↦ (↑V).1
i : I
s : Finset { x // x.1 ∈ c.pt.affineOpens ∧ x.1 ≤ (Opens.comap (TopCat.Hom.hom a.base)) (↑x.2).1 }
𝒱 : ↥s → (D.obj i).Opens
h𝒱 : IsOpenCover 𝒱
h𝒱𝒰 : ∀ (j : ↥s), IsAffineOpen (𝒱 j) ∧ (↑↑j).1 = c.π.app i ⁻¹ᵁ 𝒱 j
i' : I
fi'i : i' ⟶ i
hi' : ∀ (j : ↥s), D.map fi'i ⁻¹ᵁ 𝒱 j ≤ t.app i' ⁻¹ᵁ ↑(↑(↑↑j).2).2
𝒱' : ↥s → (D.obj i').Opens := fun x ↦ D.map fi'i ⁻¹ᵁ 𝒱 x
h𝒱'𝒰 : ∀ (j : ↥s), c.π.app i' ⁻¹ᵁ 𝒱' j = (↑↑j).1
x✝ : ∀ (j : ↥s) (k : Over i'), IsAffine ((opensDiagram D i' (𝒱' j)).obj k)
j : ↥s
k₁ k₂ : Over i'
f₁₂ : k₁ ⟶ k₂
⊢ (opensDiagram D i' (𝒱' j)).map f₁₂ ≫ Hom.resLE (t.app k₂.left) (↑(↑(↑↑j).2).2) (D.map k₂.hom ⁻¹ᵁ 𝒱' j) ⋯ =
    Hom.resLE (t.app k₁.left) (↑(↑(↑↑j).2).2) (D.map k₁.hom ⁻¹ᵁ 𝒱' j) ⋯ ≫
      ((Functor.const (Over i')).obj ↑↑(↑(↑↑j).2).2).map f₁₂

Tactic:
by simp [Hom.resLE_comp_resLE]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: 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
inst✝⁴ : IsCofiltered I
inst✝³ : LocallyOfFinitePresentation f
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)
a : c.pt ⟶ X
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
𝒰 : IsOpenCover fun V ↦ (↑V).1
i : I
s : Finset { x // x.1 ∈ c.pt.affineOpens ∧ x.1 ≤ (Opens.comap (TopCat.Hom.hom a.base)) (↑x.2).1 }
𝒱 : ↥s → (D.obj i).Opens
h𝒱 : IsOpenCover 𝒱
h𝒱𝒰 : ∀ (j : ↥s), IsAffineOpen (𝒱 j) ∧ (↑↑j).1 = c.π.app i ⁻¹ᵁ 𝒱 j
i' : I
fi'i : i' ⟶ i
hi' : ∀ (j : ↥s), D.map fi'i ⁻¹ᵁ 𝒱 j ≤ t.app i' ⁻¹ᵁ ↑(↑(↑↑j).2).2
k : I
fki : k ⟶ i
ak : (j : ↥s) → ↑(D.map fki ⁻¹ᵁ 𝒱 j) ⟶ X
hak : ∀ (j : ↥s), ak j ≫ f = (D.map fki ⁻¹ᵁ 𝒱 j).ι ≫ t.app k
hak' : ∀ (j : ↥s), c.π.app k ∣_ D.map fki ⁻¹ᵁ 𝒱 j ≫ ak j = (c.π.app k ⁻¹ᵁ D.map fki ⁻¹ᵁ 𝒱 j).ι ≫ a
⊢ ∃ l flk,
    ∀ (j₁ j₂ : ↥s),
      (D.obj l).homOfLE ⋯ ≫ D.map flk ∣_ D.map fki ⁻¹ᵁ 𝒱 j₁ ≫ ak j₁ =
        (D.obj l).homOfLE ⋯ ≫ D.map flk ∣_ D.map fki ⁻¹ᵁ 𝒱 j₂ ≫ ak j₂

Tactic:
let 𝒱' := (D.map fki ⁻¹ᵁ 𝒱 ·)

Goal state after:
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
inst✝⁴ : IsCofiltered I
inst✝³ : LocallyOfFinitePresentation f
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)
a : c.pt ⟶ X
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
𝒰 : IsOpenCover fun V ↦ (↑V).1
i : I
s : Finset { x // x.1 ∈ c.pt.affineOpens ∧ x.1 ≤ (Opens.comap (TopCat.Hom.hom a.base)) (↑x.2).1 }
𝒱 : ↥s → (D.obj i).Opens
h𝒱 : IsOpenCover 𝒱
h𝒱𝒰 : ∀ (j : ↥s), IsAffineOpen (𝒱 j) ∧ (↑↑j).1 = c.π.app i ⁻¹ᵁ 𝒱 j
i' : I
fi'i : i' ⟶ i
hi' : ∀ (j : ↥s), D.map fi'i ⁻¹ᵁ 𝒱 j ≤ t.app i' ⁻¹ᵁ ↑(↑(↑↑j).2).2
k : I
fki : k ⟶ i
ak : (j : ↥s) → ↑(D.map fki ⁻¹ᵁ 𝒱 j) ⟶ X
hak : ∀ (j : ↥s), ak j ≫ f = (D.map fki ⁻¹ᵁ 𝒱 j).ι ≫ t.app k
hak' : ∀ (j : ↥s), c.π.app k ∣_ D.map fki ⁻¹ᵁ 𝒱 j ≫ ak j = (c.π.app k ⁻¹ᵁ D.map fki ⁻¹ᵁ 𝒱 j).ι ≫ a
𝒱' : ↥s → (D.obj k).Opens := fun x ↦ D.map fki ⁻¹ᵁ 𝒱 x
⊢ ∃ l flk,
    ∀ (j₁ j₂ : ↥s),
      (D.obj l).homOfLE ⋯ ≫ D.map flk ∣_ D.map fki ⁻¹ᵁ 𝒱 j₁ ≫ ak j₁ =
        (D.obj l).homOfLE ⋯ ≫ D.map flk ∣_ D.map fki ⁻¹ᵁ 𝒱 j₂ ≫ ak j₂
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
⊢ ¬(P x / P z ^ 2 = Q x / Q z ^ 2 ∧ P y / P z ^ 3 = W.toAffine.negY (Q x / Q z ^ 2) (Q y / Q z ^ 3))

Tactic:
← X_eq_iff hPz hQz,

Goal state after:
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
⊢ ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y / P z ^ 3 = W.toAffine.negY (Q x / Q z ^ 2) (Q y / Q z ^ 3))
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
a b c : ValueGroupWithZero R
hab : a ≤ b
hbc : b ≤ c
⊢ a ≤ c

Tactic:
induction a using ValueGroupWithZero.ind with | mk a₁ a₂

Goal state after:
case mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
b c : ValueGroupWithZero R
hbc : b ≤ c
a₁ : R
a₂ : ↥(posSubmonoid R)
hab : ValueGroupWithZero.mk a₁ a₂ ≤ b
⊢ ValueGroupWithZero.mk a₁ a₂ ≤ c
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
⊢ (F.NeBot ∧ ∀ U ∈ ⋯.toRingFilterBasis.toAddGroupFilterBasis, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) ↔
    F.NeBot ∧ ∀ (γ : (ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ

Tactic:
apply and_congr Iff.rfl

Goal state after:
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
⊢ (∀ U ∈ ⋯.toRingFilterBasis.toAddGroupFilterBasis, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) ↔
    ∀ (γ : (ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝⁵ : Ring R
inst✝⁴ : ValuativeRel R
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
_u : UniformSpace R
inst✝² : IsUniformAddGroup R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
F : Filter R
⊢ (F.NeBot ∧ ∀ U ∈ ⋯.toRingFilterBasis.toAddGroupFilterBasis, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) ↔
    F.NeBot ∧ ∀ (γ : (ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ

Tactic:
apply and_congr Iff.rfl

Goal state after:
R : Type u_1
inst✝⁵ : Ring R
inst✝⁴ : ValuativeRel R
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
_u : UniformSpace R
inst✝² : IsUniformAddGroup R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
F : Filter R
⊢ (∀ U ∈ ⋯.toRingFilterBasis.toAddGroupFilterBasis, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) ↔
    ∀ (γ : (ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x ↦ ↑x⁻¹) = (fun y ↦ ↑y) ∘ fun x ↦ x⁻¹
eq_bot : 𝓝 0 ⊓ 𝓝 y = ⊥
⊢ Filter.comap coe' (𝓝 ↑0) ⊓ Filter.comap coe' (𝓝 y) = ⊥

Tactic:
← Filter.comap_inf

Goal state after:
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x ↦ ↑x⁻¹) = (fun y ↦ ↑y) ∘ fun x ↦ x⁻¹
eq_bot : 𝓝 0 ⊓ 𝓝 y = ⊥
⊢ Filter.comap coe' (𝓝 ↑0 ⊓ 𝓝 y) = ⊥
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : ValuativeRel A
inst✝² : ValuativeRel B
inst✝¹ : Algebra A B
inst✝ : ValuativeExtension A B
a b : A
⊢ (algebraMap A B) a <ᵥ (algebraMap A B) b ↔ a <ᵥ b

Tactic:
rw [← not_vle, vle_iff_vle, not_vle]

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

Goal state before:
pp: K✝ : Type u_1
inst✝⁴ : Field K✝
inst✝³ : UniformSpace K✝
L : Type u_2
inst✝² : Field L
inst✝¹ : UniformSpace L
inst✝ : CompletableTopField L
K : Subfield L
F : Filter ↥K
F_cau : Cauchy F
inf_F : 𝓝 0 ⊓ F = ⊥
⊢ Cauchy (map (fun x ↦ x⁻¹) F)

Tactic:
by
    let i : K →+* L := K.subtype
    have hi : IsUniformInducing i := isUniformEmbedding_subtype_val.isUniformInducing
    rw [← hi.cauchy_map_iff] at F_cau ⊢
    rw [map_comm (show (i ∘ fun x => x⁻¹) = (fun x => x⁻¹) ∘ i by ext; rfl)]
    apply CompletableTopField.nice _ F_cau
    rw [← Filter.push_pull', ← map_zero i, ← hi.isInducing.nhds_eq_comap, inf_F, Filter.map_bot]

Goal state after:
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 Γ
inst✝ : v.IsRankOneDiscrete
⊢ IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup

Tactic:
by
  rw [← generator_zpowers_eq_valueGroup]
  exact isCyclic_zpowers (generator v)

Goal state after:
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 Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : v ↑r ≠ 0
vr : Γˣ := Units.mk0 (v ↑r) hr₀
hvr_def : vr = Units.mk0 (v ↑r) hr₀
m : ℤ
hm : Units.mk0 (v ↑π.val) ⋯ ^ m = vr
hm' : v ↑π.val ^ m = v ↑r
hm₀ : 0 ≤ m
n : ℕ
hn : m = ↑n
hpow : v (↑π.val ^ (-m) * ↑r) = 1
a : ↥v.valuationSubring := ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
ha : a = ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
⊢ ¬↑π.val ^ m = 0 ∧ ¬r = 0

Tactic:
refine ⟨?_, hr⟩

Goal state after:
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : v ↑r ≠ 0
vr : Γˣ := Units.mk0 (v ↑r) hr₀
hvr_def : vr = Units.mk0 (v ↑r) hr₀
m : ℤ
hm : Units.mk0 (v ↑π.val) ⋯ ^ m = vr
hm' : v ↑π.val ^ m = v ↑r
hm₀ : 0 ≤ m
n : ℕ
hn : m = ↑n
hpow : v (↑π.val ^ (-m) * ↑r) = 1
a : ↥v.valuationSubring := ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
ha : a = ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
⊢ ¬↑π.val ^ m = 0
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : v.IsEquiv w
⊢ Filter.Tendsto (⇑(equiv v)) (nhds 0) (nhds ((equiv v) 0))

Tactic:
map_zero,

Goal state after:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : v.IsEquiv w
⊢ Filter.Tendsto (⇑(equiv v)) (nhds 0) (nhds 0)
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
⊢ Filter.Tendsto (⇑(equiv v).symm) (nhds 0) (nhds ((equiv v).symm 0))

Tactic:
map_zero,

Goal state after:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
⊢ Filter.Tendsto (⇑(equiv v).symm) (nhds 0) (nhds 0)
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case h
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
H : (valuation K (maximalIdeal A)) x ≤ 1
π : A
hπ : Irreducible π
a b : A
hb : b ∈ nonZeroDivisors A
h_frac : (algebraMap A K) a / (algebraMap A K) b = x
ha : a = 0
⊢ (algebraMap A K) 0 = (algebraMap A K) 0 / (algebraMap A K) b

Tactic:
map_zero,

Goal state after:
case h
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
H : (valuation K (maximalIdeal A)) x ≤ 1
π : A
hπ : Irreducible π
a b : A
hb : b ∈ nonZeroDivisors A
h_frac : (algebraMap A K) a / (algebraMap A K) b = x
ha : a = 0
⊢ 0 = 0 / (algebraMap A K) b
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
h : v.IsEquiv w
h_val : Valued.v.IsEquiv Valued.v
h_res : v.restrict.IsEquiv w.restrict
⊢ Filter.Tendsto (⇑(RingHom.id R)) (nhds 0) (nhds ((RingHom.id R) 0))

Tactic:
map_zero,

Goal state after:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
h : v.IsEquiv w
h_val : Valued.v.IsEquiv Valued.v
h_res : v.restrict.IsEquiv w.restrict
⊢ Filter.Tendsto (⇑(RingHom.id R)) (nhds 0) (nhds 0)
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
H : (maximalIdeal A).intValuation π ^ n / (maximalIdeal A).intValuation ↑⟨π ^ m, hb⟩ ≤ 1
⊢ ∃ a, (algebraMap A K) a = x

Tactic:
map_pow

Goal state after:
case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
H : (maximalIdeal A).intValuation π ^ n / (maximalIdeal A).intValuation π ^ m ≤ 1
⊢ ∃ a, (algebraMap A K) a = x
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
x : K
x_ne : x ≠ 0
s : Set K
γ : (ofClass v).ValueGroup₀ˣ
hs : {y | v.restrict (y - x⁻¹) < ↑γ} ⊆ s
⊢ ∃ γ, {y | v.restrict (y - x) < ↑γ} ⊆ Inv.inv ⁻¹' s

Tactic:
let γ' := Units.mk0 ((ValueGroup₀.restrict₀ _) x) (v.restrict.ne_zero_iff.mpr x_ne)

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
x : K
x_ne : x ≠ 0
s : Set K
γ : (ofClass v).ValueGroup₀ˣ
hs : {y | v.restrict (y - x⁻¹) < ↑γ} ⊆ s
γ' : (ofClass v).ValueGroup₀ˣ := Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
⊢ ∃ γ, {y | v.restrict (y - x) < ↑γ} ⊆ Inv.inv ⁻¹' s
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 Γ₀
⊢ Tendsto (⇑v.restrict) (𝓝 0) (𝓝 (v.restrict 0))

Tactic:
map_zero,

Goal state after:
case inl
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ Tendsto (⇑v.restrict) (𝓝 0) (𝓝 0)
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
⊢ Tendsto (⇑v) (𝓝 0) (𝓝 (v 0))

Tactic:
map_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
⊢ Tendsto (⇑v) (𝓝 0) (𝓝 0)
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
⊢ v.restrict z₀ ≠ 0

Tactic:
rwa [Valuation.ne_zero_iff]

Goal state after:
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.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K) (integralModel R W).a₁ = ((integralModel R W)⁄K).a₁

Tactic:
simp [baseChange]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K) (integralModel R W).a₂ = ((integralModel R W)⁄K).a₂

Tactic:
simp [baseChange]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K) (integralModel R W).a₃ = ((integralModel R W)⁄K).a₃

Tactic:
simp [baseChange]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K) (integralModel R W).a₄ = ((integralModel R W)⁄K).a₄

Tactic:
simp [baseChange]

Goal state after: