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

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Projective R
f : R →+* S
P : Fin 3 → R
⊢ (W'.map f).neg (⇑f ∘ P) = ⇑f ∘ W'.neg P

Tactic:
by
  simp only [neg, map_negY, comp_fin3]
  map_simp

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

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

Tactic:
introv R h

Goal state after:
R S : Type u_6
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
h : IsLocalization.Away r S
⊢ (algebraMap R S).Smooth
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:
rw [FormallyUnramified, toAlgebra_algebraMap]

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

Goal state before:
pp: 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
H : ∀ (i : I), FormallySmooth R (A i)
B : Type (max u_1 u_2 u_3)
x✝¹ : CommRing B
x✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
g : ((i : I) → A i) →ₐ[R] B ⧸ J
x : B
hx : x ∈ RingHom.ker (Ideal.Quotient.mk J)
⊢ x ^ 2 ∈ ⊥

Tactic:
rw [← hJ]

Goal state after:
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
H : ∀ (i : I), FormallySmooth R (A i)
B : Type (max u_1 u_2 u_3)
x✝¹ : CommRing B
x✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
g : ((i : I) → A i) →ₐ[R] B ⧸ J
x : B
hx : x ∈ RingHom.ker (Ideal.Quotient.mk J)
⊢ x ^ 2 ∈ J ^ 2
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
k : L
this✝ : Algebra.IsSeparable K ↥K⟮k⟯
this : FiniteDimensional K ↥K⟮k⟯
⊢ ∃! g, (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)

Tactic:
have := FormallyEtale.of_isSeparable_aux K (K⟮k⟯)

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
k : L
this✝¹ : Algebra.IsSeparable K ↥K⟮k⟯
this✝ : FiniteDimensional K ↥K⟮k⟯
this : FormallyEtale K ↥K⟮k⟯
⊢ ∃! g, (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case tmul
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 y : B
⊢ (LinearMap.liftBaseChange S (↑R (map R S A B)))
      ((derivationTensorProduct R S A B).liftKaehlerDifferential ((D S B).tensorProductTo (x ⊗ₜ[S] y))) =
    (D S B).tensorProductTo (x ⊗ₜ[S] y)

Tactic:
simp only [Derivation.tensorProductTo_tmul, LinearMap.map_smul,
        Derivation.liftKaehlerDifferential_comp_D, map_liftBaseChange_smul]

Goal state after:
case tmul
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 y : B
⊢ x • (LinearMap.liftBaseChange S (↑R (map R S A B))) ((derivationTensorProduct R S A B) y) = x • (D S B) 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
P : Type u_4
inst✝³ : AddCommGroup P
inst✝² : Module R P
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f : M →ₗ[R] N
m n : ℕ
hmn : m ≤ n
⊢ (↑R (reduceModIdeal (I ^ m) f) ∘ₗ transitionMap I M hmn) ∘ₗ eval I M n = ↑R (reduceModIdeal (I ^ m) f) ∘ₗ eval I M m

Tactic:
comp_assoc,

Goal state after:
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
P : Type u_4
inst✝³ : AddCommGroup P
inst✝² : Module R P
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f : M →ₗ[R] N
m n : ℕ
hmn : m ≤ n
⊢ ↑R (reduceModIdeal (I ^ m) f) ∘ₗ transitionMap I M hmn ∘ₗ eval I M n = ↑R (reduceModIdeal (I ^ m) f) ∘ₗ eval I M m
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
r : AdicCompletion I R
x : M ⧸ I ^ n • ⊤
⊢ ↑r n • x = (evalₐ I n) r • x

Tactic:
induction r using induction_on

Goal state after:
case h
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
x : M ⧸ I ^ n • ⊤
f✝ : AdicCauchySequence I R
⊢ ↑((mk I R) f✝) n • x = (evalₐ I n) ((mk I R) f✝) • x
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:
by
  rw [← piEquivOfFintype_comp_ofTensorProduct_eq I ι, ← LinearMap.comp_assoc]
  simp

Goal state after:
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
I : Ideal S
f : A →ₐ[R] S ⧸ I
inst✝ : FormallySmooth R A
m : ℕ
T : Type u_3 := S ⧸ I ^ (m + 1 + 1)
J : Ideal T := Ideal.map (Ideal.Quotient.mkₐ R (I ^ (m + 1 + 1))) (I ^ (m + 1))
q : A →ₐ[R] T ⧸ J := (↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R ⋯).symm).comp (liftAdicCompletionAux (m + 1))
⊢ Ideal.map (Ideal.Quotient.mkₐ R (I ^ (m + 1 + 1))) (I ^ ((m + 1) * (m + 1 + 1))) = ⊥

Tactic:
exact eq_bot_mono (Ideal.map_mono <| Ideal.pow_le_pow_right (by simp))
        (Ideal.map_quotient_self _)

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

Goal state before:
pp: n m : ℕ
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_1
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsStandardSmoothOfRelativeDimension n R S
inst✝ : IsStandardSmoothOfRelativeDimension m S T
w✝⁷ w✝⁶ : Type
w✝⁵ : Finite w✝⁶
w✝⁴ : Finite w✝⁷
P : SubmersivePresentation R S w✝⁷ w✝⁶
hP : P.dimension = n
w✝³ w✝² : Type
w✝¹ : Finite w✝²
w✝ : Finite w✝³
Q : SubmersivePresentation S T w✝³ w✝²
hQ : Q.dimension = m
⊢ (Q.comp P).dimension = Q.dimension + P.dimension

Tactic:
apply PreSubmersivePresentation.dimension_comp_eq_dimension_add_dimension

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 ι σ
x : ↥P.ker
hx : ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this✝ : ↑x ∈ Ideal.span (Set.range P.relation)
c : σ →₀ P.Ring
hc : (c.sum fun i a ↦ a * P.relation i) = ↑x
heq : ∀ (i : σ), ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map i)) (P.relation x)) = 0
heq2 : (∑ i ∈ c.support, (aeval P.val) (c i) • fun j ↦ (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0
i : σ
this : LinearIndependent S fun i j ↦ (aeval P.val) ((pderiv (P.map j)) (P.relation i))
⊢ (aeval P.val) (c i) = 0

Tactic:
linearIndependent_iff''

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 ι σ
x : ↥P.ker
hx : ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this✝ : ↑x ∈ Ideal.span (Set.range P.relation)
c : σ →₀ P.Ring
hc : (c.sum fun i a ↦ a * P.relation i) = ↑x
heq : ∀ (i : σ), ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map i)) (P.relation x)) = 0
heq2 : (∑ i ∈ c.support, (aeval P.val) (c i) • fun j ↦ (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0
i : σ
this :
  ∀ (s : Finset σ) (g : σ → S),
    (∀ i ∉ s, g i = 0) →
      (∑ i ∈ s, g i • fun j ↦ (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0 → ∀ (i : σ), g i = 0
⊢ (aeval P.val) (c i) = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
P Q : Fin 3 → F
u v : F
⊢ addU (u • P) (v • Q) = (u * v) ^ 2 * addU P Q

Tactic:
simp [field, addU]

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

Goal state before:
pp: x✝⁴ : Type u_6
x✝³ : Type u_5
x✝² : CommRing x✝⁴
x✝¹ : CommRing x✝³
x✝ : x✝⁴ →+* x✝³
⊢ x✝.Etale ↔ x✝.FormallyUnramified ∧ x✝.Smooth

Tactic:
rw [etale_iff_formallyUnramified_and_smooth]

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

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Bijective ⇑f
⊢ f.Etale

Tactic:
rw [etale_iff_formallyUnramified_and_smooth]

Goal state after:
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Bijective ⇑f
⊢ f.FormallyUnramified ∧ f.Smooth
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: case h₁
n : ℕ
⊢ RespectsIso (@IsStandardSmoothOfRelativeDimension n)

Tactic:
exact isStandardSmoothOfRelativeDimension_respectsIso

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

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

Tactic:
introv R h

Goal state after:
R S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
h : IsLocalization.Away r S
⊢ (algebraMap R S).IsStandardSmooth
Module: Mathlib.RingTheory.RingHom.StandardSmooth

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

Tactic:
introv R h

Goal state after:
R S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
h : IsLocalization.Away r S
⊢ IsStandardSmoothOfRelativeDimension 0 (algebraMap R S)
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
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
⊢ ⊤ ≤
    Submodule.comap (Submodule.subtype P.ker)
        (Submodule.map (Submodule.subtype P.ker) (Submodule.span P.Ring (Set.range v))) ⊔
      P.ker • ⊤

Tactic:
Submodule.comap_map_eq_of_injective P.ker.subtype_injective,

Goal state after:
case inr
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
⊢ ⊤ ≤ Submodule.span P.Ring (Set.range v) ⊔ P.ker • ⊤
Module: Mathlib.AlgebraicGeometry.Morphisms.Proper

Goal state before:
pp: this : @IsAffineHom ⊓ @IsSeparated = @IsAffineHom
⊢ @IsIntegralHom ⊓ @LocallyOfFiniteType = @IsAffineHom ⊓ (@UniversallyClosed ⊓ @LocallyOfFiniteType)

Tactic:
IsIntegralHom.eq_universallyClosed_inf_isAffineHom,

Goal state after:
this : @IsAffineHom ⊓ @IsSeparated = @IsAffineHom
⊢ @UniversallyClosed ⊓ @IsAffineHom ⊓ @LocallyOfFiniteType = @IsAffineHom ⊓ (@UniversallyClosed ⊓ @LocallyOfFiniteType)
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
n : ι
inst✝ : ExpChar k p
ha' : IsTranscendenceBasis k fun i ↦ a ↑i
⊢ ∃ i, (IsTranscendenceBasis k fun j ↦ a ↑j) ∧ IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)

Tactic:
set S := {F : MvPolynomial ι k | F ≠ 0 ∧ F.aeval a = 0}

Goal state after:
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
n : ι
inst✝ : ExpChar k p
ha' : IsTranscendenceBasis k fun i ↦ a ↑i
S : Set (MvPolynomial ι k) := {F | F ≠ 0 ∧ (aeval a) F = 0}
⊢ ∃ i, (IsTranscendenceBasis k fun j ↦ a ↑j) ∧ IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Projective R
f : R →+* S
P : Fin 3 → R
⊢ (W'.map f).dblZ (⇑f ∘ P) = f (W'.dblZ P)

Tactic:
simp only [dblZ, negY]

Goal state after:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Projective R
f : R →+* S
P : Fin 3 → R
⊢ (⇑f ∘ P) z * ((⇑f ∘ P) y - (-(⇑f ∘ P) y - (W'.map f).a₁ * (⇑f ∘ P) x - (W'.map f).a₃ * (⇑f ∘ P) z)) ^ 3 =
    f (P z * (P y - (-P y - W'.a₁ * P x - W'.a₃ * P z)) ^ 3)
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst✝¹ : IsClosedImmersion i
f : X ⟶ Y
inst✝ : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
this✝ : IsDominant i
x : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f (g₁ x) ∈ ↑U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : g₁ x ∈ ↑V
hVU : V ≤ f ⁻¹ᵁ U
this : g₁.base = g₂.base
W : Opens ↥Z
hW : W ∈ Z.affineOpens
hxW : x ∈ ↑W
hWV : W ≤ g₁ ⁻¹ᵁ V ⊓ g₂ ⁻¹ᵁ V
⊢ ∃ U, x ∈ U ∧ U.ι ≫ g₁ = U.ι ≫ g₂

Tactic:
refine ⟨W, hxW, ?_⟩

Goal state after:
X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst✝¹ : IsClosedImmersion i
f : X ⟶ Y
inst✝ : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
this✝ : IsDominant i
x : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f (g₁ x) ∈ ↑U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : g₁ x ∈ ↑V
hVU : V ≤ f ⁻¹ᵁ U
this : g₁.base = g₂.base
W : Opens ↥Z
hW : W ∈ Z.affineOpens
hxW : x ∈ ↑W
hWV : W ≤ g₁ ⁻¹ᵁ V ⊓ g₂ ⁻¹ᵁ V
⊢ Scheme.Opens.ι W ≫ g₁ = Scheme.Opens.ι W ≫ g₂
Module: Mathlib.RingTheory.RingHom.OpenImmersion

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

Tactic:
introv R h

Goal state after:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
h : IsLocalization.Away r S
⊢ (algebraMap R S).IsStandardOpenImmersion
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: 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)
this✝ : UniversallyOpen g
U : Z.Opens := { carrier := Set.range ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ ↑U := pullback.snd f U.ι
g' : Y ⟶ ↑U := IsOpenImmersion.lift U.ι g ⋯
this : Surjective g'
⊢ IsIso (pullback.fst f' g')

Tactic:
rw [isIso_iff_isOpenImmersion_and_surjective]

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)
this✝ : UniversallyOpen g
U : Z.Opens := { carrier := Set.range ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ ↑U := pullback.snd f U.ι
g' : Y ⟶ ↑U := IsOpenImmersion.lift U.ι g ⋯
this : Surjective g'
⊢ IsOpenImmersion (pullback.fst f' g') ∧ Surjective (pullback.fst f' g')
Module: Mathlib.AlgebraicGeometry.Morphisms.Descent

Goal state before:
pp: P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝³ : P'.IsStableUnderBaseChange
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
hP : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
inst✝ : MorphismProperty.DescendsAlong (@IsAffineHom) P'
hQ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQQ' : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q'
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : P' (Spec.map φ)
hf : P (pullback.fst (Spec.map φ) g)
⊢ IsAffineHom g

Tactic:
exact MorphismProperty.of_pullback_fst_of_descendsAlong h <|
      AlgebraicGeometry.HasAffineProperty.affineAnd_le_isAffineHom P inferInstance _ hf

Goal state after:
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
L : Type u_3
inst✝⁴ : CommRing L
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : FaithfulSMul S L
x : S
y : L
⊢ (∀ (z : S), y * (algebraMap S L) z ∈ Subalgebra.map (IsScalarTower.toAlgHom R S L) R[x]) ↔
    ∀ (z : S), y * (algebraMap S L) z ∈ R[(algebraMap S L) x]

Tactic:
· rw [AlgHom.map_adjoin, Set.image_singleton]; rfl

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

Goal state before:
pp: case mem
R : Type u_3
inst✝ : CommRing R
I : Ideal R
P x : R[X]
hx : x ∈ {x | ∃ r ∈ I, C r * X = x}
i : ℕ
⊢ x.coeff i ∈ I ^ i

Tactic:
obtain ⟨r, hrI, rfl⟩ := hx
    simp +contextual [coeff_X, apply_ite, hrI, @eq_comm _ 1]

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

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

Tactic:
by
  rw [RingHom.ofLocalizationSpanTarget_iff_finite]
  introv R hs H
  algebraize [f]
  refine ⟨fun P _ ↦ ?_⟩
  have (r : s) : Module.Finite P.ResidueField (P.Fiber (Localization.Away r.1)) := by
    have : Algebra.QuasiFinite R (Localization.Away r.1) := quasiFinite_algebraMap.mp (H r)
    infer_instance
  let φ (r : s) : P.Fiber S →ₐ[P.ResidueField] P.Fiber (Localization.Away r.1) :=
    Algebra.TensorProduct.map (.id _ _) (IsScalarTower.toAlgHom _ _ _)
  let f : P.Fiber S →ₐ[P.ResidueField] Π r : s, (P.Fiber (Localization.Away r.1)) :=
    AlgHom.pi φ
  have : IsNoetherian P.ResidueField (Π r : s, (P.Fiber (Localization.Away r.1))) :=
    isNoetherian_of_isNoetherianRing_of_finite ..
  suffices Function.Injective f from .of_injective f.toLinearMap this
  rw [injective_iff_map_eq_zero]
  intro a ha
  apply eq_zero_of_localization _ fun J hJ ↦ ?_
  let I := (PrimeSpectrum.primesOverOrderIsoFiber R S P).symm ⟨J, inferInstance⟩
  have : ¬ (s : Set S) ⊆ I.1 := fun h ↦
    Ideal.IsPrime.ne_top' (top_le_iff.mp (hs.symm.trans_le (Ideal.span_le.mpr h)))
  obtain ⟨r, hrs, hrI⟩ := Set.not_subset.mp this
  let ψ : P.Fiber (Localization.Away r) →ₐ[P.ResidueField] Localization.AtPrime J :=
    Algebra.TensorProduct.lift (Algebra.ofId _ _) ⟨IsLocalization.map (M := .powers r)
      (T := J.primeCompl) _ Algebra.TensorProduct.includeRight.toRingHom (by
      simpa [Submonoid.powers_le] using! hrI), by
      simp [IsScalarTower.algebraMap_apply R S (Localization.Away r),
        -Algebra.TensorProduct.algebraMap_apply,
        ← IsScalarTower.algebraMap_apply R _ (Localization.AtPrime J)]⟩ (fun _ _ ↦ .all _ _)
  have hψ : ψ.comp (φ ⟨r, hrs⟩) = IsScalarTower.toAlgHom _ _ _ := by ext; simp [φ, ψ]
  refine congr($hψ a).symm.trans
    (show ψ (f a ⟨r, hrs⟩) = 0 by simp only [ha, Pi.zero_apply, map_zero])

Goal state after:
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: case mp.inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).IsIntegralElem f
n : σ →₀ ℕ
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S},
    (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).IsIntegralElem f →
      ∀ (n : σ →₀ ℕ), Finite σ → IsIntegral R (coeff n f)
hσ : ¬Finite σ
⊢ IsIntegral R (coeff n f)

pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).IsIntegralElem f
n : σ →₀ ℕ
hσ : Finite σ
⊢ IsIntegral R (coeff n f)

Tactic:
· obtain ⟨g, hg⟩ := MvPolynomial.exists_rename_eq_of_vars_subset_range (τ := f.vars) f _
      Subtype.val_injective (by simp)
    by_cases hn : n ∈ Set.range (Finsupp.mapDomain ((↑) : f.vars → σ))
    · obtain ⟨n, rfl⟩ := hn
      simp_rw [← hg, coeff_rename_mapDomain _ Subtype.val_injective]
      exact this (f := g) (RingHom.IsIntegralElem.of_map
        (g := (rename ((↑) : f.vars → σ)).toRingHom) (rename_injective _ Subtype.val_injective)
        (.of_comp (f := (killCompl (f := ((↑) : f.vars → σ)) Subtype.val_injective).toRingHom) <| by
        simp only [AlgHom.toRingHom_eq_coe, algebraMap_def, RingHom.coe_coe, hg]
        convert!
          H.map
            ((rename Subtype.val).comp
                (killCompl (f := ((↑) : f.vars → σ)) Subtype.val_injective)).toRingHom
        · exact RingHom.ext (by simp [MvPolynomial.killCompl_map])
        · nth_rw 1 12 [← hg]; simp)) n (.of_fintype _)
    · rw [← hg, coeff_rename_eq_zero _ _ _ (by grind)]
      exact isIntegral_zero

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).IsIntegralElem f
n : σ →₀ ℕ
hσ : Finite σ
⊢ IsIntegral R (coeff n f)
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
x : R
hx : x ∈ Ideal.under R p
hx' : x ∉ Ideal.under R q
this✝ : IsLocalHom f.toRingHom
this : IsUnit ((algebraMap R (Localization.AtPrime p)) x)
⊢ IsUnit (IsLocalization.mk' (Localization.AtPrime p) ((algebraMap R S) x) 1)

Tactic:
by simpa [IsLocalization.mk'_one]

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

Goal state before:
pp: 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]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
f : R⟮X⟯
p q p' q' : R[X]
hq : q ∈ R[X]⁰
hq' : q' ∈ R[X]⁰
h : q' * p = q * p'
⊢ (if h : φ q ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ p) ⟨φ q, h⟩ } else 0) =
    if h : φ q' ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ p') ⟨φ q', h⟩ } else 0

Tactic:
simp only [Submonoid.mem_comap.mp (hφ hq), Submonoid.mem_comap.mp (hφ hq'),
        dif_pos, ofFractionRing.injEq, Localization.mk_eq_mk_iff]

Goal state after:
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]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
f : R⟮X⟯
p q p' q' : R[X]
hq : q ∈ R[X]⁰
hq' : q' ∈ R[X]⁰
h : q' * p = q * p'
⊢ (Localization.r S[X]⁰) (φ p, ⟨φ q, ⋯⟩) (φ p', ⟨φ q', ⋯⟩)