mathlib-initiative/mathlib-tactics huggingface dataset:
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
a : κ → ι
b : σ → ι
hg : Function.Surjective ⇑g
v : Basis ι R M
hainj : Function.Injective a
hsa : ∀ (i : κ), s (v (a i)) = 0
hlib : LinearIndependent R (⇑s ∘ ⇑v ∘ b)
hab : Codisjoint (Set.range a) (Set.range b)
k : κ
⊢ (ofSplitExact hs hfg hg v hainj hsa hlib hab) k = g (v (a k))

Tactic:
by
  simp [ofSplitExact]

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.Core

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Presentation R S ι σ
⊢ P.coeffs ⊆ Set.range ⇑(algebraMap P.Core R)

Tactic:
by
    refine subset_trans P.coeffs_subset_core ?_
    simp [Core, Subalgebra.algebraMap_eq]

Goal state after:
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
⊢ Ideal.map ((localizationAway T g).toComp P).toAlgHom P.ker *
      Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} ≤
    RingHom.ker (compLocalizationAwayAlgHom T g P)

Tactic:
Ideal.mul_le

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
⊢ ∀ r ∈ Ideal.map ((localizationAway T g).toComp P).toAlgHom P.ker,
    ∀ s ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1},
      r * s ∈ RingHom.ker (compLocalizationAwayAlgHom T g P)
Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree

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
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
this :
  ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
    [FinitePresentation R S] (p : Ideal S) [inst_4 : p.IsPrime] [IsSmoothAt R p],
    Smooth R S → ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)
h : ¬Smooth R S
⊢ ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)

Tactic:
obtain ⟨g, hg, hsm⟩ := IsSmoothAt.exists_notMem_smooth R p

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
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
this :
  ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
    [FinitePresentation R S] (p : Ideal S) [inst_4 : p.IsPrime] [IsSmoothAt R p],
    Smooth R S → ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)
h : ¬Smooth R S
g : S
hg : g ∉ p
hsm : Smooth R (Localization.Away g)
⊢ ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)
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
⊢ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} *
      Ideal.map ((localizationAway T g).toComp P).toAlgHom P.ker ≤
    RingHom.ker (compLocalizationAwayAlgHom T g P)

Tactic:
Ideal.mul_le

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
⊢ ∀ r ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1},
    ∀ s ∈ Ideal.map ((localizationAway T g).toComp P).toAlgHom P.ker,
      r * s ∈ 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
⊢ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} *
      Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} ≤
    RingHom.ker (compLocalizationAwayAlgHom T g P)

Tactic:
Ideal.mul_le

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
⊢ ∀ r ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1},
    ∀ s ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1},
      r * s ∈ 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✝
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
h✝ : Smooth R S
κ : Type u_2
a : κ → S
b : Module.Basis κ (Localization.AtPrime p) Ω[Localization.AtPrime p⁄R]
hb : ∀ (i : κ), b i = (⇑(map R R S (Localization.AtPrime p)) ∘ ⇑(D R S)) (a i)
e : (κ →₀ S) →ₗ[S] Ω[S⁄R] := Finsupp.linearCombination S fun i ↦ (D R S) (a i)
l₁ : (κ →₀ S) →ₗ[S] κ →₀ Localization.AtPrime p :=
  Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.AtPrime p))
l₂ : Ω[S⁄R] →ₗ[S] Ω[Localization.AtPrime p⁄R] := map R R S (Localization.AtPrime p)
eₚ : (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R] :=
  (IsLocalizedModule.mapExtendScalars p.primeCompl l₁ l₂ (Localization.AtPrime p)) e
this✝ : eₚ = ↑b.repr.symm
heₚ : Function.Bijective ⇑eₚ
this : Finite κ
g : S
hg : g ∉ p
l₁ₜ : (κ →₀ S) →ₗ[S] κ →₀ Localization.Away g := Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.Away g))
l₂ₜ : Ω[S⁄R] →ₗ[S] Ω[Localization.Away g⁄R] := map R R S (Localization.Away g)
h : Function.Bijective ⇑((IsLocalizedModule.map (Submonoid.powers g) l₁ₜ l₂ₜ) e)
⊢ ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)

Tactic:
let eₜ' : (κ →₀ Localization.Away g) →ₗ[Localization.Away g] Ω[Localization.Away g⁄R] :=
    IsLocalizedModule.mapExtendScalars (Submonoid.powers g) l₁ₜ l₂ₜ (Localization.Away g) e

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
inst✝⁸ : CommRing R✝
inst✝⁷ : CommRing S✝
inst✝⁶ : Algebra R✝ S✝
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
h✝ : Smooth R S
κ : Type u_2
a : κ → S
b : Module.Basis κ (Localization.AtPrime p) Ω[Localization.AtPrime p⁄R]
hb : ∀ (i : κ), b i = (⇑(map R R S (Localization.AtPrime p)) ∘ ⇑(D R S)) (a i)
e : (κ →₀ S) →ₗ[S] Ω[S⁄R] := Finsupp.linearCombination S fun i ↦ (D R S) (a i)
l₁ : (κ →₀ S) →ₗ[S] κ →₀ Localization.AtPrime p :=
  Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.AtPrime p))
l₂ : Ω[S⁄R] →ₗ[S] Ω[Localization.AtPrime p⁄R] := map R R S (Localization.AtPrime p)
eₚ : (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R] :=
  (IsLocalizedModule.mapExtendScalars p.primeCompl l₁ l₂ (Localization.AtPrime p)) e
this✝ : eₚ = ↑b.repr.symm
heₚ : Function.Bijective ⇑eₚ
this : Finite κ
g : S
hg : g ∉ p
l₁ₜ : (κ →₀ S) →ₗ[S] κ →₀ Localization.Away g := Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.Away g))
l₂ₜ : Ω[S⁄R] →ₗ[S] Ω[Localization.Away g⁄R] := map R R S (Localization.Away g)
h : Function.Bijective ⇑((IsLocalizedModule.map (Submonoid.powers g) l₁ₜ l₂ₜ) e)
eₜ' : (κ →₀ Localization.Away g) →ₗ[Localization.Away g] Ω[Localization.Away g⁄R] :=
  (IsLocalizedModule.mapExtendScalars (Submonoid.powers g) l₁ₜ l₂ₜ (Localization.Away g)) e
⊢ ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)
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
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ 0 ^ 3 = 0

Tactic:
zero_pow three_ne_zero

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ 0 = 0
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 α
inst✝ : Module.Free S P.toExtension.Cotangent
h✝ : Nontrivial S
⊢ ∃ P' b,
    P'.val ∘ Sum.inr = P.val ∧
      ∀ (r : Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)), b r = Extension.Cotangent.mk ⟨P'.relation r, ⋯⟩

Tactic:
have : Module.Finite S P.toExtension.Cotangent :=
    Algebra.Extension.Cotangent.finite P.fg_ker_of_finitePresentation

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 α
inst✝ : Module.Free S P.toExtension.Cotangent
h✝ : Nontrivial S
this : Module.Finite S P.toExtension.Cotangent
⊢ ∃ P' b,
    P'.val ∘ Sum.inr = P.val ∧
      ∀ (r : Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)), b r = Extension.Cotangent.mk ⟨P'.relation r, ⋯⟩
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: case inr
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : IsOpenImmersion (pullback.diagonal f)
this : ∀ {X : Scheme} (f : X ⟶ Spec R) [IsOpenImmersion (pullback.diagonal f)], (∃ S, X = Spec S) → FormallyUnramified f
hX : ¬∃ S, X = Spec S
i : X.affineCover.I₀
⊢ FormallyUnramified (X.affineCover.f i ≫ f)

Tactic:
have inst : IsOpenImmersion (pullback.diagonal (X.affineCover.f i ≫ f)) :=
      MorphismProperty.comp_mem (.diagonal @IsOpenImmersion) _ _
        (inferInstanceAs (IsOpenImmersion _)) ‹_›

