mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: case hS
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Limits.HasPullbacks C
K : Precoverage C
inst✝ : K.IsStableUnderBaseChange
S : C
F : Cᵒᵖ ⥤ Type u_2
𝒰 : K.ZeroHypercover S
𝒱 : K.ZeroHypercover S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
⊢ Presieve.IsSheafFor F (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f)).arrows

Tactic:
← Presieve.isSheafFor_iff_generate

Goal state after:
case hS
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Limits.HasPullbacks C
K : Precoverage C
inst✝ : K.IsStableUnderBaseChange
S : C
F : Cᵒᵖ ⥤ Type u_2
𝒰 : K.ZeroHypercover S
𝒱 : K.ZeroHypercover S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
⊢ Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: case refine_1
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
E : PreOneHypercover X
F : Cᵒᵖ ⥤ Type u_2
h : E.IsStronglySheafFor F
s t : (E.multifork F).pt
hst : (E.multifork F).toSections s = (E.multifork F).toSections t
⊢ s = t

pp: case refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
E : PreOneHypercover X
F : Cᵒᵖ ⥤ Type u_2
h : E.IsStronglySheafFor F
s : (E.multicospanIndex F).sections
⊢ ∃ a, (E.multifork F).toSections a = s

Tactic:
· exact h.isSheafFor_presieve₀.isSeparatedFor.ext fun _ _ ⟨i⟩ ↦ congr($(hst).val i)

Goal state after:
case refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
E : PreOneHypercover X
F : Cᵒᵖ ⥤ Type u_2
h : E.IsStronglySheafFor F
s : (E.multicospanIndex F).sections
⊢ ∃ a, (E.multifork F).toSections a = s
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.addY P (W'.neg P) = -W'.dblZ P

Tactic:
by
  simp only [addY, addX_neg, negAddY_neg hP, addZ_neg, negY, fin3_def_ext, mul_zero, sub_zero]

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

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
⊢ W.Nonsingular (W.add P Q)

Tactic:
· by_cases hxy : P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z
      · by_cases hy : P y * Q z = Q y * P z
        · simp only [add_of_Y_eq hP.left hPz hQz hxy.left hy hxy.right, nonsingular_smul _ <|
              isUnit_dblU_of_Y_eq hP hPz hQz hxy.left hy hxy.right, nonsingular_zero]
        · simp only [add_of_Y_ne hP.left hQ.left hPz hQz hxy.left hy,
            nonsingular_smul _ <| isUnit_addU_of_Y_ne hPz hQz hy, nonsingular_zero]
      · classical
        have := nonsingular_add_of_Z_ne_zero hP hQ hPz hQz hxy
        by_cases hx : P x * Q z = Q x * P z
        · simpa only [add_of_Y_ne' hP.left hQ.left hPz hQz hx <| not_and.mp hxy hx,
            nonsingular_smul _ <| isUnit_dblZ_of_Y_ne' hP.left hQ.left hPz hQz hx <|
              not_and.mp hxy hx]
        · simpa only [add_of_X_ne hP.left hQ.left hPz hQz hx,
            nonsingular_smul _ <| isUnit_addZ_of_X_ne hP.left hQ.left hx]

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Nonsingular P
hPz : P z = 0
hPy : P y = 0
⊢ False

Tactic:
simp only [nonsingular_of_Z_eq_zero hPz, X_eq_zero_of_Z_eq_zero hP.left hPz, hPy, add_zero,
    sub_zero, mul_zero, zero_pow two_ne_zero, or_self, ne_self_iff_false, and_false] at hP

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type s
inst✝ : CommRing S
f : R →+* S
⊢ (W'.map f).polynomialX = (MvPolynomial.map f) W'.polynomialX

Tactic:
by
  simp only [polynomialX, map_polynomial, pderiv_map]

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

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective ⇑f
P : Fin 3 → A
⊢ (W'⁄B).Nonsingular (⇑f ∘ P) ↔ (W'⁄A).Nonsingular P

Tactic:
by
  rw [← RingHom.coe_coe, ← map_nonsingular _ hf, AlgHom.toRingHom_eq_coe, map_baseChange]

Goal state after:
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: case refine_6
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
hg₃ : ∀ (x y : L) (h : x ∈ K⟮y⟯), (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)
H : ∀ (x y : L), ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯
⊢ (Ideal.Quotient.mkₐ K I).comp
      { toFun := fun x ↦ (g x) (IntermediateField.AdjoinSimple.gen K x), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
        map_add' := ⋯, commutes' := ⋯ } =
    f

Tactic:
ext x
    simpa using AlgHom.congr_fun (hg₁ x) (IntermediateField.AdjoinSimple.gen K x)

Goal state after:
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : S
a : A
⊢ (tensorKaehlerEquiv R S A (S ⊗[R] A)).symm ((D S (S ⊗[R] A)) (s ⊗ₜ[R] a)) =
    (algebraMap S (S ⊗[R] A)) s ⊗ₜ[A] (D R A) a

Tactic:
apply (tensorKaehlerEquiv R S A _).symm_apply_eq.mpr ?_
  simp only [Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply,
    tensorKaehlerEquiv_tmul_D]
  rw [show s ⊗ₜ 1 = algebraMap S (S ⊗ A) s by simp, Algebra.TensorProduct.right_algebraMap_apply,
    algebraMap_smul, ← Derivation.map_smul, smul_tmul', smul_eq_mul, mul_one]

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: S : Type u_5
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsAdicComplete I S
x : AdicCompletion I S
⊢ (Ideal.Quotient.mk I) ((ofAlgEquiv I).symm x) = (evalOneₐ I) x

Tactic:
by
  simp [evalOneₐ, ← mk_ofAlgEquiv_symm]

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.Core

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Presentation R S ι σ
R₀ : Type u_5
inst✝⁴ : CommRing R₀
inst✝³ : Algebra R₀ R
inst✝² : Algebra R₀ S
inst✝¹ : IsScalarTower R₀ R S
inst✝ : P.HasCoeffs R₀
x : MvPolynomial ι R₀
⊢ (P.tensorModelOfHasCoeffsInv R₀) ((algebraMap P.Ring S) ((MvPolynomial.map (algebraMap R₀ R)) x)) =
    1 ⊗ₜ[R₀] (Ideal.Quotient.mk (Ideal.span (Set.range (relationOfHasCoeffs R₀)))) x

Tactic:
← quotientEquiv_mk

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Presentation R S ι σ
R₀ : Type u_5
inst✝⁴ : CommRing R₀
inst✝³ : Algebra R₀ R
inst✝² : Algebra R₀ S
inst✝¹ : IsScalarTower R₀ R S
inst✝ : P.HasCoeffs R₀
x : MvPolynomial ι R₀
⊢ (P.tensorModelOfHasCoeffsInv R₀)
      (P.quotientEquiv ((Ideal.Quotient.mk P.ker) ((MvPolynomial.map (algebraMap R₀ R)) x))) =
    1 ⊗ₜ[R₀] (Ideal.Quotient.mk (Ideal.span (Set.range (relationOfHasCoeffs R₀)))) x
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
x : P.toExtension.CotangentSpace
y : P.toExtension.Cotangent
⊢ (∀ (x_1 : σ),
      P.cotangentEquiv
          (P.cotangentEquiv.symm
            ((Finsupp.linearEquivFunOnFinite S S σ) ((Finsupp.lcomapDomain P.map ⋯) (P.cotangentSpaceBasis.repr x))))
          x_1 =
        P.cotangentEquiv y x_1) ↔
    ∀ (i : σ), (P.cotangentSpaceBasis.repr x) (P.map i) = P.cotangentComplexAux y i

Tactic:
LinearEquiv.apply_symm_apply

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
x : P.toExtension.CotangentSpace
y : P.toExtension.Cotangent
⊢ (∀ (x_1 : σ),
      (Finsupp.linearEquivFunOnFinite S S σ) ((Finsupp.lcomapDomain P.map ⋯) (P.cotangentSpaceBasis.repr x)) x_1 =
        P.cotangentEquiv y x_1) ↔
    ∀ (i : σ), (P.cotangentSpaceBasis.repr x) (P.map i) = P.cotangentComplexAux y i
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hQz : Q z = 0
⊢ -(P y * 0 - Q y * P z) ^ 3 / (P z * 0) = 0

Tactic:
mul_zero <| P z,

Goal state after:
F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hQz : Q z = 0
⊢ -(P y * 0 - Q y * P z) ^ 3 / 0 = 0
Module: Mathlib.RingTheory.RingHom.Etale

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
algInst✝ : Algebra R S := f.toAlgebra
⊢ Algebra.Etale R S ↔ Module.Flat R S ∧ Algebra.FormallyUnramified R S ∧ (algebraMap R S).FinitePresentation

Tactic:
RingHom.finitePresentation_algebraMap

Goal state after:
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
algInst✝ : Algebra R S := f.toAlgebra
⊢ Algebra.Etale R S ↔ Module.Flat R S ∧ Algebra.FormallyUnramified R S ∧ Algebra.FinitePresentation R S
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ✝ : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
i : σ
⊢ ((AlgebraTensorModule.curry (D.tensorCotangentInv ∘ₗ D.tensorCotangentHom)) 1) (Extension.Cotangent.mk (D.kerGen i)) =
    ((AlgebraTensorModule.curry LinearMap.id) 1) (Extension.Cotangent.mk (D.kerGen i))

Tactic:
simp [-toExtension_commRing, -toExtension_Ring, -toExtension_algebra₂, tensorCotangentHom_tmul,
      kerGen, D.hf]

Goal state after:
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: case refine_2.refine_1
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
hf₀ :
  Function.Surjective
    ⇑(Ideal.Quotient.mkₐ (↥(subalgebra R D))
        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D)))))
i : D.vars
hinj : Function.Injective ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
t : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
ht : (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))) t = D.q i
⊢ (D.q i).IsHomogeneous 1

Tactic:
exact D.hqhom i

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝ : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h✝ : Subsingleton S
⊢ ∃ P' b, P'.val ∘ Sum.inr = P.val ∧ ∀ (r : Unit ⊕ σ), b r = Extension.Cotangent.mk ⟨P'.relation r, ⋯⟩

Tactic:
let P' : Presentation R S (Unit ⊕ α) (Unit ⊕ σ) :=
      { toGenerators := .ofSurjective (fun i : Unit ⊕ α ↦ 0) (Function.surjective_to_subsingleton _)
        relation _ := 1
        span_range_relation_eq_ker := by simpa using (RingHom.ker_eq_top_of_subsingleton _).symm }

Goal state after:
case inl
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝ : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h✝ : Subsingleton S
P' : Presentation R S (Unit ⊕ α) (Unit ⊕ σ) :=
  let __Generators := ofSurjective (fun i ↦ 0) ⋯;
  { toGenerators := __Generators, relation := fun x ↦ 1, span_range_relation_eq_ker := ⋯ }
⊢ ∃ P' b, P'.val ∘ Sum.inr = P.val ∧ ∀ (r : Unit ⊕ σ), b r = Extension.Cotangent.mk ⟨P'.relation r, ⋯⟩
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝ : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h✝ : Subsingleton S
P' : Presentation R S (Unit ⊕ α) (Unit ⊕ σ) :=
  let __Generators := ofSurjective (fun i ↦ 0) ⋯;
  { toGenerators := __Generators, relation := fun x ↦ 1, span_range_relation_eq_ker := ⋯ }
this : Subsingleton P'.toExtension.Cotangent
⊢ P'.val ∘ Sum.inr = P.val

Tactic:
by subsingleton

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝ : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h✝ : Subsingleton S
P' : Presentation R S (Unit ⊕ α) (Unit ⊕ σ) :=
  let __Generators := ofSurjective (fun i ↦ 0) ⋯;
  { toGenerators := __Generators, relation := fun x ↦ 1, span_range_relation_eq_ker := ⋯ }
this : Subsingleton P'.toExtension.Cotangent
⊢ ∀ (r : Unit ⊕ σ), default r = Extension.Cotangent.mk ⟨P'.relation r, ⋯⟩

Tactic:
by subsingleton

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝ : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h✝ : Nontrivial S
f : P.toExtension.Cotangent → ↥P.toExtension.ker
hf : ∀ (b : P.toExtension.Cotangent), Extension.Cotangent.mk (f b) = b
v : σ → ↥P.ker := fun i ↦ f (b₀ i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val ∘ v))
hJfg : P.ker.FG
hJ✝ : J ≤ P.ker
hJ : P.ker ≤ J ⊔ P.ker • P.ker
⊢ ∃ P' b, P'.val ∘ Sum.inr = P.val ∧ ∀ (r : Unit ⊕ σ), b r = Extension.Cotangent.mk ⟨P'.relation r, ⋯⟩

Tactic:
obtain ⟨g, hgmem, hg⟩ := Submodule.exists_sub_one_mem_and_smul_le_of_fg_of_le_sup hJfg le_rfl hJ
    let D : Aux P b₀ := { f := f, hf := hf, g := g, hgmem := hgmem, hg := hg }
    exact ⟨D.pres, D.basis, D.pres_val_comp_inr, D.basis_apply⟩

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝¹ : Finite α
inst✝ : Module.Free S P.toExtension.Cotangent
h✝ : Subsingleton S
P' : Presentation R S (Unit ⊕ α) (Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)) :=
  let __Generators := ofSurjective (fun i ↦ 0) ⋯;
  { toGenerators := __Generators, relation := fun x ↦ 1, span_range_relation_eq_ker := ⋯ }
this : Subsingleton P'.toExtension.Cotangent
⊢ P'.val ∘ Sum.inr = P.val

Tactic:
by subsingleton

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝¹ : Finite α
inst✝ : Module.Free S P.toExtension.Cotangent
h✝ : Subsingleton S
P' : Presentation R S (Unit ⊕ α) (Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)) :=
  let __Generators := ofSurjective (fun i ↦ 0) ⋯;
  { toGenerators := __Generators, relation := fun x ↦ 1, span_range_relation_eq_ker := ⋯ }
this : Subsingleton P'.toExtension.Cotangent
⊢ ∀ (r : Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)), default r = Extension.Cotangent.mk ⟨P'.relation r, ⋯⟩

Tactic:
by subsingleton

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
p : ℕ
hp : Nat.Prime p
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
this : ∀ (i : ι), ∀ σ ∈ F.support, p ∣ σ i
σ' : (ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ σ ∈ F.support, σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), ↑σ = p • σ' ↑σ
H : ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K), LinearIndependent k v → LinearIndependent k fun x ↦ v x ^ p
⊢ ∃ s g, ∑ i ∈ s, g i • (aeval a) ((monomial ↑i) 1) = 0 ∧ ∃ i ∈ s, g i ≠ 0

Tactic:
refine ⟨.univ, (F.coeff ·), ?_, by simpa [MvPolynomial.eq_zero_iff] using! hF0⟩

Goal state after:
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
p : ℕ
hp : Nat.Prime p
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
this : ∀ (i : ι), ∀ σ ∈ F.support, p ∣ σ i
σ' : (ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ σ ∈ F.support, σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), ↑σ = p • σ' ↑σ
H : ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K), LinearIndependent k v → LinearIndependent k fun x ↦ v x ^ p
⊢ ∑ i, (fun x ↦ coeff (↑x) F) i • (aeval a) ((monomial ↑i) 1) = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ W.addY P Q = W.addY P Q * (P z * Q z) ^ 3 / (P z * Q z) ^ (2 + 1)

Tactic:
mul_div_cancel_right₀ _ <| pow_ne_zero 3 <| mul_ne_zero hPz hQz

Goal state after:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ W.addY P Q = W.addY P Q
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
n : ι
inst✝ : ExpChar k p
ha' : IsTranscendenceBasis k fun i ↦ a ↑i
S : Set (MvPolynomial ι k) := {F | F ≠ 0 ∧ (aeval a) F = 0}
h : AlgebraicIndependent k a
⊢ a '' {n}ᶜ = Set.range fun x ↦ a ↑x

Tactic:
aesop

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
n : ι
inst✝ : ExpChar k p
ha' : IsTranscendenceBasis k fun i ↦ a ↑i
S : Set (MvPolynomial ι k) := {F | F ≠ 0 ∧ (aeval a) F = 0}
F : MvPolynomial ι k
hFmin : ∀ (G : MvPolynomial ι k), G ≠ 0 → (aeval a) G = 0 → F.totalDegree ≤ G.totalDegree
hF₀ : F ≠ 0
hFa : (aeval a) F = 0
hFirr : Irreducible F
i : ι
σ : ι →₀ ℕ
hσ : σ ∈ F.support
hi : ¬p ∣ σ i
⊢ σ i ≠ 0

Tactic:
aesop

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: X Y Z' Z : Scheme
i : Z' ⟶ Z
inst✝¹ : IsClosedImmersion i
f : X ⟶ Y
inst✝ : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
n : ℕ
hn : Scheme.Hom.ker i ^ n = 0
⊢ DenseRange ⇑i

Tactic:
denseRange_iff_closure_range,

Goal state after:
X Y Z' Z : Scheme
i : Z' ⟶ Z
inst✝¹ : IsClosedImmersion i
f : X ⟶ Y
inst✝ : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
n : ℕ
hn : Scheme.Hom.ker i ^ n = 0
⊢ closure (Set.range ⇑i) = Set.univ
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
inst✝ : ExpChar k p
s : Set ι
n : ι
ha : IsTranscendenceBasis k fun i ↦ a ↑i
hn : n ∉ s
x : { j // j ≠ ⟨n, ⋯⟩ }
⊢ ↑↑x ∈ s

Tactic:
aesop

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
inst✝ : ExpChar k p
s : Set ι
n : ι
ha : IsTranscendenceBasis k fun i ↦ a ↑i
hn : n ∉ s
x : ↑s
⊢ ↑x ∈ insert n s

Tactic:
aesop

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
inst✝ : ExpChar k p
s : Set ι
n : ι
ha : IsTranscendenceBasis k fun i ↦ a ↑i
hn : n ∉ s
x : ↑s
⊢ ⟨↑x, ⋯⟩ ≠ ⟨n, ⋯⟩

Tactic:
aesop

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
inst✝ : ExpChar k p
s : Set ι
n : ι
ha : IsTranscendenceBasis k fun i ↦ a ↑i
hn : n ∉ s
e₁ : { j // j ≠ ⟨n, ⋯⟩ } ≃ ↑s :=
  { toFun := fun x ↦ ⟨↑↑x, ⋯⟩, invFun := fun x ↦ ⟨⟨↑x, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
i : ↑(insert n s)
hi : IsTranscendenceBasis k fun j ↦ a ↑↑j
hi' : IsSeparable (↥(adjoin k ((fun i ↦ a ↑i) '' {i}ᶜ))) (a ↑i)
e₂ : { j // j ≠ i } ≃ ↑(insert n s \ {↑i}) :=
  { toFun := fun x ↦ ⟨↑↑x, ⋯⟩, invFun := fun x ↦ ⟨⟨↑x, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
x✝ : K
⊢ x✝ ∈ a '' (insert n s \ {↑i}) ↔ x✝ ∈ (fun x ↦ a ↑x) '' {i}ᶜ

Tactic:
aesop

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

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Projective R
f : R →+* S
P : Fin 3 → R
⊢ (W'.map f).dblY (⇑f ∘ P) = f (W'.dblY P)

Tactic:
by
  simp only [dblY, negY_eq, map_negDblY, map_dblX, map_dblZ]
  map_simp

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

Goal state before:
pp: R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Projective R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (W'⁄B).dblXYZ (⇑↑f ∘ P) = ⇑↑f ∘ (W'⁄A).dblXYZ P

Tactic:
← map_dblXYZ,

Goal state after:
R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Projective R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (W'⁄B).dblXYZ (⇑↑f ∘ P) = ((W'⁄A).map ↑f).dblXYZ (⇑↑f ∘ P)