mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: 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
x y : L
h : x ∈ K⟮y⟯
⊢ K⟮x⟯ ≤ K⟮y⟯

Tactic:
IntermediateField.adjoin_le_iff

Goal state after:
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
x y : L
h : x ∈ K⟮y⟯
⊢ {x} ⊆ ↑K⟮y⟯
Module: Mathlib.RingTheory.Smooth.AdicCompletion

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FormallySmooth R A
I : Ideal S
f : A →ₐ[R] S ⧸ I
⊢ ∃ g, (AlgHom.restrictScalars R (AdicCompletion.evalOneₐ I)).comp g = f

Tactic:
refine ⟨AdicCompletion.liftAlgHom I (liftAdicCompletionAux I f)
    (factorₐ_comp_liftAdicCompletionAux_of_le I f), ?_⟩

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FormallySmooth R A
I : Ideal S
f : A →ₐ[R] S ⧸ I
⊢ (AlgHom.restrictScalars R (AdicCompletion.evalOneₐ I)).comp
      (AdicCompletion.liftAlgHom I (liftAdicCompletionAux I f) ⋯) =
    f
Module: Mathlib.LinearAlgebra.Basis.Exact

Goal state before:
pp: case inr
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hfg : Function.Exact ⇑f ⇑g
κ : Type u_6
σ : Type u_7
v : κ ⊕ σ → M
hg : Function.Surjective ⇑g
hslzero : ∀ (i : κ), s (v (Sum.inl i)) = 0
hli : LinearIndependent R (⇑s ∘ v ∘ Sum.inr)
hsp : ⊤ ≤ Submodule.span R (Set.range v)
m : M
this :
  ∀ {R : Type u_1} {M : Type u_2} {K : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
    [inst_2 : AddCommGroup K] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R K]
    [inst_6 : Module R P] {f : K →ₗ[R] M} {g : M →ₗ[R] P} {s : M →ₗ[R] K},
    s ∘ₗ f = LinearMap.id →
      Function.Exact ⇑f ⇑g →
        ∀ {κ : Type u_6} {σ : Type u_7} (v : κ ⊕ σ → M),
          Function.Surjective ⇑g →
            (∀ (i : κ), s (v (Sum.inl i)) = 0) →
              LinearIndependent R (⇑s ∘ v ∘ Sum.inr) →
                ⊤ ≤ Submodule.span R (Set.range v) → ∀ m ∈ s.ker, g m ∈ Submodule.span R (Set.range (⇑g ∘ v ∘ Sum.inl))
h : m ∉ s.ker
x : M := f (s m)
hs : s (f (s m)) = s m
⊢ m - f (s m) ∈ s.ker