Goal state after:
case inr
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : IsOpenImmersion (pullback.diagonal f)
this : ∀ {X : Scheme} (f : X ⟶ Spec R) [IsOpenImmersion (pullback.diagonal f)], (∃ S, X = Spec S) → FormallyUnramified f
hX : ¬∃ S, X = Spec S
i : X.affineCover.I₀
inst : IsOpenImmersion (pullback.diagonal (X.affineCover.f i ≫ f))
⊢ FormallyUnramified (X.affineCover.f i ≫ f)
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
this✝ : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FormallyUnramified
algInst✝¹ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algInst✝ : Algebra ↑Γ(Y, U) ↑Γ(Z, W) := (CommRingCat.Hom.hom (Scheme.Hom.appLE (g₁ ≫ f) U W ⋯)).toAlgebra
algebraizeInst✝ : Algebra.FormallyUnramified ↑Γ(Y, U) ↑Γ(X, V)
ψ₁ : ↑Γ(X, V) →ₐ[↑Γ(Y, U)] ↑Γ(Z, W) := { toRingHom := CommRingCat.Hom.hom (Scheme.Hom.appLE g₁ V W ⋯), commutes' := ⋯ }
ψ₂ : ↑Γ(X, V) →ₐ[↑Γ(Y, U)] ↑Γ(Z, W) := { toRingHom := CommRingCat.Hom.hom (Scheme.Hom.appLE g₂ V W ⋯), commutes' := ⋯ }
this : ψ₁ = ψ₂
⊢ Scheme.Opens.ι W ≫ g₁ = Scheme.Opens.ι W ≫ g₂

Tactic:
simpa [ψ₁, ψ₂, -Iso.cancel_iso_hom_left, IsAffineOpen.isoSpec_hom] using
      congr(hW.isoSpec.hom ≫ Spec.map (CommRingCat.ofHom ($this).toRingHom) ≫ hV.fromSpec)

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

Goal state before:
pp: R S T : Type u_1
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) g →
        (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) (g.comp f)

Tactic:
_

Goal state after:
R S T : Type u_1
inst✝ : CommRing R
⊢ ∀ [inst : CommRing S] [inst_1 : CommRing T] (f : R →+* S) (g : S →+* T),
    (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) g →
        (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) (g.comp f)
Module: Mathlib.RingTheory.RingHom.Injective

Goal state before:
pp: R S T : Type u_1
inst✝ : CommRing R
⊢ ∀ [inst : CommRing S] [inst_1 : CommRing T] (f : R →+* S) (g : S →+* T),
    (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) g →
        (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) (g.comp f)

Tactic:
_

Goal state after:
R S T : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ [inst : CommRing T] (f : R →+* S) (g : S →+* T),
    (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) g →
        (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) (g.comp f)
Module: Mathlib.RingTheory.RingHom.Injective

Goal state before:
pp: R S T : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ [inst : CommRing T] (f : R →+* S) (g : S →+* T),
    (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) g →
        (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) (g.comp f)

Tactic:
_

Goal state after:
R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
⊢ ∀ (f : R →+* S) (g : S →+* T),
    (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) g →
        (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) (g.comp f)
Module: Mathlib.RingTheory.RingHom.Injective

Goal state before:
pp: R S : Type u_1
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), Function.Injective ⇑e.toRingHom

Tactic:
_

Goal state after:
R S : Type u_1
inst✝ : CommRing R
⊢ ∀ [inst : CommRing S] (e : R ≃+* S), Function.Injective ⇑e.toRingHom
Module: Mathlib.RingTheory.RingHom.Injective

Goal state before:
pp: R S : Type u_1
inst✝ : CommRing R
⊢ ∀ [inst : CommRing S] (e : R ≃+* S), Function.Injective ⇑e.toRingHom

Tactic:
_

Goal state after:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (e : R ≃+* S), Function.Injective ⇑e.toRingHom
Module: Mathlib.AlgebraicGeometry.Morphisms.Descent

Goal state before:
pp: P P' : MorphismProperty Scheme
inst✝³ : P'.IsStableUnderBaseChange
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
inst✝ : IsZariskiLocalAtTarget P
H :
  ∀ {R S : CommRingCat} {Y : Scheme} (φ : R ⟶ S) (g : Y ⟶ Spec R),
    P' (Spec.map φ) → P (pullback.fst (Spec.map φ) g) → P g
