mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Smooth.Local

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : IsLocalRing S
inst✝¹¹ : Algebra R S
P : Type u_3
K : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CommRing P
inst✝⁸ : Algebra R P
inst✝⁷ : Algebra P S
inst✝⁶ : IsScalarTower R P S
inst✝⁵ : Algebra S K
inst✝⁴ : Algebra P K
inst✝³ : IsScalarTower P S K
inst✝² : FormallySmooth R P
inst✝¹ : Module.Free P Ω[P⁄R]
inst✝ : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective ⇑(algebraMap P S)
h₂ : (RingHom.ker (algebraMap P S)).FG
h₃ : maximalIdeal S ≤ RingHom.ker (algebraMap S K)
f : ResidueField S →ₐ[S] K := Ideal.Quotient.liftₐ (maximalIdeal S) (ofId S K) h₃
this : Algebra (ResidueField S) K := f.toAlgebra
⊢ FormallySmooth R S ↔ Function.Injective ⇑(cotangentComplexBaseChange R S P K)

Tactic:
have := IsScalarTower.of_algebraMap_eq' f.comp_algebraMap.symm

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : IsLocalRing S
inst✝¹¹ : Algebra R S
P : Type u_3
K : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CommRing P
inst✝⁸ : Algebra R P
inst✝⁷ : Algebra P S
inst✝⁶ : IsScalarTower R P S
inst✝⁵ : Algebra S K
inst✝⁴ : Algebra P K
inst✝³ : IsScalarTower P S K
inst✝² : FormallySmooth R P
inst✝¹ : Module.Free P Ω[P⁄R]
inst✝ : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective ⇑(algebraMap P S)
h₂ : (RingHom.ker (algebraMap P S)).FG
h₃ : maximalIdeal S ≤ RingHom.ker (algebraMap S K)
f : ResidueField S →ₐ[S] K := Ideal.Quotient.liftₐ (maximalIdeal S) (ofId S K) h₃
this✝ : Algebra (ResidueField S) K := f.toAlgebra
this : IsScalarTower S (ResidueField S) K
⊢ FormallySmooth R S ↔ Function.Injective ⇑(cotangentComplexBaseChange R S P K)
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: case mp
K : Type u_1
A : Type u
inst✝³ : Field K
inst✝² : CommRing A
inst✝¹ : Algebra K A
inst✝ : EssFiniteType K A
⊢ FormallyEtale K A → ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Algebra.IsSeparable K (Ai i)

pp: case mpr
K : Type u_1
A : Type u
inst✝³ : Field K
inst✝² : CommRing A
inst✝¹ : Algebra K A
inst✝ : EssFiniteType K A
⊢ (∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Algebra.IsSeparable K (Ai i)) → FormallyEtale K A

Tactic:
· intro H
    have := FormallyUnramified.finite_of_free K A
    have := FormallyUnramified.isReduced_of_field K A
    have : IsArtinianRing A := isArtinian_of_tower K inferInstance
    let v (i : MaximalSpectrum A) : A := (IsArtinianRing.equivPi A).symm (Pi.single i 1)
    rw [FormallyEtale.iff_of_equiv ((IsArtinianRing.equivPi A).restrictScalars K),
      FormallyEtale.pi_iff] at H
    exact ⟨_, inferInstance, _, _, _, (IsArtinianRing.equivPi A).restrictScalars K,
      fun I ↦ (iff_isSeparable _ _).mp inferInstance⟩

Goal state after:
case mpr
K : Type u_1
A : Type u
inst✝³ : Field K
inst✝² : CommRing A
inst✝¹ : Algebra K A
inst✝ : EssFiniteType K A
⊢ (∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Algebra.IsSeparable K (Ai i)) → FormallyEtale K A
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
x : Ω[B⁄S]
⊢ (LinearMap.liftBaseChange S (↑R (map R S A B))).toFun ((derivationTensorProduct R S A B).liftKaehlerDifferential x) =
    x

Tactic:
by
    obtain ⟨x, rfl⟩ := tensorProductTo_surjective _ _ x
    dsimp
    induction x with
    | zero => simp
    | add x y e₁ e₂ => simp only [map_add, e₁, e₂]
    | tmul x y =>
      -- We use the specialized version of `map_smul` here for performance.
      simp only [Derivation.tensorProductTo_tmul, LinearMap.map_smul,
        Derivation.liftKaehlerDifferential_comp_D, map_liftBaseChange_smul]
      induction y using h.1.inductionOn
      · simp only [map_zero, smul_zero]
      · simp only [AlgHom.toLinearMap_apply, IsScalarTower.coe_toAlgHom',
          derivationTensorProduct_algebraMap, LinearMap.liftBaseChange_tmul,
          LinearMap.coe_restrictScalars, map_D, one_smul]
      · -- We use the specialized version of `map_smul` here for performance.
        simp only [Derivation.map_smul, LinearMap.map_smul, *, smul_comm x]
      · simp only [map_add, smul_add, *]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Flat R S
inst✝⁹ : CommRing P
inst✝⁸ : Algebra R P
inst✝⁷ : Algebra P S
inst✝⁶ : IsScalarTower R P S
inst✝⁵ : IsLocalRing R
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalHom (algebraMap R S)
inst✝² : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
M : Submonoid P
inst✝¹ : IsLocalization M S
inst✝ : FinitePresentation R P
n : ℕ
f₀ : MvPolynomial (Fin n) R →ₐ[R] P
hf₀ : Function.Surjective ⇑f₀
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
fP : P' →ₐ[R] S := IsLocalization.liftAlgHom ⋯
hf₁ : Function.Surjective ⇑fP
this : (RingHom.ker f₀.toRingHom).FG
x : MvPolynomial (Fin n) R
hx : x ∈ RingHom.ker f₀.toRingHom
⊢ x ∈ Ideal.comap (algebraMap (MvPolynomial (Fin n) R) P') (RingHom.ker fP)

Tactic:
by simp_all [fP]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
j : ι
x : AdicCauchySequence I (M j)
i : ι
n : ℕ
⊢ Submodule.Quotient.mk (if h : j = i then Eq.recOn h (↑x n) else 0) =
    ↑(if h : j = i then Eq.recOn h ((mk I (M j)) x) else 0) n

Tactic:
split

Goal state after:
case isTrue
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
j : ι
x : AdicCauchySequence I (M j)
i : ι
n : ℕ
h✝ : j = i
⊢ Submodule.Quotient.mk (Eq.recOn h✝ (↑x n)) = ↑(Eq.recOn h✝ ((mk I (M j)) x)) n

case isFalse
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
j : ι
x : AdicCauchySequence I (M j)
i : ι
n : ℕ
h✝ : ¬j = i
⊢ Submodule.Quotient.mk 0 = ↑0 n
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : ℕ → R
hx : x ∈ submodule I R
hy : y ∈ submodule I R
m n : ℕ
hmn : m ≤ n
⊢ (x * y) m ≡ (x * y) n [SMOD I ^ m • ⊤]

Tactic:
simp only [Pi.mul_apply]

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : ℕ → R
hx : x ∈ submodule I R
hy : y ∈ submodule I R
m n : ℕ
hmn : m ≤ n
⊢ x m * y m ≡ x n * y n [SMOD I ^ m • ⊤]
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: case zero
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
y : AdicCompletion I N
⊢ { m // Submodule.Quotient.mk (f m) = (eval I N 0) y }

Tactic:
use 0

Goal state after:
case property
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
y : AdicCompletion I N
⊢ Submodule.Quotient.mk (f 0) = (eval I N 0) y
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
y : AdicCompletion I N
x : (n : ℕ) → { m // Submodule.Quotient.mk (f m) = (eval I N n) y } :=
  fun n ↦ Nat.recAux ⟨0, ⋯⟩ (fun n xn ↦ (fun z hz ↦ ⟨z, ⋯⟩) (Classical.choose ⋯) ⋯) n
⊢ ∃ x, ∀ (n : ℕ), x n ≡ x (n + 1) [SMOD I ^ n • ⊤] ∧ Submodule.Quotient.mk (f (x n)) = (eval I N n) y

Tactic:
exact ⟨fun n ↦ (x n).val, fun n ↦ ⟨(Classical.choose_spec (exists_smodEq_pow_smul_top_and_mkQ_eq
      h (y' := eval I _ (n + 1) y) (by simp) (x n).2)).1, (x n).property⟩⟩

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j : ι
k : ℕ
⊢ (if j = i then 1 else 0) = ↑(if j = i then 1 else 0) k

Tactic:
split

Goal state after:
case isTrue
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j : ι
k : ℕ
h✝ : j = i
⊢ 1 = ↑1 k

case isFalse
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j : ι
k : ℕ
h✝ : ¬j = i
⊢ 0 = ↑0 k
Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ofTensorProduct I (ι → R) =
    ↑(piEquivOfFintype I fun x ↦ R).symm ∘ₗ ↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι)

Tactic:
← piEquivOfFintype_comp_ofTensorProduct_eq I ι,

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ofTensorProduct I (ι → R) =
    ↑(piEquivOfFintype I fun x ↦ R).symm ∘ₗ ↑(piEquivOfFintype I fun x ↦ R) ∘ₗ ofTensorProduct I (ι → R)
Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct

Goal state before:
pp: case hg
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective ⇑p
f : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M := ⋯
g : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M := ⋯
hfg : f = g
⊢ Function.Surjective ⇑(map I p)

pp: case hf
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective ⇑p
f : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M := ⋯
g : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M := ⋯
hfg : f = g
⊢ Function.Surjective ⇑(ofTensorProduct I (Fin n → R))

Tactic:
· exact AdicCompletion.map_surjective I hp

Goal state after:
case hf
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective ⇑p
f : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M := ⋯
g : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M := ⋯
hfg : f = g
⊢ Function.Surjective ⇑(ofTensorProduct I (Fin n → R))
Module: Mathlib.LinearAlgebra.Basis.Exact

Goal state before:
pp: 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
hfg : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
p q : Submodule R M
hpq : IsCompl p q
hker : Disjoint g.ker q
hmap : map g q = ⊤
⊢ Function.Bijective ⇑(p.projectionOnto q hpq ∘ₗ f)

Tactic:
refine ⟨?_, Submodule.projectionOnto_comp_surjective_of_exact hfg _ hmap⟩
  rwa [LinearMap.coe_comp, Set.InjOn.injective_iff ↑(LinearMap.range f) _ subset_rfl]
  simpa [← LinearMap.disjoint_ker_iff_injOn, ← hfg.linearMap_ker_eq]

Goal state after:
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✝ : IsStandardSmooth R S
⊢ Free S Ω[S⁄R]

Tactic:
obtain ⟨_, _, _, _, ⟨P⟩⟩ := ‹IsStandardSmooth R S›
  exact P.free_kaehlerDifferential

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
⊢ ![u ^ 4 * W'.dblX P, u ^ 4 * W'.dblY P, u ^ 4 * W'.dblZ P] =
    ![u ^ 4 * W'.dblX P, u ^ 4 * W'.dblXYZ P y, u ^ 4 * W'.dblXYZ P z]

Tactic:
dblXYZ_Y,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
⊢ ![u ^ 4 * W'.dblX P, u ^ 4 * W'.dblY P, u ^ 4 * W'.dblZ P] =
    ![u ^ 4 * W'.dblX P, u ^ 4 * W'.dblY P, u ^ 4 * W'.dblXYZ P z]
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
⊢ IsStandardSmooth R S ↔ Subsingleton (H1Cotangent R S) ∧ ∃ I b, Set.range ⇑b ⊆ Set.range ⇑(D R S)

Tactic:
by
  refine ⟨fun h ↦ ⟨inferInstance, ?_⟩, fun ⟨h, ⟨_, b, hb⟩⟩ ↦ .of_basis_kaehlerDifferential b hb⟩
  obtain ⟨ι, σ, _, _, ⟨P⟩⟩ := Algebra.IsStandardSmooth.out (R := R) (S := S)
  exact ⟨_, P.basisKaehler, by simp [Set.range_subset_iff]⟩

Goal state after:
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✝ : Smooth R S
f : (p : Ideal S) → [inst : p.IsPrime] → [IsSmoothAt R p] → S
hf₁ : ∀ (p : Ideal S) [inst : p.IsPrime] [inst_1 : IsSmoothAt R p], f p ∉ p
hf₂ : ∀ (p : Ideal S) [inst : p.IsPrime] [inst_1 : IsSmoothAt R p], IsStandardSmooth R (Localization.Away (f p))
a✝ : PrimeSpectrum S
⊢ IsStandardSmooth R (Localization.Away (f a✝.asIdeal))

Tactic:
apply hf₂

Goal state after:
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

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:
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
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.RingHom.StandardSmooth

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsStandardSmooth
⊢ ∃ n g, g.comp MvPolynomial.C = f ∧ g.Etale

Tactic:
obtain ⟨_, _, _, _, ⟨P⟩⟩ := hf

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
w✝² w✝¹ : Type
w✝ : _root_.Finite w✝¹
left✝ : _root_.Finite w✝²
P : Algebra.SubmersivePresentation R S w✝² w✝¹
⊢ ∃ n g, g.comp MvPolynomial.C = f ∧ g.Etale
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [FormallyUnramified f] [LocallyOfFiniteType f],
    ((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R) → IsOpenImmersion (pullback.diagonal f)
hX : ¬((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R)
𝒰Y : Y.OpenCover := ⋯
𝒰X : (j : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀) →
  ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X j).OpenCover := ⋯
⊢ ∀ (i : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) × (𝒰X i).I₀),
    IsOpenImmersion
      (pullback.diagonal f ∣_ Scheme.Hom.opensRange ((Scheme.Pullback.diagonalCover f 𝒰Y 𝒰X).f ⟨i.fst, (i.snd, i.snd)⟩))

Tactic:
intro ⟨i, j⟩

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [FormallyUnramified f] [LocallyOfFiniteType f],
    ((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R) → IsOpenImmersion (pullback.diagonal f)
hX : ¬((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R)
𝒰Y : Y.OpenCover := Y.affineCover
𝒰X : (j : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀) →
  ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X j).OpenCover :=
  fun j ↦ ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X j).affineCover
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀
j : (𝒰X i).I₀
⊢ IsOpenImmersion
    (pullback.diagonal f ∣_
      Scheme.Hom.opensRange ((Scheme.Pullback.diagonalCover f 𝒰Y 𝒰X).f ⟨⟨i, j⟩.fst, (⟨i, j⟩.snd, ⟨i, j⟩.snd)⟩))
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [FormallyUnramified f] [LocallyOfFiniteType f],
    ((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R) → IsOpenImmersion (pullback.diagonal f)
hX : ¬((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R)
𝒰Y : Y.OpenCover := Y.affineCover
𝒰X : (j : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀) →
  ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X j).OpenCover :=
  fun j ↦ ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X j).affineCover
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀
j : (𝒰X i).I₀
hu : FormallyUnramified ((𝒰X i).f j ≫ pullback.snd f (𝒰Y.f i))
⊢ IsOpenImmersion (pullback.diagonal ((𝒰X i).f j ≫ pullback.snd f (𝒰Y.f i)))

Tactic:
have hfin : LocallyOfFiniteType ((𝒰X i).f j ≫ pullback.snd f (𝒰Y.f i)) :=
      comp_mem _ _ _ inferInstance (pullback_snd _ _ inferInstance)

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [FormallyUnramified f] [LocallyOfFiniteType f],
    ((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R) → IsOpenImmersion (pullback.diagonal f)
hX : ¬((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R)
𝒰Y : Y.OpenCover := Y.affineCover
𝒰X : (j : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀) →
  ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X j).OpenCover :=
  fun j ↦ ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X j).affineCover
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀
j : (𝒰X i).I₀
hu : FormallyUnramified ((𝒰X i).f j ≫ pullback.snd f (𝒰Y.f i))
hfin : LocallyOfFiniteType ((𝒰X i).f j ≫ pullback.snd f (𝒰Y.f i))
⊢ IsOpenImmersion (pullback.diagonal ((𝒰X i).f j ≫ pullback.snd f (𝒰Y.f i)))
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
h✝ : CharZero k
s : Finset K
hs : adjoin k ↑s = ⊤
⊢ Algebra.IsAlgebraic (↥(adjoin k ↑s)) K

Tactic:
hs,

Goal state after:
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
h✝ : CharZero k
s : Finset K
hs : adjoin k ↑s = ⊤
⊢ Algebra.IsAlgebraic (↥⊤) K
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal R
x : S
hx : IsIntegral (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) (C x * X)
h✝ : Subsingleton R
⊢ ∃ p, p.Monic ∧ (aeval x) p = 0 ∧ ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)

Tactic:
use 0

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal R
x : S
hx : IsIntegral (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) (C x * X)
h✝ : Subsingleton R
⊢ Monic 0 ∧ (aeval x) 0 = 0 ∧ ∀ (i : ℕ), coeff 0 i ∈ I ^ (natDegree 0 - i)
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
⊢ eval f a (x * y) = eval f a x * eval f a y

Tactic:
by
  unfold eval
  by_cases hxy : Polynomial.eval₂ f a (denom (x * y)) = 0
  · have := Polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero f a (denom_mul_dvd x y) hxy
    rw [Polynomial.eval₂_mul] at this
    cases mul_eq_zero.mp this <;> contradiction
  rw [div_mul_div_comm, eq_div_iff (mul_ne_zero hx hy), div_eq_mul_inv, mul_right_comm, ←
    div_eq_mul_inv, div_eq_iff hxy]
  repeat' rw [← Polynomial.eval₂_mul]
  congr 1
  apply num_denom_mul

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

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

Tactic:
use 0

Goal state after:
case h
K : Type u_1
inst✝ : Field K
n : WithZero (Multiplicative ℤ)
hn0 : n = 0
⊢ Valued.v 0 = n
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

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
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp (mapRingHom (algebraMap R I.ResidueField))) ⋯ ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
x✝ : I.ResidueField[X]
x : I.ResidueField[X]
hx : (aeval ((algebraMap R[X] J.ResidueField) X)) x = 0
r : R[X]
hr : map (Ideal.Quotient.mk I) r = IsLocalization.integerNormalization (R ⧸ I)⁰ x
b : R ⧸ I
hb0 : b ∈ (R ⧸ I)⁰
hb : map (algebraMap (R ⧸ I) I.ResidueField) (IsLocalization.integerNormalization (R ⧸ I)⁰ x) = b • x
⊢ ∃ s ∉ I, map (algebraMap R I.ResidueField) r = s • x

Tactic:
obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective b

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
I : Ideal R
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp (mapRingHom (algebraMap R I.ResidueField))) ⋯ ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
x✝ : I.ResidueField[X]
x : I.ResidueField[X]
hx : (aeval ((algebraMap R[X] J.ResidueField) X)) x = 0
r : R[X]
hr : map (Ideal.Quotient.mk I) r = IsLocalization.integerNormalization (R ⧸ I)⁰ x
s : R
hb0 : (Ideal.Quotient.mk I) s ∈ (R ⧸ I)⁰
hb :
  map (algebraMap (R ⧸ I) I.ResidueField) (IsLocalization.integerNormalization (R ⧸ I)⁰ x) = (Ideal.Quotient.mk I) s • x
⊢ ∃ s ∉ I, map (algebraMap R I.ResidueField) r = s • x