Tactic:
simp [hs]

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₀
h : Function.Surjective ⇑((↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp (Ideal.Quotient.mkₐ R P.ker))
⊢ (P.tensorModelOfHasCoeffsHom R₀).comp
      ((Ideal.Quotient.liftₐ P.ker
            ((TensorProduct.map (AlgHom.id R R)
                  (Ideal.Quotient.mkₐ R₀ (Ideal.span (Set.range (relationOfHasCoeffs R₀))))).comp
              ↑(MvPolynomial.algebraTensorAlgEquiv R₀ R).symm)
            ⋯).comp
        (((↑(AlgEquiv.restrictScalars R P.quotientEquiv).symm).comp ↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp
          (Ideal.Quotient.mkₐ R P.ker))) =
    (↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp (Ideal.Quotient.mkₐ R P.ker)

Tactic:
AlgEquiv.symm_comp,

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₀
h : Function.Surjective ⇑((↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp (Ideal.Quotient.mkₐ R P.ker))
⊢ (P.tensorModelOfHasCoeffsHom R₀).comp
      ((Ideal.Quotient.liftₐ P.ker
            ((TensorProduct.map (AlgHom.id R R)
                  (Ideal.Quotient.mkₐ R₀ (Ideal.span (Set.range (relationOfHasCoeffs R₀))))).comp
              ↑(MvPolynomial.algebraTensorAlgEquiv R₀ R).symm)
            ⋯).comp
        ((AlgHom.id R (P.Ring ⧸ P.ker)).comp (Ideal.Quotient.mkₐ R P.ker))) =
    (↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp (Ideal.Quotient.mkₐ R P.ker)
Module: Mathlib.RingTheory.Extension.Cotangent.Free

Goal state before:
pp: case hker
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
hfg : Function.Exact ⇑f ⇑g
⊢ Submodule.map (↑P.cotangentSpaceBasis.repr.symm) (P.toExtension.toKaehler ∘ₗ ↑P.cotangentSpaceBasis.repr.symm).ker ⊓
      Submodule.span S (Set.range fun x ↦ ↑P.cotangentSpaceBasis.repr.symm (Finsupp.single (v x) 1)) =
    Submodule.map ↑P.cotangentSpaceBasis.repr.symm ⊥

Tactic:
LinearMap.ker_comp,

Goal state after:
case hker
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
hfg : Function.Exact ⇑f ⇑g
⊢ Submodule.map (↑P.cotangentSpaceBasis.repr.symm)
        (Submodule.comap (↑P.cotangentSpaceBasis.repr.symm) P.toExtension.toKaehler.ker) ⊓
      Submodule.span S (Set.range fun x ↦ ↑P.cotangentSpaceBasis.repr.symm (Finsupp.single (v x) 1)) =
    Submodule.map ↑P.cotangentSpaceBasis.repr.symm ⊥
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case refine_1
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
⊢ Function.Surjective (⇑(algebraMap D.T S) ∘ ⇑(algebraMap P.Ring D.T))

Tactic:
convert! P.algebraMap_surjective

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
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ ⇑(algebraMap D.T S) ∘ ⇑(algebraMap P.Ring D.T) = ⇑(algebraMap P.Ring S)
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: case refine_3
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
inst✝¹ : Finite D.vars
inst✝ : Finite D.rels
⊢ (⋃ i, ⋃ x ∈ (D.q i).coeffs, ↑(coeffs x)).Finite

Tactic:
refine Set.finite_iUnion fun i ↦ ?_
    exact Set.Finite.biUnion (Finset.finite_toSet _) (fun i hi ↦ Finset.finite_toSet _)

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

Goal state before:
pp: case refine_4
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
inst✝¹ : Finite D.vars
inst✝ : Finite D.rels
⊢ (⋃ i, ⋃ x ∈ (D.p i).coeffs, ↑x.coeffs).Finite

Tactic:
refine Set.finite_iUnion fun i ↦ ?_
    exact Set.Finite.biUnion (Finset.finite_toSet _) (fun i hi ↦ Finset.finite_toSet _)

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

Goal state before:
pp: case 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
⊢ Presentation.ModelOfHasCoeffs ↥(subalgebra R D) →ₐ[↥(subalgebra R D)]
    MvPolynomial D.vars ↥(subalgebra R D) ⧸
      RingHom.ker
          (Ideal.Quotient.mkₐ (↥(subalgebra R D))
            (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))) ^
        2

Tactic:
refine Ideal.Quotient.liftₐ _ ((Ideal.Quotient.mkₐ _ _).comp <| aeval p) ?_
    simp_rw [← RingHom.mem_ker, ← SetLike.le_def, Ideal.span_le, Set.range_subset_iff]
    intro i
    simp only [← AlgHom.comap_ker, Ideal.coe_comap, Set.mem_preimage, SetLike.mem_coe]
    rw [← RingHom.ker_coe_toRingHom, Ideal.Quotient.mkₐ_ker,
      ← RingHom.ker_coe_toRingHom, Ideal.Quotient.mkₐ_ker]
    have hinj : Function.Injective
        (MvPolynomial.map (σ := D.vars) (algebraMap (D.subalgebra R) A)) :=
      map_injective _ (FaithfulSMul.algebraMap_injective (D.subalgebra R) A)
    rw [Ideal.mem_span_pow_iff_exists_isHomogeneous]
    obtain ⟨q, hq⟩ := (D.p i).mem_range_map_iff_coeffs_subset.mpr (D.coeffs_p_subset R i)
    refine ⟨q, .of_map hinj ?_, hinj ?_⟩
    · rw [hq]
      exact D.hphom i
    · simp_rw [map_eval, Function.comp_def, Presentation.map_relationOfHasCoeffs,
        hq, D.hp, MvPolynomial.map_aeval, hp]
      simp [MvPolynomial.eval₂_map_comp_C, Presentation.map_relationOfHasCoeffs, aeval_def]

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 := ⋯
J : Ideal P.Ring := ⋯
⊢ Function.Surjective ⇑(aeval P.val)

Tactic:
convert! P.algebraMap_surjective

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
α : 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))
⊢ ⇑(aeval P.val) = ⇑(algebraMap P.Ring S)
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:
by
    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.RingHom.LocallyStandardSmooth

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Locally (fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth) f
⊢ f.Smooth

Tactic:
rw [← locally_iff_of_localizationSpanTarget Smooth.propertyIsLocal.respectsIso
    Smooth.ofLocalizationSpanTarget]

Goal state after:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Locally (fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth) f
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ Smooth) f
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
⊢ ∃ 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:
by
  cases subsingleton_or_nontrivial S
  · 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 }
    have : Subsingleton P'.toExtension.Cotangent := Module.subsingleton S _
    exact ⟨P', default, by subsingleton, by subsingleton⟩
  have : Module.Finite S P.toExtension.Cotangent :=
    Algebra.Extension.Cotangent.finite P.fg_ker_of_finitePresentation
  exact exists_presentation_of_basis_cotangent _ <| Module.finBasis S P.toExtension.Cotangent

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
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
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
h₁ : (aeval a) q₁ = 0
ne : q₁ ≠ 0 ∧ q₂ ≠ 0
this : F.totalDegree ≤ q₁.totalDegree
⊢ IsUnit q₁ ∨ IsUnit q₂

Tactic:
rw [e, totalDegree_mul_of_isDomain ne.1 ne.2, add_le_iff_nonpos_right, nonpos_iff_eq_zero] at this

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 : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
h₁ : (aeval a) q₁ = 0
ne : q₁ ≠ 0 ∧ q₂ ≠ 0
this : q₂.totalDegree = 0
⊢ IsUnit q₁ ∨ IsUnit q₂
Module: Mathlib.AlgebraicGeometry.Morphisms.Proper

Goal state before:
pp: X : Scheme
K : Type u
inst✝² : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝¹ : IsIntegral X
inst✝ : UniversallyClosed f
F : CommRingCat.of K ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso (CommRingCat.of K)).inv ≫ Scheme.Hom.appTop f
⊢ IsField ↑Γ(X, ⊤)

Tactic:
have : F.hom.IsIntegral := by
    apply RingHom.isIntegral_respectsIso.2 (e := (Scheme.ΓSpecIso _).symm.commRingCatIsoToRingEquiv)
    exact isIntegral_appTop_of_universallyClosed f

Goal state after:
X : Scheme
K : Type u
inst✝² : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝¹ : IsIntegral X
inst✝ : UniversallyClosed f
F : CommRingCat.of K ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso (CommRingCat.of K)).inv ≫ Scheme.Hom.appTop f
this : (CommRingCat.Hom.hom F).IsIntegral
⊢ IsField ↑Γ(X, ⊤)
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 Q : Fin 3 → R
⊢ (W'.map f).addZ (⇑f ∘ P) (⇑f ∘ Q) = f (W'.addZ P Q)

Tactic:
by
  simp only [addZ]
  map_simp

Goal state after:
Module: Mathlib.RingTheory.RingHom.QuasiFinite

Goal state before:
pp: R S T : Type u_6
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
H : (algebraMap R T).QuasiFinite
⊢ (algebraMap S (TensorProduct R S T)).QuasiFinite

Tactic:
quasiFinite_algebraMap

Goal state after:
R S T : Type u_6
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
H : Algebra.QuasiFinite R T
⊢ Algebra.QuasiFinite S (TensorProduct R S T)
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal R
x : S
h✝ : Nontrivial R
p : (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x}))[X]
hp : p.Monic
e : eval₂ (algebraMap (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) S[X]) (C x * X) p = 0
q : R[X] := ∑ i ∈ Finset.range (p.natDegree + 1), C ((↑(p.coeff i)).coeff (p.natDegree - i)) * X ^ i
i : ℕ
hi : i ∈ Finset.range (p.natDegree + 1)
⊢ i ≤ p.natDegree

Tactic:
by simpa [Nat.lt_succ_iff] using! hi

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ ∀ {a b : S}, a ∈ {s | IsAlmostIntegral R s} → b ∈ {s | IsAlmostIntegral R s} → a * b ∈ {s | IsAlmostIntegral R s}

Tactic:
rintro a b ⟨r, hr, hr'⟩ ⟨s, hs, hs'⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
a b : S
r : R
hr : r ∈ R⁰
hr' : ∀ (n : ℕ), r • a ^ n ∈ (algebraMap R S).range
s : R
hs : s ∈ R⁰
hs' : ∀ (n : ℕ), s • b ^ n ∈ (algebraMap R S).range
⊢ a * b ∈ {s | IsAlmostIntegral R s}
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ ∀ {a b : S}, a ∈ {s | IsAlmostIntegral R s} → b ∈ {s | IsAlmostIntegral R s} → a + b ∈ {s | IsAlmostIntegral R s}

Tactic:
rintro a b ⟨r, hr, hr'⟩ ⟨s, hs, hs'⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
a b : S
r : R
hr : r ∈ R⁰
hr' : ∀ (n : ℕ), r • a ^ n ∈ (algebraMap R S).range
s : R
hs : s ∈ R⁰
hs' : ∀ (n : ℕ), s • b ^ n ∈ (algebraMap R S).range
⊢ a + b ∈ {s | IsAlmostIntegral R s}
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case neg
K : Type u_1
inst✝ : Field K
n : WithZero (Multiplicative ℤ)
hn0 : ¬n = 0
⊢ ∃ a, Valued.v a = n

Tactic:
use (RatFunc.X ^ (-WithZero.log n))
    simp [WithZero.exp_log hn0]

Goal state after:
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : QuasiFinite R (Localization.AtPrime p ⧸ Ideal.map (algebraMap R (Localization.AtPrime p)) (Ideal.under R p))
q : Ideal T
inst✝ : q.IsPrime
f : Localization.AtPrime p →ₐ[R] Localization.AtPrime q
hf : Function.Surjective ⇑f
⊢ Ideal.under R p ≤
    Ideal.comap ((↑f).comp (algebraMap R (Localization.AtPrime p)))
      (Ideal.map (algebraMap R (Localization.AtPrime q)) (Ideal.under R q))

Tactic:
AlgHom.comp_algebraMap_of_tower

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : QuasiFinite R (Localization.AtPrime p ⧸ Ideal.map (algebraMap R (Localization.AtPrime p)) (Ideal.under R p))
q : Ideal T
inst✝ : q.IsPrime
f : Localization.AtPrime p →ₐ[R] Localization.AtPrime q
hf : Function.Surjective ⇑f
⊢ Ideal.under R p ≤
    Ideal.comap (algebraMap R (Localization.AtPrime q))
      (Ideal.map (algebraMap R (Localization.AtPrime q)) (Ideal.under R q))
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: case mpr
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
x : ↥X
hx : x ∈ U.toOpens
⊢ (∃ i ∈ s, x ∈ X.basicOpen i) → ∃ V, (∃ f ∈ s, ∃ g, X.basicOpen (f * g) = V.toOpens) ∧ ∃ x_1, x ∈ V.toOpens

Tactic:
rintro ⟨f, hfs, hxf⟩

Goal state after:
case mpr
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
x : ↥X
hx : x ∈ U.toOpens
f : ↑Γ(X, ↑U)
hfs : f ∈ s
hxf : x ∈ X.basicOpen f
⊢ ∃ V, (∃ f ∈ s, ∃ g, X.basicOpen (f * g) = V.toOpens) ∧ ∃ x_1, x ∈ V.toOpens
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case inl
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
f : R⟮X⟯
p q p' q' : R[X]
hq : q ∈ R[X]⁰
hq' : q' ∈ R[X]⁰
h : q' * p = q * p'
h✝ : Subsingleton R
⊢ φ p / φ q = φ p' / φ q'

Tactic:
rw [Subsingleton.elim p q, Subsingleton.elim p' q, Subsingleton.elim q' q]

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case inl
K : Type u
inst✝⁵ : CommRing K
inst✝⁴ : IsDomain K
R : Type u_1
F : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F K[X] R[X]
inst✝ : MonoidWithZeroHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p : K[X]
⊢ (map φ hφ) ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) 0) =
    (algebraMap R[X] R⟮X⟯) (φ p) / (algebraMap R[X] R⟮X⟯) (φ 0)

Tactic:
have : (0 : K⟮X⟯) = algebraMap K[X] _ 0 / algebraMap K[X] _ 1 := by simp
    rw [map_zero, map_zero, map_zero, div_zero, div_zero, this, map_apply_div_ne_zero, map_one,
      map_one, div_one, map_zero, map_zero]
    exact one_ne_zero

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
y : ↥K[X]⁰
⊢ IsUnit ((algebraMap K[X] K⟮X⟯) ↑y)

Tactic:
← ofFractionRing_algebraMap

Goal state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
y : ↥K[X]⁰
⊢ IsUnit { toFractionRing := (algebraMap K[X] (FractionRing K[X])) ↑y }
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
x y : K[X]
⊢ { toFractionRing := (algebraMap K[X] (FractionRing K[X])) x } = (algebraMap K[X] K⟮X⟯) y → ∃ c, ↑c * x = ↑c * y

Tactic:
← ofFractionRing_algebraMap

Goal state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
x y : K[X]
⊢ { toFractionRing := (algebraMap K[X] (FractionRing K[X])) x } =
      { toFractionRing := (algebraMap K[X] (FractionRing K[X])) y } →
    ∃ c, ↑c * x = ↑c * y
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsStandardEtale R S
Sₛ : Type u_4
inst✝⁴ : CommRing Sₛ
inst✝³ : Algebra S Sₛ
inst✝² : Algebra R Sₛ
inst✝¹ : IsScalarTower R S Sₛ
s : S
inst✝ : IsLocalization.Away s Sₛ
⊢ IsStandardEtale R Sₛ

Tactic:
have P : StandardEtalePresentation R S := IsStandardEtale.nonempty_standardEtalePresentation.some

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsStandardEtale R S
Sₛ : Type u_4
inst✝⁴ : CommRing Sₛ
inst✝³ : Algebra S Sₛ
inst✝² : Algebra R Sₛ
inst✝¹ : IsScalarTower R S Sₛ
s : S
inst✝ : IsLocalization.Away s Sₛ
P : StandardEtalePresentation R S
⊢ IsStandardEtale R Sₛ