R : CommRingCat
⊢ ∀ {X Y : Scheme} (f : X ⟶ Spec R) (g : Y ⟶ Spec R), (P' ⊓ @QuasiCompact) f → P (pullback.fst f g) → P g

Tactic:
X

Goal state after:
P P' : MorphismProperty Scheme
inst✝³ : P'.IsStableUnderBaseChange
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
inst✝ : IsZariskiLocalAtTarget P
H :
  ∀ {R S : CommRingCat} {Y : Scheme} (φ : R ⟶ S) (g : Y ⟶ Spec R),
    P' (Spec.map φ) → P (pullback.fst (Spec.map φ) g) → P g
R : CommRingCat
X : Scheme
⊢ ∀ {Y : Scheme} (f : X ⟶ Spec R) (g : Y ⟶ Spec R), (P' ⊓ @QuasiCompact) f → P (pullback.fst f g) → P g
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: case refine_1
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✝ : CommRingCat
⊢ ∀ {S : CommRingCat} {f : R✝ ⟶ S}, (@Surjective ⊓ @Flat) (Spec.map f) → (CommRingCat.Hom.hom f).FaithfullyFlat

Tactic:
_

Goal state after:
case refine_1
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✝}, (@Surjective ⊓ @Flat) (Spec.map f) → (CommRingCat.Hom.hom f).FaithfullyFlat
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:
_

Goal state after:
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
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'
this : IsOpenImmersion (pullback.fst f (g' ≫ U.ι))
⊢ IsOpenImmersion (pullback.fst f' g' ≫ pullback.fst f U.ι)

Tactic:
rw [← pullbackLeftPullbackSndIso_hom_fst]

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'
this : IsOpenImmersion (pullback.fst f (g' ≫ U.ι))
⊢ IsOpenImmersion ((pullbackLeftPullbackSndIso f U.ι g').hom ≫ pullback.fst f (g' ≫ U.ι))
Module: Mathlib.RingTheory.IntegralClosure.GoingDown

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : FaithfulSMul R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
⊢ ∀ [p.IsPrime] (Q : Ideal S) [Q.IsPrime], p < Ideal.under R Q → ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
_

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsDomain S
inst✝³ : FaithfulSMul R S
inst✝² : Algebra.IsIntegral R S
inst✝¹ : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
inst✝ : p.IsPrime
⊢ ∀ (Q : Ideal S) [Q.IsPrime], p < Ideal.under R Q → ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
Module: Mathlib.RingTheory.IntegralClosure.GoingDown

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsDomain S
inst✝³ : FaithfulSMul R S
inst✝² : Algebra.IsIntegral R S
inst✝¹ : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
inst✝ : p.IsPrime
Q : Ideal S
⊢ ∀ [Q.IsPrime], p < Ideal.under R Q → ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
_

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
inst✝⁴ : FaithfulSMul R S
inst✝³ : Algebra.IsIntegral R S
inst✝² : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
inst✝¹ : p.IsPrime
Q : Ideal S
inst✝ : Q.IsPrime
⊢ p < Ideal.under R Q → ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
H : IsIntegral R s
h : ∃ t ∈ R⁰, t • s ∈ (algebraMap R S).range
b : R
hb' : b ∈ R⁰
hb : ∀ i < (minpoly R s).natDegree, b • s ^ i ∈ (algebraMap R S).range
n : ℕ
IH : ∀ m < n, b • s ^ m ∈ (algebraMap R S).range
⊢ b • s ^ n ∈ (algebraMap R S).range

Tactic:
obtain hn | hn := lt_or_ge n (minpoly R s).natDegree

Goal state after:
case h.inl
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
H : IsIntegral R s
h : ∃ t ∈ R⁰, t • s ∈ (algebraMap R S).range
b : R
hb' : b ∈ R⁰
hb : ∀ i < (minpoly R s).natDegree, b • s ^ i ∈ (algebraMap R S).range
n : ℕ
IH : ∀ m < n, b • s ^ m ∈ (algebraMap R S).range
hn : n < (minpoly R s).natDegree
⊢ b • s ^ n ∈ (algebraMap R S).range

case h.inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
H : IsIntegral R s
h : ∃ t ∈ R⁰, t • s ∈ (algebraMap R S).range
b : R
hb' : b ∈ R⁰
hb : ∀ i < (minpoly R s).natDegree, b • s ^ i ∈ (algebraMap R S).range
n : ℕ
IH : ∀ m < n, b • s ^ m ∈ (algebraMap R S).range
hn : (minpoly R s).natDegree ≤ n
⊢ b • s ^ n ∈ (algebraMap R S).range
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case pos
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
hxy : Polynomial.eval₂ f a (x + y).denom = 0
⊢ Polynomial.eval₂ f a (x + y).num / Polynomial.eval₂ f a (x + y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom +
      Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom

Tactic:
have := Polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero f a (denom_add_dvd x y) hxy

Goal state after:
case pos
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
hxy : Polynomial.eval₂ f a (x + y).denom = 0
this : Polynomial.eval₂ f a (x.denom * y.denom) = 0
⊢ Polynomial.eval₂ f a (x + y).num / Polynomial.eval₂ f a (x + y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom +
      Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom