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

Goal state before:
pp: case «0»
R : Type r
P : Fin 3 → R
⊢ ![P x, P y, P z] ((fun i ↦ i) ⟨0, ⋯⟩) = P ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl

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

Goal state before:
pp: case «1»
R : Type r
P : Fin 3 → R
⊢ ![P x, P y, P z] ((fun i ↦ i) ⟨1, ⋯⟩) = P ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl

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

Goal state before:
pp: case «2»
R : Type r
P : Fin 3 → R
⊢ ![P x, P y, P z] ((fun i ↦ i) ⟨2, ⋯⟩) = P ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
rfl

Goal state after:
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
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)
t𝒱 : (j : ↥s) → opensDiagram D i' (𝒱' j) ⟶ (Functor.const (Over i')).obj ↑↑(↑(↑↑j).2).2 :=
  fun j ↦ { app := fun k ↦ Hom.resLE (t.app k.left) (↑(↑(↑↑j).2).2) (D.map k.hom ⁻¹ᵁ 𝒱' j) ⋯, naturality := ⋯ }
this : ∀ (j : ↥s), IsAffine ↑(↑(↑↑j).2).1
k : ↥s → Over i'
ak : (j : ↥s) → (opensDiagram D i' (𝒱' j)).obj (k j) ⟶ ↑(↑(↑↑j).2).1
hk : ∀ (j : ↥s), (opensCone D c i' (𝒱' j)).π.app (k j) ≫ ak j = Hom.resLE a (↑(↑↑j).2).1 (c.π.app i' ⁻¹ᵁ 𝒱' j) ⋯
hk' : ∀ (j : ↥s), ak j ≫ Hom.resLE f (↑(↑(↑↑j).2).2) (↑(↑↑j).2).1 ⋯ = (t𝒱 j).app (k j)
i'' : I
fi''i' : i'' ⟶ i'
fi'' : (x : ↥s) → i'' ⟶ (k x).left
hi'' : ∀ (x : ↥s), fi'' x ≫ (k x).hom = fi''i'
j : ↥s
⊢ D.map (fi''i' ≫ fi'i) ⁻¹ᵁ 𝒱 j ≤ D.map (fi''i' ≫ fi'i) ⁻¹ᵁ 𝒱 j

Tactic:
rfl

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
𝒱' : ↥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)
t𝒱 : (j : ↥s) → opensDiagram D i' (𝒱' j) ⟶ (Functor.const (Over i')).obj ↑↑(↑(↑↑j).2).2 :=
  fun j ↦ { app := fun k ↦ Hom.resLE (t.app k.left) (↑(↑(↑↑j).2).2) (D.map k.hom ⁻¹ᵁ 𝒱' j) ⋯, naturality := ⋯ }
this : ∀ (j : ↥s), IsAffine ↑(↑(↑↑j).2).1
k : ↥s → Over i'
ak : (j : ↥s) → (opensDiagram D i' (𝒱' j)).obj (k j) ⟶ ↑(↑(↑↑j).2).1
hk : ∀ (j : ↥s), (opensCone D c i' (𝒱' j)).π.app (k j) ≫ ak j = Hom.resLE a (↑(↑↑j).2).1 (c.π.app i' ⁻¹ᵁ 𝒱' j) ⋯
hk' : ∀ (j : ↥s), ak j ≫ Hom.resLE f (↑(↑(↑↑j).2).2) (↑(↑↑j).2).1 ⋯ = (t𝒱 j).app (k j)
i'' : I
fi''i' : i'' ⟶ i'
fi'' : (x : ↥s) → i'' ⟶ (k x).left
hi'' : ∀ (x : ↥s), fi'' x ≫ (k x).hom = fi''i'
j : ↥s
⊢ c.π.app i ⁻¹ᵁ 𝒱 j ≤ c.π.app i ⁻¹ᵁ 𝒱 j

Tactic:
rfl

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, C • E = E'

Tactic:
obtain ⟨C, hE'⟩ := E'.exists_variableChange_isShortNF

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
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'
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
𝒱' : ↥s → (D.obj k).Opens := fun x ↦ D.map fki ⁻¹ᵁ 𝒱 x
l : ↥s → ↥s → I
flk : (j₁ j₂ : ↥s) → l j₁ j₂ ⟶ k
hflk :
  ∀ (j₁ j₂ : ↥s),
    (D.obj (l j₁ j₂)).homOfLE ⋯ ≫ D.map (flk j₁ j₂) ∣_ D.map fki ⁻¹ᵁ 𝒱 j₁ ≫ ak j₁ =
      (D.obj (l j₁ j₂)).homOfLE ⋯ ≫ D.map (flk j₁ j₂) ∣_ D.map fki ⁻¹ᵁ 𝒱 j₂ ≫ ak j₂
l' : I
fl'k : l' ⟶ k
fl'l : (x : ↥s × ↥s) → l' ⟶ l x.1 x.2
hl' : ∀ (x : ↥s × ↥s), fl'l x ≫ flk x.1 x.2 = fl'k
j₁ j₂ : ↥s
⊢ D.map (fl'k ≫ fki) ⁻¹ᵁ (𝒱 j₁ ⊓ 𝒱 j₂) ≤ D.map (fl'k ≫ fki) ⁻¹ᵁ (𝒱 j₁ ⊓ 𝒱 j₂)

Tactic:
rfl

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

Goal state before:
pp: case pos
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
⊢ ∃ C, C • E = E'

Tactic:
have ha₄ := E.Δ'.ne_zero
    rw [coe_Δ', Δ_of_isShortNF, ha₆, zero_pow two_ne_zero, mul_zero, add_zero, ← mul_assoc,
      mul_ne_zero_iff, pow_ne_zero_iff three_ne_zero] at ha₄
    replace ha₄ := ha₄.2
    have ha₆' : E'.a₆ = 0 := by
      rw [ha₆, zero_pow two_ne_zero, mul_zero, mul_eq_zero] at heq
      exact (pow_eq_zero_iff two_ne_zero).1 <| heq.resolve_left <| pow_ne_zero 3 ha₄
    have ha₄' := E'.Δ'.ne_zero
    rw [coe_Δ', Δ_of_isShortNF, ha₆', zero_pow two_ne_zero, mul_zero, add_zero, ← mul_assoc,
      mul_ne_zero_iff, pow_ne_zero_iff three_ne_zero] at ha₄'
    replace ha₄' := ha₄'.2
    obtain ⟨u, hu⟩ := IsSepClosed.exists_pow_nat_eq (E.a₄ / E'.a₄) 4
    have hu0 : u ≠ 0 := by
      rw [← pow_ne_zero_iff four_ne_zero, hu, div_ne_zero_iff]
      exact ⟨ha₄, ha₄'⟩
    use ⟨Units.mk0 u hu0, 0, 0, 0⟩
    ext
    · simp [variableChange_a₁]
    · simp [variableChange_a₂]
    · simp [variableChange_a₃]
    · simp_rw [variableChange_a₄, a₁_of_isShortNF, a₂_of_isShortNF, a₃_of_isShortNF,
        Units.val_inv_eq_inv_val, Units.val_mk0, inv_pow, inv_mul_eq_div, hu]
      simp [field]
    · simp [ha₆, ha₆', variableChange_a₆]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
m : ℕ
h : ↑↑(m + 1) ≠ 0
hn : m = 0
hm : (↑(m + 1)).natAbs = m + 1
h' : 1 = 0
⊢ 0 = 0

Tactic:
rfl

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
m : ℕ
h : ↑(-↑(m + 1)) ≠ 0
hn : m = 0
hm : (-↑(m + 1)).natAbs = m + 1
h' : 1 = 0
⊢ 0 = 0

Tactic:
rfl

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 : I
flk : l ⟶ k
hl :
  ∀ (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₂
h𝒲 : IsOpenCover fun k_1 ↦
  (Opens.comap (TopCat.Hom.hom (D.map flk).base)) ((Opens.comap (TopCat.Hom.hom (D.map fki).base)) (𝒱 k_1)) :=
  IsOpenCover.comap (IsOpenCover.comap h𝒱 (TopCat.Hom.hom (D.map fki).base)) (TopCat.Hom.hom (D.map flk).base)
𝒲 : (D.obj l).OpenCover := (D.obj l).openCoverOfIsOpenCover (fun x ↦ D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ 𝒱 x) h𝒲
F : D.obj l ⟶ X := Cover.glueMorphisms 𝒲 (fun j ↦ D.map flk ∣_ D.map fki ⁻¹ᵁ 𝒱 j ≫ ak j) ⋯
hF : ∀ (j : ↥s), (D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ 𝒱 j).ι ≫ F = D.map flk ∣_ D.map fki ⁻¹ᵁ 𝒱 j ≫ ak j
j : (Precoverage.ZeroHypercover.pullback₁ (c.π.app l) 𝒲).I₀
⊢ c.π.app i ⁻¹ᵁ 𝒱 j ≤ c.π.app i ⁻¹ᵁ 𝒱 j

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case refine_2
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 : I
flk : l ⟶ k
hl :
  ∀ (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₂
h𝒲 : IsOpenCover fun k_1 ↦
  (Opens.comap (TopCat.Hom.hom (D.map flk).base)) ((Opens.comap (TopCat.Hom.hom (D.map fki).base)) (𝒱 k_1)) :=
  IsOpenCover.comap (IsOpenCover.comap h𝒱 (TopCat.Hom.hom (D.map fki).base)) (TopCat.Hom.hom (D.map flk).base)
𝒲 : (D.obj l).OpenCover := (D.obj l).openCoverOfIsOpenCover (fun x ↦ D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ 𝒱 x) h𝒲
F : D.obj l ⟶ X := Cover.glueMorphisms 𝒲 (fun j ↦ D.map flk ∣_ D.map fki ⁻¹ᵁ 𝒱 j ≫ ak j) ⋯
hF : ∀ (j : ↥s), (D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ 𝒱 j).ι ≫ F = D.map flk ∣_ D.map fki ⁻¹ᵁ 𝒱 j ≫ ak j
j : 𝒲.I₀
⊢ (D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ 𝒱 j).ι ≫ t.app l = 𝒲.f j ≫ t.app l

Tactic:
rfl

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ ![(u • P) x, u ^ 3 * W'.negY P, (u • P) z] = u • W'.neg P

Tactic:
rfl

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

Goal state before:
pp: case h
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : NonarchimedeanGroup G
K : Type u_3
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : NonarchimedeanGroup K
U : Set (G × K)
U₁ : Set G
hU₁ : U₁ ∈ 𝓝 1.1
U₂ : Set K
hU₂ : U₂ ∈ 𝓝 1.2
h : U₁ ×ˢ U₂ ⊆ U
V : OpenSubgroup G
hV : ↑V ⊆ U₁
W : OpenSubgroup K
hW : ↑W ⊆ U₂
⊢ ∃ W, ↑V ×ˢ ↑W ⊆ U

Tactic:
grind

Goal state after:
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] y = -W'.dblZ P ^ 3

Tactic:
rfl

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ W'.dblY (u • P) = (u ^ 4) ^ 3 * W'.dblY P

Tactic:
simp only [dblY, negY_eq, negDblY_smul, dblX_smul, dblZ_smul]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ -((u ^ 4) ^ 3 * W'.negDblY P) - W'.a₁ * ((u ^ 4) ^ 2 * W'.dblX P) * (u ^ 4 * W'.dblZ P) -
      W'.a₃ * (u ^ 4 * W'.dblZ P) ^ 3 =
    (u ^ 4) ^ 3 * (-W'.negDblY P - W'.a₁ * W'.dblX P * W'.dblZ P - W'.a₃ * W'.dblZ P ^ 3)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P' Q' : Fin 3 → R
u v : Rˣ
⊢ W'.add ((fun m ↦ m • P') u) ((fun m ↦ m • Q') v) ≈ W'.add P' Q'

Tactic:
exact add_smul_equiv P' Q' u.isUnit v.isUnit

Goal state after:
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)
⊢ toAffine W
      ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1] =
    toAffine W P + toAffine W Q

Tactic:
rw [toAffine_some <| nonsingular_add_of_Z_ne_zero hP hQ hPz hQz hxy, toAffine_of_Z_ne_zero hP hPz,
    toAffine_of_Z_ne_zero hQ hQz,
    Affine.Point.add_some <| by rwa [← X_eq_iff hPz hQz, ← Y_eq_iff' hPz hQz]]

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ₀ γ₁ : (ofClass v).ValueGroup₀ˣ
⊢ ∃ k,
    v.ltAddSubgroup ((Units.map ↑embedding) k) ≤
      v.ltAddSubgroup ((Units.map ↑embedding) γ₀) ⊓ v.ltAddSubgroup ((Units.map ↑embedding) γ₁)

Tactic:
use min γ₀ γ₁

Goal state after:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ₀ γ₁ : (ofClass v).ValueGroup₀ˣ
⊢ v.ltAddSubgroup ((Units.map ↑embedding) (min γ₀ γ₁)) ≤
    v.ltAddSubgroup ((Units.map ↑embedding) γ₀) ⊓ v.ltAddSubgroup ((Units.map ↑embedding) γ₁)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : W.Point
⊢ (P + Q).toAffineLift = P.toAffineLift + Q.toAffineLift

Tactic:
rcases P, Q with ⟨@⟨⟨_⟩, hP⟩, @⟨⟨_⟩, hQ⟩⟩

Goal state after:
case mk.mk
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
point✝¹ : PointClass F
a✝¹ : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝¹)
point✝ : PointClass F
a✝ : Fin 3 → F
hQ : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝)
⊢ ({ point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝¹, nonsingular := hP } +
        { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝, nonsingular := hQ }).toAffineLift =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝¹, nonsingular := hP }.toAffineLift +
      { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝, nonsingular := hQ }.toAffineLift
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Field F
inst✝ : Field K
W' : Jacobian R
W : Jacobian F
x✝ : W.Point
⊢ x✝ + 0 = x✝

Tactic:
by
    classical
    apply (toAffineAddEquiv W).injective
    simp only [map_add, toAffineAddEquiv_apply, toAffineLift_zero, add_zero]

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

Goal state before:
pp: α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
l : Filter α
f : α → Γ₀
⊢ Tendsto f l (𝓝 0) ↔ ∀ (γ₀ : Γ₀), γ₀ ≠ 0 → ∀ᶠ (x : α) in l, f x < γ₀

Tactic:
by
  simp [nhds_zero]

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

Goal state before:
pp: R K : Type u
inst✝² : Ring R
inst✝¹ : DivisionRing K
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
this : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
s : Set R
γ : (ofClass v).ValueGroup₀ˣ
⊢ ↑(v.ltAddSubgroup ((Units.map ↑embedding) γ)) ⊆ s ↔ {x | v x < embedding ↑γ} ⊆ s

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : TopologicalSpace R
inst✝ : IsValuativeTopology R
s : Set R
⊢ s ∈ 𝓝 0 ↔ ∃ γ, {x | (valuation R) x < ↑γ} ⊆ s

Tactic:
by
  simp [mem_nhds_iff']

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y : R
this : x ≤ᵥ y ∨ y ≤ᵥ x
⊢ x <ᵥ y ↔ x ≤ᵥ y ∧ ¬y ≤ᵥ x

Tactic:
grind

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

Goal state before:
pp: M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : IsUniformAddGroup α
a✝ : Completion α
a : α
⊢ ↑0 = 0

Tactic:
rfl

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

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalRing α
x y : α
⊢ x - y ∈ closure 0 ↔ x - y ∈ ⊥.closure

Tactic:
rfl

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

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

Tactic:
by_cases h : x = 0
  · rw [h, inv_zero]
    dsimp [Inv.inv]
    norm_cast
    simp
  · conv_lhs => dsimp [Inv.inv]
    rw [if_neg]
    · exact hatInv_extends h
    · exact fun H => h (isDenseEmbedding_coe.injective H)

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
inf_F : 𝓝 0 ⊓ F = ⊥
i : ↥K →+* L := K.subtype
F_cau : Cauchy (map (⇑i) F)
hi : IsUniformInducing ⇑i
x✝ : ↥K
⊢ (⇑i ∘ fun x ↦ x⁻¹) x✝ = ((fun x ↦ x⁻¹) ∘ ⇑i) x✝

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Ring R
v : Valuation R Γ₀
S : Type u_3
inst✝¹ : Ring S
Λ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Λ₀
w : Valuation S Λ₀
s : Set (WithVal v)
x : WithVal v
e : ValuativeRel.ValueGroupWithZero (WithVal v) ≃*o (MonoidWithZeroHom.ofClass (valuation v)).ValueGroup₀ :=
  ValuativeRel.ValueGroupWithZero.orderMonoidIso (valuation v)
a : (MonoidWithZeroHom.ofClass (valuation v)).ValueGroup₀ˣ
⊢ {y | Valued.v.restrict (-x + y) < ↑a} ⊆ s ↔ {a_1 | (valuation v).restrict (-x + a_1) < ↑a} ⊆ s

Tactic:
rfl

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

Goal state before:
pp: Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst✝ : Ring R
v : Valuation R Γ₀
⊢ Subgroup.closure (Units.val ⁻¹' Set.range ⇑Valued.v) = Subgroup.closure (Units.val ⁻¹' Set.range (⇑v ∘ ofVal))

Tactic:
rfl

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
⊢ addZ (⇑f ∘ P) (⇑f ∘ Q) = f (addZ P Q)

Tactic:
simp only [addZ]
  map_simp

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

Goal state before:
pp: Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀'
K : Type u_7
inst✝ : Field K
v : Valuation K Γ₀
w : Valuation K Γ₀'
h : v.IsEquiv w
h1 : ∀ (x : UniformSpace.Completion (WithVal v)), Valued.v x ≤ 1 ↔ Valued.v.restrict x ≤ 1
x✝ : UniformSpace.Completion (WithVal v)
⊢ Valued.v ((mapEquiv h.uniformEquiv) x✝) ≤ 1 ↔ Valued.v ((mapEquiv h.uniformEquiv).toHomeomorph x✝) ≤ 1

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Interval.Finset.DenselyOrdered

Goal state before:
pp: X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered ↑s
x : X
hx : ↑x ∈ s
y : X
hy : ↑y ∈ s
hxy : x < y
⊢ ⟨↑x, hx⟩ < ⟨↑y, hy⟩

Tactic:
simp [hxy]

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

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

Tactic:
rfl

Goal state after: