mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Unramified.Pi

Goal state before:
pp: case map_one
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := Pi.single x 1
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := Ideal.span {1 - f₁ e}
f₁' : f x →ₐ[R] B ⧸ J' :=
  AlgHom.ofLinearMap (((Ideal.Quotient.mkₐ R J').comp f₁).toLinearMap ∘ₗ LinearMap.single R f x) ⋯ ⋯
⊢ (Ideal.Quotient.mk J') (1 - f₂ (Pi.single x 1)) = 0

Tactic:
Ideal.Quotient.eq_zero_iff_mem,

Goal state after:
case map_one
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := Pi.single x 1
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := Ideal.span {1 - f₁ e}
f₁' : f x →ₐ[R] B ⧸ J' :=
  AlgHom.ofLinearMap (((Ideal.Quotient.mkₐ R J').comp f₁).toLinearMap ∘ₗ LinearMap.single R f x) ⋯ ⋯
⊢ 1 - f₂ (Pi.single x 1) ∈ J'
Module: Mathlib.RingTheory.Etale.Locus

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
⊢ Module.support A Ω[A⁄R] ⊆ (↑(PrimeSpectrum.basicOpen f))ᶜ ∧
      ↑(PrimeSpectrum.basicOpen f) ⊆ (Module.support A (H1Cotangent R A))ᶜ ↔
    FormallyEtale R (Localization.Away f)

Tactic:
PrimeSpectrum.basicOpen_eq_zeroLocus_compl,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
⊢ Module.support A Ω[A⁄R] ⊆ (PrimeSpectrum.zeroLocus {f})ᶜᶜ ∧
      (PrimeSpectrum.zeroLocus {f})ᶜ ⊆ (Module.support A (H1Cotangent R A))ᶜ ↔
    FormallyEtale R (Localization.Away f)
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
this✝ : Algebra.IsPushout R A S B
e₁ : B ⊗[A] Ω[A⁄R] ≃ₗ[A] Ω[A⁄R] ⊗[R] S :=
  AlgebraTensorModule.congr (↑(Algebra.IsPushout.equiv R A S B).symm) (LinearEquiv.refl A Ω[A⁄R]) ≪≫ₗ
      TensorProduct.comm A (A ⊗[R] S) Ω[A⁄R] ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S
e₂ : B ⊗[A] Ω[A⁄R] ≃ₗ[R] Ω[B⁄S] :=
  LinearEquiv.restrictScalars R e₁ ≪≫ₗ TensorProduct.comm R Ω[A⁄R] S ≪≫ₗ
    LinearEquiv.restrictScalars R (tensorKaehlerEquivBase R S A B)
a : A
b : S
y : Ω[A⁄R]
x : A
z : S
this : b • z • a • x • (map R S A B) y = ((algebraMap A B) a * (algebraMap S B) b) • z • x • (map R S A B) y
⊢ e₂ ((Algebra.IsPushout.equiv R A S B) (a ⊗ₜ[R] b) • (Algebra.IsPushout.equiv R A S B) (x ⊗ₜ[R] z) ⊗ₜ[A] y) =
    (Algebra.IsPushout.equiv R A S B) (a ⊗ₜ[R] b) • e₂ ((Algebra.IsPushout.equiv R A S B) (x ⊗ₜ[R] z) ⊗ₜ[A] y)

Tactic:
simpa [e₂, e₁, smul_tmul', Algebra.IsPushout.equiv_tmul, ← mul_smul,
      Algebra.IsPushout.equiv_symm_algebraMap_left, Algebra.IsPushout.equiv_symm_algebraMap_right]

Goal state after:
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
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
ι : Type u_5
κ : Type u_6
σ : Type u_7
v : ι → M
a : κ → ι
b : σ → ι
hg : Function.Surjective ⇑g
hsa : ∀ (i : κ), s (v (a i)) = 0
hlib : LinearIndependent R (⇑s ∘ v ∘ b)
hab : Codisjoint (Set.range a) (Set.range b)
hsp : ⊤ ≤ span R (Set.range v)
⊢ ⊤ ≤ span R (Set.range (⇑g ∘ v ∘ a))

Tactic:
by
  apply top_le_span_of_aux hs hfg (Sum.elim (v ∘ a) (v ∘ b)) hg hsa hlib
  simp only [codisjoint_iff, Set.sup_eq_union, Set.top_eq_univ] at hab
  rwa [Set.Sum.elim_range, Set.range_comp, Set.range_comp, ← Set.image_union, hab, Set.image_univ]

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✝ : Finite σ
P : SubmersivePresentation R S ι σ
⊢ IsCompl (Set.range Subtype.val) (Set.range P.map)

Tactic:
rw [Subtype.range_coe_subtype]
    exact IsCompl.symm isCompl_compl

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

Goal state before:
pp: case hsp
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 : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
b : Module.Basis σ S P.toExtension.Cotangent
hb : ∀ (r : σ), b r = Extension.Cotangent.mk ⟨P.relation r, ⋯⟩
h : Function.Bijective ⇑(P.cotangentRestrict ⋯)
heq :
  (fun j i ↦ (aeval P.val) ((pderiv (P.map i)) (P.relation j))) =
    ⇑(Finsupp.linearEquivFunOnFinite S S σ) ∘ ⇑(P.cotangentRestrict ⋯) ∘ ⇑b
⊢ (↑(Finsupp.linearEquivFunOnFinite S S σ)).range = ⊤

Tactic:
LinearEquiv.range

Goal state after:
case hsp
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 : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
b : Module.Basis σ S P.toExtension.Cotangent
hb : ∀ (r : σ), b r = Extension.Cotangent.mk ⟨P.relation r, ⋯⟩
h : Function.Bijective ⇑(P.cotangentRestrict ⋯)
heq :
  (fun j i ↦ (aeval P.val) ((pderiv (P.map i)) (P.relation j))) =
    ⇑(Finsupp.linearEquivFunOnFinite S S σ) ∘ ⇑(P.cotangentRestrict ⋯) ∘ ⇑b
⊢ ⊤ = ⊤
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
hsple :
  ∀ {x : ((localizationAway T g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
x : ((localizationAway T g).comp P).Ring
hx : x ∈ Ideal.map ((localizationAway T g).toComp P).toAlgHom P.ker
y : ((localizationAway T g).comp P).Ring
⊢ y ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} →
    x * y ∈ RingHom.ker (compLocalizationAwayAlgHom T g P)

Tactic:
hy

Goal state after:
case a
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
hsple :
  ∀ {x : ((localizationAway T g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
x : ((localizationAway T g).comp P).Ring
hx : x ∈ Ideal.map ((localizationAway T g).toComp P).toAlgHom P.ker
y : ((localizationAway T g).comp P).Ring
hy : y ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1}
⊢ x * y ∈ RingHom.ker (compLocalizationAwayAlgHom T g P)
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: case a.a
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
hsple :
  ∀ {x : ((localizationAway T g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
x : ((localizationAway T g).comp P).Ring
hx : x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1}
y : ((localizationAway T g).comp P).Ring
⊢ y ∈ Ideal.map ((localizationAway T g).toComp P).toAlgHom P.ker →
    x * y ∈ RingHom.ker (compLocalizationAwayAlgHom T g P)

Tactic:
hy

Goal state after:
case a.a
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
hsple :
  ∀ {x : ((localizationAway T g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
x : ((localizationAway T g).comp P).Ring
hx : x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1}
y : ((localizationAway T g).comp P).Ring
hy : y ∈ Ideal.map ((localizationAway T g).toComp P).toAlgHom P.ker
⊢ x * y ∈ RingHom.ker (compLocalizationAwayAlgHom T g P)
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
hsple :
  ∀ {x : ((localizationAway T g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
x : ((localizationAway T g).comp P).Ring
hx : x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1}
y : ((localizationAway T g).comp P).Ring
⊢ y ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} →
    x * y ∈ RingHom.ker (compLocalizationAwayAlgHom T g P)

Tactic:
hy

Goal state after:
case a
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
hsple :
  ∀ {x : ((localizationAway T g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
x : ((localizationAway T g).comp P).Ring
hx : x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1}
y : ((localizationAway T g).comp P).Ring
hy : y ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1}
⊢ x * y ∈ RingHom.ker (compLocalizationAwayAlgHom T g P)
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
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
⊢ ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)

Tactic:
wlog h : Smooth R S
  · obtain ⟨g, hg, hsm⟩ := IsSmoothAt.exists_notMem_smooth R p
    have _ : (Ideal.map (algebraMap S (Localization.Away g)) p).IsPrime := by
      apply IsLocalization.isPrime_of_isPrime_disjoint (.powers g) _ _ ‹_›
      rwa [Ideal.disjoint_powers_iff_notMem_of_isPrime]
    obtain ⟨g', hg', hstd⟩ := this (R := R) (p.map (algebraMap S (Localization.Away g))) hsm
    have : IsLocalization.Away (g * (IsLocalization.Away.sec g g').1) (Localization.Away g') :=
      .mul_of_associated _ _ g' <| IsLocalization.Away.associated_sec_fst g g'
    let e : Localization.Away (g * (IsLocalization.Away.sec g g').1) ≃ₐ[S] Localization.Away g' :=
      Localization.algEquiv _ _
    refine ⟨g * (IsLocalization.Away.sec g g').1, ?_, .of_algEquiv (e.restrictScalars R).symm⟩
    refine Ideal.IsPrime.mul_notMem ‹_› hg fun hmem ↦ hg' ?_
    rw [Ideal.mem_iff_of_associated (IsLocalization.Away.associated_sec_fst g g').symm]
    exact Ideal.mem_map_of_mem (algebraMap S (Localization.Away g)) hmem
  -- `Ω[Sₚ⁄R]` is projective, so free over the local ring `Sₚ` and
  -- a basis extends to a neighbourhood `D(g)`.
  obtain ⟨κ, a, b, hb⟩ := Module.exists_basis_of_span_of_flat _
    (span_range_map_derivation_of_isLocalization R _ (Localization.AtPrime p) p.primeCompl)
  let e : (κ →₀ S) →ₗ[S] Ω[S⁄R] :=
    Finsupp.linearCombination S fun i : κ ↦ D R S (a i)
  let l₁ : (κ →₀ S) →ₗ[S] (κ →₀ Localization.AtPrime p) :=
    Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.AtPrime p))
  let l₂ : Ω[S⁄R] →ₗ[S] Ω[Localization.AtPrime p⁄R] := map R R S (Localization.AtPrime p)
  let eₚ : (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R] :=
    IsLocalizedModule.mapExtendScalars p.primeCompl l₁ l₂ (Localization.AtPrime p) e
  have : eₚ = b.repr.symm := by
    ext i
    trans IsLocalizedModule.map p.primeCompl l₁ l₂ e <| l₁ <| Finsupp.single i 1
    · simp [eₚ, -IsLocalizedModule.map_apply, l₁]
    · simp [l₂, e, hb]
  have heₚ : Function.Bijective eₚ := this ▸ b.repr.symm.bijective
  have : Finite κ := Module.Finite.finite_basis b
  obtain ⟨g, hg, h⟩ := Module.FinitePresentation.exists_notMem_bijective e p l₁ l₂ heₚ
  let l₁ₜ : (κ →₀ S) →ₗ[S] (κ →₀ Localization.Away g) :=
    Finsupp.mapRange.linearMap (Algebra.linearMap S _)
  let l₂ₜ : Ω[S⁄R] →ₗ[S] Ω[Localization.Away g⁄R] :=
    map R R S (Localization.Away g)
  rw [← IsLocalizedModule.map_bijective_iff_localizedModuleMap_bijective l₁ₜ l₂ₜ] at h
  let eₜ' : (κ →₀ Localization.Away g) →ₗ[Localization.Away g] Ω[Localization.Away g⁄R] :=
    IsLocalizedModule.mapExtendScalars (Submonoid.powers g) l₁ₜ l₂ₜ (Localization.Away g) e
  refine ⟨g, hg, .of_basis_kaehlerDifferential (.ofRepr (LinearEquiv.ofBijective eₜ' h).symm) ?_⟩
  rintro - ⟨i, rfl⟩
  exact ⟨algebraMap S _ (a i), by simp +zetaDelta [IsLocalizedModule.map_linearCombination]⟩

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

Goal state before:
pp: ⊢ StableUnderComposition fun {R S} [inst : CommRing R] [inst_1 : CommRing S] ↦
    (fun R S x x_1 f ↦ f.FormallyUnramified ∧ f.Smooth) R S inst inst_1

Tactic:
exact FormallyUnramified.stableUnderComposition.and Smooth.stableUnderComposition

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
σ✝ : 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 : ι
⊢ (aeval P.val) (X i) = (algebraMap D.T S) (D.presLeft.val i)

Tactic:
simp [RingHom.algebraMap_toAlgebra, presLeft, hom, T]

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

Goal state before:
pp: case refine_1.refine_2
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
i : D.rels
hinj : Function.Injective ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
q : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
hq : (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))) q = D.p i
⊢ (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
      ((eval (Presentation.relationOfHasCoeffs ↥(subalgebra R D))) q) =
    (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
      ((aeval p) (Presentation.relationOfHasCoeffs (↥(subalgebra R D)) i))

Tactic:
simp_rw [map_eval, Function.comp_def, Presentation.map_relationOfHasCoeffs,
        hq, D.hp, MvPolynomial.map_aeval, hp]

Goal state after:
case refine_1.refine_2
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
i : D.rels
hinj : Function.Injective ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
q : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
hq : (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))) q = D.p i
⊢ (aeval D.h) (D.P.relation i) =
    (eval₂Hom
        ((MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)).comp
          (algebraMap (↥(subalgebra R D)) (MvPolynomial D.vars ↥(subalgebra R D))))
        fun i ↦ D.h i)
      (Presentation.relationOfHasCoeffs (↥(subalgebra R D)) i)
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: 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
inst✝ : Smooth A B
P : Presentation A B (Fin (Presentation.ofFinitePresentationVars A B))
  (Fin (Presentation.ofFinitePresentationRels A B)) :=
  Presentation.ofFinitePresentation A B
f : P.Ring →ₐ[A] B := IsScalarTower.toAlgHom A P.Ring B
hkerf : RingHom.ker f = Ideal.span (Set.range P.relation)
σ : B →ₐ[A] MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A ⧸ RingHom.ker f ^ 2
hsig : f.kerSquareLift.comp σ = AlgHom.id A B
h : Fin (Presentation.ofFinitePresentationVars A B) → MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A
hh :
  ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)), (Ideal.Quotient.mk (RingHom.ker f ^ 2)) (h i) = σ (P.val i)
hdiag : (Ideal.Quotient.mkₐ A (RingHom.ker f ^ 2)).comp (aeval h) = σ.comp (aeval P.val)
this :
  ∀ (j : Fin (Presentation.ofFinitePresentationRels A B)),
    (Ideal.Quotient.mk (RingHom.ker f ^ 2)) ((aeval h) (P.relation j)) = 0
⊢ ∃ A₀ B₀ x x_1, A₀.FG ∧ Smooth (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)

Tactic:
Ideal.Quotient.eq_zero_iff_mem,

Goal state after:
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
inst✝ : Smooth A B
P : Presentation A B (Fin (Presentation.ofFinitePresentationVars A B))
  (Fin (Presentation.ofFinitePresentationRels A B)) :=
  Presentation.ofFinitePresentation A B
f : P.Ring →ₐ[A] B := IsScalarTower.toAlgHom A P.Ring B
hkerf : RingHom.ker f = Ideal.span (Set.range P.relation)
σ : B →ₐ[A] MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A ⧸ RingHom.ker f ^ 2
hsig : f.kerSquareLift.comp σ = AlgHom.id A B
h : Fin (Presentation.ofFinitePresentationVars A B) → MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A
hh :
  ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)), (Ideal.Quotient.mk (RingHom.ker f ^ 2)) (h i) = σ (P.val i)
hdiag : (Ideal.Quotient.mkₐ A (RingHom.ker f ^ 2)).comp (aeval h) = σ.comp (aeval P.val)
this : ∀ (j : Fin (Presentation.ofFinitePresentationRels A B)), (aeval h) (P.relation j) ∈ RingHom.ker f ^ 2
⊢ ∃ A₀ B₀ x x_1, A₀.FG ∧ Smooth (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)
Module: Mathlib.RingTheory.RingHom.LocallyStandardSmooth

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

Tactic:
by
  algebraize [f]
  obtain ⟨s, hs, h⟩ := Algebra.Smooth.exists_span_eq_top_isStandardSmooth R S
  refine ⟨s, hs, fun t ht ↦ ?_⟩
  dsimp only
  rw [← f.algebraMap_toAlgebra, ← IsScalarTower.algebraMap_eq, isStandardSmooth_algebraMap]
  exact h t ht

Goal state after:
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
⊢ IsField ↑Γ(X, ⊤)

Tactic:
by
  let F := (Scheme.ΓSpecIso _).inv ≫ f.appTop
  have : F.hom.IsIntegral := by
    apply RingHom.isIntegral_respectsIso.2 (e := (Scheme.ΓSpecIso _).symm.commRingCatIsoToRingEquiv)
    exact isIntegral_appTop_of_universallyClosed f
  algebraize [F.hom]
  exact isField_of_isIntegral_of_isField' (Field.toIsField K)

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -W'.negAddY P Q - W'.a₁ * W'.addX P Q - W'.a₃ * W'.addZ P Q = P y ^ 2 * Q z * Q y

Tactic:
negAddY_of_Z_eq_zero_left hP hPz,

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -(P y ^ 2 * Q z * W'.negY Q) - W'.a₁ * W'.addX P Q - W'.a₃ * W'.addZ P Q = P y ^ 2 * Q z * Q y
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₀
⊢ IsOpenImmersion
    (pullback.diagonal f ∣_
      Scheme.Hom.opensRange ((Scheme.Pullback.diagonalCover f 𝒰Y 𝒰X).f ⟨⟨i, j⟩.fst, (⟨i, j⟩.snd, ⟨i, j⟩.snd)⟩))

Tactic:
rw [arrow_mk_iso_iff (P := @IsOpenImmersion)
      (Scheme.Pullback.diagonalRestrictIsoDiagonal f 𝒰Y 𝒰X 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 ((𝒰X i).f j ≫ pullback.snd f (𝒰Y.f i)))
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).negY (⇑↑f ∘ P) = ↑f ((W'⁄A).negY P)

Tactic:
← map_negY,

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).negY (⇑↑f ∘ P) = ((W'⁄A).map ↑f).negY (⇑↑f ∘ P)
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : FaithfullyFlat R S
H : Function.Surjective ⇑(algebraMap S (S ⊗[R] T))
⊢ Function.Surjective ⇑(algebraMap R T)

Tactic:
have : LinearMap.lTensor S (Algebra.linearMap R T) =
      Algebra.linearMap S (S ⊗[R] T) ∘ₗ (AlgebraTensorModule.rid R S S).toLinearMap := by
    ext; simp
  apply (Module.FaithfullyFlat.lTensor_surjective_iff_surjective R S (Algebra.linearMap R T)).mp
  simpa [this] using! H

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

Goal state before:
pp: case refine_2
R S : CommRingCat
φ : R ⟶ S
h : (@Surjective ⊓ @Flat) (Spec.map φ)
T : CommRingCat
this : IsAffine (Spec T)
ψ : R ⟶ T
hfst : IsIso (pullback.fst (Spec.map φ) (Spec.map ψ))
⊢ ∀ {R S : CommRingCat} {f : R ⟶ S}, True

Tactic:
implies_true

Goal state after: