mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: case neg.refine_1
F : Type u
inst✝¹ : Field F
W : Projective F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ⇑f ∘ P ≈ ⇑f ∘ Q
hz : ¬f (P z) = 0
⊢ P x * Q z = Q x * P z

pp: case neg.refine_2
F : Type u
inst✝¹ : Field F
W : Projective F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ⇑f ∘ P ≈ ⇑f ∘ Q
hz : ¬f (P z) = 0
⊢ P y * Q z = Q y * P z

Tactic:
all_goals apply f.injective; map_simp

Goal state after:
case neg.refine_1
F : Type u
inst✝¹ : Field F
W : Projective F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ⇑f ∘ P ≈ ⇑f ∘ Q
hz : ¬f (P z) = 0
⊢ f (P x) * f (Q z) = f (Q x) * f (P z)

case neg.refine_2
F : Type u
inst✝¹ : Field F
W : Projective F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ⇑f ∘ P ≈ ⇑f ∘ Q
hz : ¬f (P z) = 0
⊢ f (P y) * f (Q z) = f (Q y) * f (P z)
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: ⊢ zariskiTopology.Subcanonical

Tactic:
apply GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj
  intro X
  rw [Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange]
  rintro Y S hS x hx
  obtain ⟨(𝓤 : OpenCover Y), rfl⟩ := exists_cover_of_mem_pretopology hS
  let e : Y ⟶ X := 𝓤.glueMorphisms (fun j => x (𝓤.f _) (.mk _)) <| by
    intro i j
    apply hx
    exact Limits.pullback.condition
  refine ⟨e, ?_, ?_⟩
  · rintro Z e ⟨j⟩
    dsimp [e]
    rw [𝓤.ι_glueMorphisms]
  · intro e' h
    apply 𝓤.hom_ext
    intro j
    rw [𝓤.ι_glueMorphisms]
    exact h (𝓤.f j) (.mk j)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (algebraMap R S).FormallyUnramified ↔ Algebra.FormallyUnramified R S

Tactic:
FormallyUnramified,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Algebra.FormallyUnramified R S ↔ Algebra.FormallyUnramified R S
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
⊢ f.FormallyUnramified

Tactic:
FormallyUnramified,

Goal state after:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
⊢ Algebra.FormallyUnramified R S
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
⊢ f.FormallyUnramified

Tactic:
FormallyUnramified,

Goal state after:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
⊢ Algebra.FormallyUnramified R S
Module: Mathlib.RingTheory.Smooth.Locus

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Smooth R A
⊢ smoothLocus R A = Set.univ

Tactic:
by
  rw [smoothLocus_eq_univ_iff]
  infer_instance

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
x : PrimeSpectrum A
hx : x ∈ smoothLocus R A
f : A
hxf : x ∈ ↑(basicOpen f)
hf : Module.Projective (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])
Af : Type u_2 := Localization.Away f
this✝³ : FinitePresentation A (Localization.Away f)
this✝² : FinitePresentation R (Localization.Away f)
this✝¹ : LocalizedModule (Submonoid.powers f) Ω[A⁄R] ≃ₗ[A] Ω[Localization.Away f⁄R]
this✝ : LocalizedModule (Submonoid.powers f) Ω[A⁄R] ≃ₗ[Localization.Away f] Ω[Localization.Away f⁄R]
this : Module.Projective (Localization.Away f) Ω[Localization.Away f⁄R]
⊢ IsOpen ((zeroLocus ↑(Module.annihilator Af (H1Cotangent R Af)))ᶜ ∩ Module.freeLocus Af Ω[Af⁄R])

Tactic:
exact (isClosed_zeroLocus _).isOpen_compl.inter Module.isOpen_freeLocus

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

Goal state before:
pp: case intro.mp
R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : Finite I
val✝ : Fintype I
⊢ FormallySmooth R ((i : I) → A i) → ∀ (i : I), FormallySmooth R (A i)

Tactic:
exact fun _ ↦ of_pi A

Goal state after:
Module: Mathlib.RingTheory.Unramified.Pi

Goal state before:
pp: case intro.mpr
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)
⊢ FormallyUnramified R ((i : I) → f i)

Tactic:
iff_comp_injective

Goal state after:
case intro.mpr
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_1 : Algebra R B] (I_1 : Ideal B),
    I_1 ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I_1).comp
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
⊢ W'.negY (u • P) = u * W'.negY P

Tactic:
simp only [negY, smul_fin3_ext]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
⊢ -(u * P y) - W'.a₁ * (u * P x) - W'.a₃ * (u * P z) = u * (-P y - W'.a₁ * P x - W'.a₃ * P z)
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)
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
Sp : Type (max u_1 u_2) := 𝓀[R] ⊗[R] S
Pp : Type (max u_1 u_3) := 𝓀[R] ⊗[R] P
φ : Pp →ₐ[𝓀[R]] Sp := TensorProduct.map (AlgHom.id 𝓀[R] 𝓀[R]) (IsScalarTower.toAlgHom R P S)
⊢ FormallySmooth R S

Tactic:
let ψ : Sp →ₐ[R] 𝓀[S] := Algebra.TensorProduct.lift (IsScalarTower.toAlgHom _ _ _)
    (IsScalarTower.toAlgHom _ _ _) fun _ _ ↦ .all _ _

Goal state after:
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)
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
Sp : Type (max u_1 u_2) := 𝓀[R] ⊗[R] S
Pp : Type (max u_1 u_3) := 𝓀[R] ⊗[R] P
φ : Pp →ₐ[𝓀[R]] Sp := TensorProduct.map (AlgHom.id 𝓀[R] 𝓀[R]) (IsScalarTower.toAlgHom R P S)
ψ : Sp →ₐ[R] 𝓀[S] := TensorProduct.lift (IsScalarTower.toAlgHom R 𝓀[R] 𝓀[S]) (IsScalarTower.toAlgHom R S 𝓀[S]) ⋯
⊢ FormallySmooth R S
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case add
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)
x✝ : B ⊗[A] Ω[A⁄R]
x y : A ⊗[R] S
a✝¹ : e₂ ((Algebra.IsPushout.equiv R A S B) x • x✝) = (Algebra.IsPushout.equiv R A S B) x • e₂ x✝
a✝ : e₂ ((Algebra.IsPushout.equiv R A S B) y • x✝) = (Algebra.IsPushout.equiv R A S B) y • e₂ x✝
⊢ e₂ ((Algebra.IsPushout.equiv R A S B) (x + y) • x✝) = (Algebra.IsPushout.equiv R A S B) (x + y) • e₂ x✝

Tactic:
simp only [add_smul, map_add, *]

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
I : Ideal R
M : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
k : ℕ
hk : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)
⊢ Function.Injective ⇑(map I f)

Tactic:
← LinearMap.ker_eq_bot,

Goal state after:
R : Type u
inst✝⁶ : CommRing R
I : Ideal R
M : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
k : ℕ
hk : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)
⊢ (map I f).ker = ⊥
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: case add
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 : N
n : ℕ
y1 : N
hy1 : y1 ∈ I ^ n • ⊤
y2 : N
hy2 : y2 ∈ I ^ n • ⊤
ih1 : ∃ x ∈ I ^ n • ⊤, f x ≡ y1 [SMOD I ^ (n + 1) • ⊤]
ih2 : ∃ x ∈ I ^ n • ⊤, f x ≡ y2 [SMOD I ^ (n + 1) • ⊤]
⊢ ∃ x ∈ I ^ n • ⊤, f x ≡ y1 + y2 [SMOD I ^ (n + 1) • ⊤]

Tactic:
obtain ⟨x1, hx1, hx1'⟩ := ih1

Goal state after:
case add
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 : N
n : ℕ
y1 : N
hy1 : y1 ∈ I ^ n • ⊤
y2 : N
hy2 : y2 ∈ I ^ n • ⊤
ih2 : ∃ x ∈ I ^ n • ⊤, f x ≡ y2 [SMOD I ^ (n + 1) • ⊤]
x1 : M
hx1 : x1 ∈ I ^ n • ⊤
hx1' : f x1 ≡ y1 [SMOD I ^ (n + 1) • ⊤]
⊢ ∃ x ∈ I ^ n • ⊤, f x ≡ y1 + y2 [SMOD I ^ (n + 1) • ⊤]
Module: Mathlib.RingTheory.AdicCompletion.Exactness

Goal state before:
pp: R : Type u
inst✝⁸ : CommRing R
I : Ideal R
M : Type u
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
k : ℕ
hkn : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)
x : AdicCauchySequence I N
hker : ∀ (n : ℕ), g (↑x n) ∈ I ^ n • ⊤
n : ℕ
d : N
hdmem : d ∈ I ^ (k + n + 1) • ⊤
y yₙ : M
hd : f y = ↑x (k + n + 1) - d
hyₙ : f yₙ - ↑x (k + n) ∈ I ^ (k + n) • ⊤
h : f (y - yₙ) ∈ I ^ (k + n) • ⊤
hincl : I ^ (k + n - k) • (I ^ k • ⊤ ⊓ f.range) ≤ I ^ (k + n - k) • f.range
⊢ y - yₙ ∈ I ^ n • ⊤

Tactic:
convert_to y - yₙ ∈ (I ^ (k + n - k) • ⊤ : Submodule R M)
    · simp
    · rw [← Submodule.comap_map_eq_of_injective hf (I ^ (k + n - k) • ⊤ : Submodule R M),
        Submodule.map_smul'', Submodule.map_top]
      apply hincl
      rw [← hkn (k + n) (by lia)]
      exact ⟨h, ⟨y - yₙ, rfl⟩⟩

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

Goal state before:
pp: R : Type u
inst✝⁸ : CommRing R
I : Ideal R
M : Type u
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
k : ℕ
hkn : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)
x : AdicCauchySequence I N
hker : ∀ (n : ℕ), g (↑x n) ∈ I ^ n • ⊤
x✝ : ℕ
d : N := ⋯.choose
y : M := ⋯.choose
hdy : f y = ↑x (k + 0) - d
hdmem : ⋯.choose ∈ I ^ (k + 0) • ⊤
⊢ y ∈ {a | f a - ↑x (k + Nat.zero) ∈ I ^ (k + Nat.zero) • ⊤}

Tactic:
simpa [hdy]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Exact

Goal state before:
pp: case hg
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
q : Submodule R M
E : Type u_8
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i : E →ₗ[R] M
hi : Function.Injective ⇑i
h : IsCompl i.range q
hker : Disjoint g.ker q
hmap : Submodule.map g q = ⊤
⊢ Function.Bijective ⇑(i.range.projectionOnto q h ∘ₗ f)

Tactic:
exact Submodule.projectionOnto_comp_bijective_of_exact hfg hf h hker hmap

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 ι σ
⊢ Function.Injective ⇑P.cotangentComplexAux

Tactic:
← LinearMap.ker_eq_bot,

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 ι σ
⊢ P.cotangentComplexAux.ker = ⊥
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -W'.negDblY P - W'.a₁ * W'.dblX P - W'.a₃ * W'.dblZ P = P y ^ 4

Tactic:
negDblY_of_Z_eq_zero hP hPz,

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ - -P y ^ 4 - W'.a₁ * W'.dblX P - W'.a₃ * W'.dblZ P = P y ^ 4
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: 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 ι
⊢ ((localizationAway T g).comp P).ker ^ 2 ≤ RingHom.ker (compLocalizationAwayAlgHom T g P)

Tactic:
have hsple {x} (hx : x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1}) :
        (compLocalizationAwayAlgHom T g P) x = 0 := by
    obtain ⟨a, rfl⟩ := Ideal.mem_span_singleton.mp hx
    rw [map_mul, compLocalizationAwayAlgHom_relation_eq_zero, zero_mul]

Goal state after:
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
⊢ ((localizationAway T g).comp P).ker ^ 2 ≤ RingHom.ker (compLocalizationAwayAlgHom T g P)
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
i : D.rels
⊢ (aeval p) (Presentation.relationOfHasCoeffs (↥(subalgebra R D)) i) ∈
    RingHom.ker
        ↑(Ideal.Quotient.mkₐ (↥(subalgebra R D))
            (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))) ^
      2

Tactic:
Ideal.Quotient.mkₐ_ker

Goal state after:
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
i : D.rels
⊢ (aeval p) (Presentation.relationOfHasCoeffs (↥(subalgebra R D)) i) ∈
    Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))) ^ 2
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
⊢ P.ker • P.ker ≤ (Submodule.subtype P.ker).range

Tactic:
simp [Ideal.mul_le_right]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this✝¹ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := ⋯
p : Ideal ↑Γ(Y, U) := ⋯
q : Ideal ↑Γ(X, V) := ⋯
this✝ : q.LiesOver p
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := ⋯
⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth ↔
    Algebra.FormallySmooth (Localization.AtPrime p) (Localization.AtPrime q)

Tactic:
← formallySmooth_algebraMap

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this✝¹ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
p : Ideal ↑Γ(Y, U) := (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal
q : Ideal ↑Γ(X, V) := (hV.primeIdealOf ⟨x, hx⟩).asIdeal
this✝ : q.LiesOver p
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth ↔
    (algebraMap (Localization.AtPrime p) (Localization.AtPrime q)).FormallySmooth
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
⊢ addU (⇑f ∘ P) (⇑f ∘ Q) = f (addU P Q)

Tactic:
simp only [addU]

Goal state after:
F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
⊢ -((⇑f ∘ P) y * (⇑f ∘ Q) z - (⇑f ∘ Q) y * (⇑f ∘ P) z) ^ 3 / ((⇑f ∘ P) z * (⇑f ∘ Q) z) =
    f (-(P y * Q z - Q y * P z) ^ 3 / (P z * Q z))
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent

Goal state before:
pp: ⊢ ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T],
    (algebraMap R S).FaithfullyFlat →
      Function.Injective ⇑(algebraMap S (S ⊗[R] T)) → Function.Injective ⇑(algebraMap R T)

Tactic:
introv h H

Goal state after:
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : (algebraMap R S).FaithfullyFlat
H : Function.Injective ⇑(algebraMap S (S ⊗[R] T))
⊢ Function.Injective ⇑(algebraMap R T)
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent

Goal state before:
pp: ⊢ ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T],
    (algebraMap R S).FaithfullyFlat →
      Function.Surjective ⇑(algebraMap S (S ⊗[R] T)) → Function.Surjective ⇑(algebraMap R T)

Tactic:
introv h H

Goal state after:
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : (algebraMap R S).FaithfullyFlat
H : Function.Surjective ⇑(algebraMap S (S ⊗[R] T))
⊢ Function.Surjective ⇑(algebraMap R T)
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : MorphismProperty C
inst✝ : P.RespectsIso
H : ∀ {X Y Z : C} {f : Z ⟶ X} {g : Z ⟶ Y} [inst : HasPushout f g], Q f → P (pushout.inl f g) → P g
A X Y Z : C
f : A ⟶ X
g : A ⟶ Y
inl : X ⟶ Z
inr : Y ⟶ Z
h : IsPushout f g inl inr
hf : Q f
hfst : P inl
this : HasPushout f g
⊢ P (pushout.inl f g)

Tactic:
← P.cancel_right_of_respectsIso _ h.isoPushout.inv,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : MorphismProperty C
inst✝ : P.RespectsIso
H : ∀ {X Y Z : C} {f : Z ⟶ X} {g : Z ⟶ Y} [inst : HasPushout f g], Q f → P (pushout.inl f g) → P g
A X Y Z : C
f : A ⟶ X
g : A ⟶ Y
inl : X ⟶ Z
inr : Y ⟶ Z
h : IsPushout f g inl inr
hf : Q f
hfst : P inl
this : HasPushout f g
⊢ P (pushout.inl f g ≫ h.isoPushout.inv)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: ⊢ ∀ {X Y Z : Scheme} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g],
    (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f → IsOpenImmersion (pullback.fst f g) → IsOpenImmersion g

Tactic:
intro X Y Z f g _ hf hg

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (pullback.fst f g)
⊢ IsOpenImmersion g
Module: Mathlib.RingTheory.RingHom.QuasiFinite

Goal state before:
pp: ⊢ HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ QuasiFinite

Tactic:
introv R _
  exact quasiFinite_algebraMap.mpr (.of_isLocalization (.powers r))

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal

Goal state before:
pp: case inr.refine_3
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
hq : q.natDegree = p.natDegree
⊢ ∀ (i : ℕ), q.coeff i ∈ I ^ (p.natDegree - i)

Tactic:
simp [q, apply_ite, coeff_mem_pow_of_mem_adjoin_C_mul_X (p.coeff _).2]

Goal state after: