mathlib-initiative/mathlib-tactics huggingface dataset:
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 ι σ
r : σ
⊢ P.cotangentEquiv (Cotangent.mk ⟨P.relation r, ⋯⟩) = P.cotangentEquiv (P.basisCotangent r)

Tactic:
ext

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 ι σ
r x✝ : σ
⊢ P.cotangentEquiv (Cotangent.mk ⟨P.relation r, ⋯⟩) x✝ = P.cotangentEquiv (P.basisCotangent r) x✝
Module: Mathlib.RingTheory.Extension.Cotangent.Free

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_3
σ : Type u_4
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
hm : Submodule.span S (Set.range fun i ↦ (D R S) (P.val (v i))) = ⊤
hk : Disjoint P.toExtension.toKaehler.ker (Submodule.span S (Set.range fun x ↦ P.cotangentSpaceBasis (v x)))
inst✝ : Subsingleton (H1Cotangent R S)
f : P.toExtension.Cotangent →ₗ[S] ι →₀ S := ↑P.cotangentSpaceBasis.repr ∘ₗ P.toExtension.cotangentComplex
⊢ Function.Bijective
    ⇑(LinearMap.linearProjOfIsCompl (Submodule.span S (Set.range fun x ↦ Finsupp.single (v x) 1))
          (Finsupp.lmapDomain S S u) ⋯ ⋯ ∘ₗ
        f)

Tactic:
let g : (ι →₀ S) →ₗ[S] (Ω[S⁄R]) := P.toExtension.toKaehler ∘ₗ P.cotangentSpaceBasis.repr.symm

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_3
σ : Type u_4
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
hm : Submodule.span S (Set.range fun i ↦ (D R S) (P.val (v i))) = ⊤
hk : Disjoint P.toExtension.toKaehler.ker (Submodule.span S (Set.range fun x ↦ P.cotangentSpaceBasis (v x)))
inst✝ : Subsingleton (H1Cotangent R S)
f : P.toExtension.Cotangent →ₗ[S] ι →₀ S := ↑P.cotangentSpaceBasis.repr ∘ₗ P.toExtension.cotangentComplex
g : (ι →₀ S) →ₗ[S] Ω[S⁄R] := P.toExtension.toKaehler ∘ₗ ↑P.cotangentSpaceBasis.repr.symm
⊢ Function.Bijective
    ⇑(LinearMap.linearProjOfIsCompl (Submodule.span S (Set.range fun x ↦ Finsupp.single (v x) 1))
          (Finsupp.lmapDomain S S u) ⋯ ⋯ ∘ₗ
        f)
Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree

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
inst✝ : Subsingleton (H1Cotangent R S)
I : Type u_3
b : Module.Basis I S Ω[S⁄R]
a✝ : Nontrivial S
n : ℕ
P✝ : Generators R S (Fin n)
f' : ⦃a : Ω[S⁄R]⦄ → a ∈ Set.range ⇑b → S
hf' : ∀ ⦃a : Ω[S⁄R]⦄ (a_1 : a ∈ Set.range ⇑b), (D R S) (f' a_1) = a
P : Generators R S (Fin n ⊕ I) := P✝.extend fun i ↦ f' ⋯
hb : ∀ (i : I), b i = (D R S) (P.val (Sum.inr i))
this✝ : Function.Bijective ⇑(P.cotangentRestrict ⋯)
bcot' : Module.Basis (Fin n) S P.toExtension.Cotangent :=
  { repr := LinearEquiv.ofBijective (P.cotangentRestrict ⋯) this✝ }
this : Finite I
⊢ IsStandardSmooth R S

Tactic:
obtain ⟨Q, bcot, hcomp, hbcot⟩ := P.exists_presentation_of_basis_cotangent bcot'

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FinitePresentation R S
inst✝ : Subsingleton (H1Cotangent R S)
I : Type u_3
b : Module.Basis I S Ω[S⁄R]
a✝ : Nontrivial S
n : ℕ
P✝ : Generators R S (Fin n)
f' : ⦃a : Ω[S⁄R]⦄ → a ∈ Set.range ⇑b → S
hf' : ∀ ⦃a : Ω[S⁄R]⦄ (a_1 : a ∈ Set.range ⇑b), (D R S) (f' a_1) = a
P : Generators R S (Fin n ⊕ I) := P✝.extend fun i ↦ f' ⋯
hb : ∀ (i : I), b i = (D R S) (P.val (Sum.inr i))
this✝ : Function.Bijective ⇑(P.cotangentRestrict ⋯)
bcot' : Module.Basis (Fin n) S P.toExtension.Cotangent :=
  { repr := LinearEquiv.ofBijective (P.cotangentRestrict ⋯) this✝ }
this : Finite I
Q : Presentation R S (Unit ⊕ Fin n ⊕ I) (Unit ⊕ Fin n)
bcot : Module.Basis (Unit ⊕ Fin n) S Q.toExtension.Cotangent
hcomp : Q.val ∘ Sum.inr = P.val
hbcot : ∀ (r : Unit ⊕ Fin n), bcot r = Extension.Cotangent.mk ⟨Q.relation r, ⋯⟩
⊢ IsStandardSmooth R S
Module: Mathlib.RingTheory.RingHom.Etale

Goal state before:
pp: ⊢ @Etale = fun R S x x_1 f ↦ f.FormallyUnramified ∧ f.Smooth

Tactic:
ext

Goal state after:
x✝⁴ : Type u_6
x✝³ : Type u_5
x✝² : CommRing x✝⁴
x✝¹ : CommRing x✝³
x✝ : x✝⁴ →+* x✝³
⊢ x✝.Etale ↔ x✝.FormallyUnramified ∧ x✝.Smooth
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmooth R T
⊢ inst✝ = (algebraMap R T).toAlgebra

Tactic:
ext

Goal state after:
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmooth R T
r✝ : R
x✝ : T
⊢ (have I := inst✝;
    r✝ • x✝) =
    r✝ • x✝
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmooth R T
this : Algebra.IsStandardSmooth S (S ⊗[R] T)
⊢ (algebraMap S (S ⊗[R] T)).toAlgebra = Algebra.TensorProduct.leftAlgebra

Tactic:
ext

Goal state after:
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmooth R T
this : Algebra.IsStandardSmooth S (S ⊗[R] T)
r✝ : S
x✝ : S ⊗[R] T
⊢ (have I := (algebraMap S (S ⊗[R] T)).toAlgebra;
    r✝ • x✝) =
    r✝ • x✝
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
⊢ inst✝ = (algebraMap R T).toAlgebra

Tactic:
ext

Goal state after:
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
r✝ : R
x✝ : T
⊢ (have I := inst✝;
    r✝ • x✝) =
    r✝ • x✝
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
this : Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
⊢ (algebraMap S (S ⊗[R] T)).toAlgebra = Algebra.TensorProduct.leftAlgebra

Tactic:
ext

Goal state after:
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
this : Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
r✝ : S
x✝ : S ⊗[R] T
⊢ (have I := (algebraMap S (S ⊗[R] T)).toAlgebra;
    r✝ • x✝) =
    r✝ • x✝
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
Rᵣ : Type u_2
inst✝² : CommRing Rᵣ
inst✝¹ : Algebra R Rᵣ
r : R
inst✝ : IsLocalization.Away r Rᵣ
⊢ (algebraMap R Rᵣ).toAlgebra = inst✝¹

Tactic:
ext

Goal state after:
R : Type u
inst✝³ : CommRing R
Rᵣ : Type u_2
inst✝² : CommRing Rᵣ
inst✝¹ : Algebra R Rᵣ
r : R
inst✝ : IsLocalization.Away r Rᵣ
r✝ : R
x✝ : Rᵣ
⊢ (have I := (algebraMap R Rᵣ).toAlgebra;
    r✝ • x✝) =
    r✝ • x✝
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
r : σ
⊢ (LinearMap.liftBaseChange S
        (Extension.Cotangent.map ((localizationAway S D.gbar).toComp D.presLeft.toGenerators).toExtensionHom))
      (D.basisLeft r) =
    Extension.Cotangent.mk ⟨D.pres.relation (Sum.inr r), ⋯⟩

Tactic:
basisLeft,

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
r : σ
⊢ (LinearMap.liftBaseChange S
        (Extension.Cotangent.map ((localizationAway S D.gbar).toComp D.presLeft.toGenerators).toExtensionHom))
      ((b.map D.tensorCotangentEquiv.symm) r) =
    Extension.Cotangent.mk ⟨D.pres.relation (Sum.inr r), ⋯⟩
Module: Mathlib.RingTheory.RingHom.LocallyStandardSmooth

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ f.Etale ↔ IsStandardSmoothOfRelativeDimension 0 f

Tactic:
by
  algebraize [f]
  exact Algebra.Etale.iff_isStandardSmoothOfRelativeDimension_zero

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 α
inst✝ : Module.Free S P.toExtension.Cotangent
h✝ : Subsingleton S
⊢ ∃ P' b,
    P'.val ∘ Sum.inr = P.val ∧
      ∀ (r : Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)), b r = Extension.Cotangent.mk ⟨P'.relation r, ⋯⟩

Tactic:
let P' : Presentation R S (Unit ⊕ α) (Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)) :=
      { 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 α
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 := ⋯ }
⊢ ∃ P' b,
    P'.val ∘ Sum.inr = P.val ∧
      ∀ (r : Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)), b r = Extension.Cotangent.mk ⟨P'.relation r, ⋯⟩
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
a : ι → K
F : MvPolynomial ι k
hFa : (aeval a) F = 0
i : ι
⊢ (AlgHom.restrictScalars k (Polynomial.aeval (a i))).comp
      ((Polynomial.mapAlgHom (aeval fun j ↦ ⟨a ↑j, ⋯⟩)).comp
        ((↑(optionEquivLeft k { b // b ≠ i })).comp ↑(renameEquiv k (Equiv.optionSubtypeNe i).symm))) =
    aeval a

Tactic:
ext

Goal state after:
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
hFa : (aeval a) F = 0
i i✝ : ι
⊢ ((AlgHom.restrictScalars k (Polynomial.aeval (a i))).comp
        ((Polynomial.mapAlgHom (aeval fun j ↦ ⟨a ↑j, ⋯⟩)).comp
          ((↑(optionEquivLeft k { b // b ≠ i })).comp ↑(renameEquiv k (Equiv.optionSubtypeNe i).symm))))
      (X i✝) =
    (aeval a) (X i✝)
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
a : ι → K
F : MvPolynomial ι k
hF : Irreducible F
i : ι
H : AlgebraicIndependent k fun x ↦ a ↑x
⊢ a '' {i}ᶜ = Set.range fun x ↦ a ↑x

Tactic:
ext

Goal state after:
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
hF : Irreducible F
i : ι
H : AlgebraicIndependent k fun x ↦ a ↑x
x✝ : K
⊢ x✝ ∈ a '' {i}ᶜ ↔ x✝ ∈ Set.range fun x ↦ a ↑x
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
a : ι → K
F : MvPolynomial ι k
hF : Irreducible F
i : ι
H : AlgebraicIndependent k fun x ↦ a ↑x
hc : a '' {i}ᶜ = Set.range fun x ↦ a ↑x
d : { j // j ≠ i } ≃ ↑{j | j ≠ i} := Equiv.subtypeEquivRight ⋯
⊢ ↑((renameEquiv k d).trans
        (H.aevalEquiv.trans ((Algebra.adjoin k (Set.range fun x ↦ a ↑x)).equivOfEq (Algebra.adjoin k (a '' {i}ᶜ)) ⋯))) =
    ↑(aeval fun j ↦ ⟨a ↑j, ⋯⟩)

Tactic:
ext

Goal state after:
case hC
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
hF : Irreducible F
i : ι
H : AlgebraicIndependent k fun x ↦ a ↑x
hc : a '' {i}ᶜ = Set.range fun x ↦ a ↑x
d : { j // j ≠ i } ≃ ↑{j | j ≠ i} := ⋯
x✝ : k
⊢ ↑(((↑((renameEquiv k d).trans
                (H.aevalEquiv.trans
                  ((Algebra.adjoin k (Set.range fun x ↦ a ↑x)).equivOfEq (Algebra.adjoin k (a '' {i}ᶜ)) ⋯)))).comp
          C)
        x✝) =
    ↑(((↑(aeval fun j ↦ ⟨a ↑j, ⋯⟩)).comp C) x✝)

case hX
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
hF : Irreducible F
i : ι
H : AlgebraicIndependent k fun x ↦ a ↑x
hc : a '' {i}ᶜ = Set.range fun x ↦ a ↑x
d : { j // j ≠ i } ≃ ↑{j | j ≠ i} := ⋯
i✝ : { j // j ≠ i }
⊢ ↑(↑((renameEquiv k d).trans
            (H.aevalEquiv.trans
              ((Algebra.adjoin k (Set.range fun x ↦ a ↑x)).equivOfEq (Algebra.adjoin k (a '' {i}ᶜ)) ⋯)))
        (X i✝)) =
    ↑(↑(aeval fun j ↦ ⟨a ↑j, ⋯⟩) (X i✝))
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
a : ι → K
F : MvPolynomial ι k
hF : Irreducible F
i : ι
H : AlgebraicIndependent k fun x ↦ a ↑x
hc : a '' {i}ᶜ = Set.range fun x ↦ a ↑x
d : { j // j ≠ i } ≃ ↑{j | j ≠ i} := Equiv.subtypeEquivRight ⋯
⊢ ↑((renameEquiv k d).trans
        (H.aevalEquiv.trans ((Algebra.adjoin k (Set.range fun x ↦ a ↑x)).equivOfEq (Algebra.adjoin k (a '' {i}ᶜ)) ⋯))) =
    ↑(aeval fun j ↦ ⟨a ↑j, ⋯⟩)

Tactic:
ext <;> simp [d]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ⇑f ⁻¹' U.carrier
this✝¹ : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
algInst✝ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algebraizeInst✝ : Algebra.FinitePresentation ↑Γ(Y, U) ↑Γ(X, V)
this✝ : Algebra.IsSmoothAt (↑Γ(Y, U)) (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
r : ↑Γ(X, V)
hrx : r ∉ (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
hr : (algebraMap (↑Γ(Y, U)) (Localization.Away r)).Smooth
this : IsLocalization.Away r ↑Γ(X, X.basicOpen r)
⊢ CommRingCat.Hom.hom (Scheme.Hom.appLE f U (X.basicOpen r) ⋯) =
    (IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) ↑Γ(X, X.basicOpen r)).toRingEquiv.toRingHom.comp
      (algebraMap (↑Γ(Y, U)) (Localization.Away r))

Tactic:
ext

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ⇑f ⁻¹' U.carrier
this✝¹ : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
algInst✝ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algebraizeInst✝ : Algebra.FinitePresentation ↑Γ(Y, U) ↑Γ(X, V)
this✝ : Algebra.IsSmoothAt (↑Γ(Y, U)) (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
r : ↑Γ(X, V)
hrx : r ∉ (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
hr : (algebraMap (↑Γ(Y, U)) (Localization.Away r)).Smooth
this : IsLocalization.Away r ↑Γ(X, X.basicOpen r)
x✝ : ↑Γ(Y, U)
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U (X.basicOpen r) ⋯)) x✝ =
    ((IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r)
                ↑Γ(X, X.basicOpen r)).toRingEquiv.toRingHom.comp
        (algebraMap (↑Γ(Y, U)) (Localization.Away r)))
      x✝
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case refine_2
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : σ i ≠ 0
F₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H :
  (Algebra.adjoin k (a '' {i}ᶜ)).val
      ((aeval fun j ↦ ⟨a ↑j, ⋯⟩)
        (((optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)).coeff (σ i))) =
    0
⊢ (aeval a).comp (rename Subtype.val) = (Algebra.adjoin k (a '' {i}ᶜ)).val.comp (aeval fun j ↦ ⟨a ↑j, ⋯⟩)

Tactic:
ext

Goal state after:
case refine_2
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : σ i ≠ 0
F₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H :
  (Algebra.adjoin k (a '' {i}ᶜ)).val
      ((aeval fun j ↦ ⟨a ↑j, ⋯⟩)
        (((optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)).coeff (σ i))) =
    0
i✝ : { b // b ≠ i }
⊢ ((aeval a).comp (rename Subtype.val)) (X i✝) =
    ((Algebra.adjoin k (a '' {i}ᶜ)).val.comp (aeval fun j ↦ ⟨a ↑j, ⋯⟩)) (X i✝)
Module: Mathlib.AlgebraicGeometry.Morphisms.Etale

Goal state before:
pp: R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ @RingHom.Etale = @RingHom.IsStandardSmoothOfRelativeDimension 0

Tactic:
ext

Goal state after:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x✝⁴ : Type ?u.17
x✝³ : Type ?u.16
x✝² : CommRing x✝⁴
x✝¹ : CommRing x✝³
x✝ : x✝⁴ →+* x✝³
⊢ x✝.Etale ↔ RingHom.IsStandardSmoothOfRelativeDimension 0 x✝
Module: Mathlib.AlgebraicGeometry.Morphisms.Etale

Goal state before:
pp: case hPi
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
this : @RingHom.Etale = @RingHom.IsStandardSmoothOfRelativeDimension 0
⊢ RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ RingHom.Etale

pp: case hPs
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
this : @RingHom.Etale = @RingHom.IsStandardSmoothOfRelativeDimension 0
⊢ RingHom.OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] ↦ RingHom.Etale

Tactic:
· exact RingHom.Etale.respectsIso

Goal state after:
case hPs
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
this : @RingHom.Etale = @RingHom.IsStandardSmoothOfRelativeDimension 0
⊢ RingHom.OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] ↦ RingHom.Etale
Module: Mathlib.AlgebraicGeometry.Morphisms.Etale

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hf : Etale f
⊢ (@LocallyOfFiniteType ⊓ @FormallyUnramified) f

Tactic:
constructor

Goal state after:
case left
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hf : Etale f
⊢ LocallyOfFiniteType f

case right
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hf : Etale f
⊢ FormallyUnramified f
Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso

Goal state before:
pp: ⊢ @IsLocalIso = sourceLocalClosure IsOpenImmersion IsOpenImmersion

Tactic:
ext

Goal state after:
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsLocalIso x✝ ↔ sourceLocalClosure IsOpenImmersion IsOpenImmersion x✝
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
⊢ IsOpenImmersion (pullback.diagonal f)

Tactic:
by
  wlog hX : (∃ S, X = Spec S) ∧ ∃ R, Y = Spec R
  · let 𝒰Y := Y.affineCover
    let 𝒰X (j : (Y.affineCover.pullback₁ f).I₀) :
        ((Y.affineCover.pullback₁ f).X j).OpenCover := Scheme.affineCover _
    apply IsZariskiLocalAtTarget.of_range_subset_iSup _
      (Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange f 𝒰Y 𝒰X)
    intro ⟨i, j⟩
    rw [arrow_mk_iso_iff (P := @IsOpenImmersion)
      (Scheme.Pullback.diagonalRestrictIsoDiagonal f 𝒰Y 𝒰X i j)]
    have hu : FormallyUnramified ((𝒰X i).f j ≫ pullback.snd f (𝒰Y.f i)) :=
      comp_mem _ _ _ inferInstance (pullback_snd _ _ inferInstance)
    have hfin : LocallyOfFiniteType ((𝒰X i).f j ≫ pullback.snd f (𝒰Y.f i)) :=
      comp_mem _ _ _ inferInstance (pullback_snd _ _ inferInstance)
    exact this _ ⟨⟨_, rfl⟩, ⟨_, rfl⟩⟩
  obtain ⟨⟨S, rfl⟩, R, rfl⟩ := hX
  obtain ⟨f, rfl⟩ := Spec.map_surjective f
  rw [HasRingHomProperty.Spec_iff (P := @FormallyUnramified),
    HasRingHomProperty.Spec_iff (P := @LocallyOfFiniteType)] at *
  algebraize [f.hom]
  rw [show f = CommRingCat.ofHom (algebraMap R S) from rfl, diagonal_SpecMap R S,
    cancel_right_of_respectsIso (P := @IsOpenImmersion)]
  infer_instance

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).dblX (⇑f ∘ P) = f (W'.dblX P)

Tactic:
by
  simp only [dblX]
  map_simp

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 := ⋯ }
⊢ a '' (insert n s \ {↑i}) = (fun x ↦ a ↑x) '' {i}ᶜ

Tactic:
ext

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
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}ᶜ