mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case inl
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✝ : Subsingleton S
P' : Presentation R S (Unit ⊕ α) (Unit ⊕ σ) :=
  let __Generators := ofSurjective (fun i ↦ 0) ⋯;
  { toGenerators := __Generators, relation := fun x ↦ 1, span_range_relation_eq_ker := ⋯ }
this : Subsingleton P'.toExtension.Cotangent
⊢ ∃ P' b, P'.val ∘ Sum.inr = P.val ∧ ∀ (r : Unit ⊕ σ), b r = Extension.Cotangent.mk ⟨P'.relation r, ⋯⟩

Tactic:
exact ⟨P', default, by subsingleton, by subsingleton⟩

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

Goal state before:
pp: case inl
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✝ : Subsingleton S
P' : Presentation R S (Unit ⊕ α) (Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)) :=
  let __Generators := ofSurjective (fun i ↦ 0) ⋯;
  { toGenerators := __Generators, relation := fun x ↦ 1, span_range_relation_eq_ker := ⋯ }
⊢ ∃ 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 : Subsingleton P'.toExtension.Cotangent := Module.subsingleton S _

Goal state after:
case inl
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✝ : Subsingleton S
P' : Presentation R S (Unit ⊕ α) (Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)) :=
  let __Generators := ofSurjective (fun i ↦ 0) ⋯;
  { toGenerators := __Generators, relation := fun x ↦ 1, span_range_relation_eq_ker := ⋯ }
this : Subsingleton 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.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case inl
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✝ : Subsingleton S
P' : Presentation R S (Unit ⊕ α) (Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)) :=
  let __Generators := ofSurjective (fun i ↦ 0) ⋯;
  { toGenerators := __Generators, relation := fun x ↦ 1, span_range_relation_eq_ker := ⋯ }
this : Subsingleton 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, ⋯⟩

Tactic:
exact ⟨P', default, by subsingleton, by subsingleton⟩

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case refine_3
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : σ i ≠ 0
H✝ : (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0
F₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H : F.totalDegree ≤ ((rename Subtype.val) (F₀.coeff (σ i))).totalDegree
this : (F₀.coeff (σ i)).totalDegree + σ i ≤ ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F).totalDegree
⊢ False

Tactic:
rw [totalDegree_renameEquiv] at this

Goal state after:
case refine_3
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : σ i ≠ 0
H✝ : (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0
F₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H : F.totalDegree ≤ ((rename Subtype.val) (F₀.coeff (σ i))).totalDegree
this : (F₀.coeff (σ i)).totalDegree + σ i ≤ F.totalDegree
⊢ False
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
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
this : ∀ (i : ι), ∀ σ ∈ F.support, p ∣ σ i
σ' : (ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ σ ∈ F.support, σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), ↑σ = p • σ' ↑σ
H : ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K), LinearIndependent k v → LinearIndependent k fun x ↦ v x ^ p
F' : ↥F.support →₀ k
hF' : (Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)) F' = 0
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (fun s ↦ σ' ↑s) F')
hF''0 : F'' ≠ 0
hF'' : (aeval a) F'' = 0
⊢ False

Tactic:
suffices hpm : p * F''.totalDegree ≤ F.totalDegree by
    have hF''0' : F''.totalDegree ≠ 0 := by
      contrapose hF''0
      rw [totalDegree_eq_zero_iff_eq_C.mp hF''0, aeval_C, map_eq_zero] at hF''
      rw [totalDegree_eq_zero_iff_eq_C.mp hF''0, hF'', map_zero]
    replace this := hpm.trans ((HF F'' hF''0 hF'').trans_eq (one_mul _).symm)
    exact hp.one_lt.not_ge ((mul_le_mul_iff_of_pos_right hF''0'.bot_lt).mp this)

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
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
this : ∀ (i : ι), ∀ σ ∈ F.support, p ∣ σ i
σ' : (ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ σ ∈ F.support, σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), ↑σ = p • σ' ↑σ
H : ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K), LinearIndependent k v → LinearIndependent k fun x ↦ v x ^ p
F' : ↥F.support →₀ k
hF' : (Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)) F' = 0
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (fun s ↦ σ' ↑s) F')
hF''0 : F'' ≠ 0
hF'' : (aeval a) F'' = 0
⊢ p * F''.totalDegree ≤ F.totalDegree
Module: Mathlib.AlgebraicGeometry.Morphisms.Descent

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
inst✝² : CompactSpace ↥X
inst✝¹ : IsZariskiLocalAtSource P
inst✝ : P.ContainsIdentities
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun i ↦ 𝒰.X i) ⟶ X := Sigma.desc fun i ↦ 𝒰.f i
⊢ ∃ Y p, Surjective p ∧ P p ∧ IsAffine Y

Tactic:
refine ⟨_, p, ⟨fun x ↦ ?_⟩, ?_, inferInstance⟩

Goal state after:
case refine_1
P : MorphismProperty Scheme
X : Scheme
inst✝² : CompactSpace ↥X
inst✝¹ : IsZariskiLocalAtSource P
inst✝ : P.ContainsIdentities
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun i ↦ 𝒰.X i) ⟶ X := Sigma.desc fun i ↦ 𝒰.f i
x : ↥X
⊢ ∃ a, p a = x

case refine_2
P : MorphismProperty Scheme
X : Scheme
inst✝² : CompactSpace ↥X
inst✝¹ : IsZariskiLocalAtSource P
inst✝ : P.ContainsIdentities
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun i ↦ 𝒰.X i) ⟶ X := Sigma.desc fun i ↦ 𝒰.f i
⊢ P p
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent

Goal state before:
pp: ⊢ CodescendsAlong (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) fun {R S} [CommRing R] [CommRing S] ↦
    FaithfullyFlat

Tactic:
by
  apply CodescendsAlong.mk _ injective_respectsIso
  introv h H
  rw [faithfullyFlat_algebraMap_iff] at h
  exact h.injective_of_tensorProduct H

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝³ : (isomorphisms C).DescendsAlong P
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : HasPullbacks C
inst✝ : HasEqualizers C
S T : C
f : T ⟶ S
hf : P f
⊢ (Over.pullback f).Faithful

Tactic:
refine ⟨fun {X} Y a b hab ↦ ?_⟩
  ext
  apply P.eq_of_isomorphisms_descendsAlong (Over.w a) (Over.w b) f hf
  convert! congr($(hab).left) <;> ext <;> simp

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H :
  ∀ (R S : CommRingCat) (φ : R ⟶ S),
    Function.Surjective ⇑(ConcreteCategory.hom φ) →
      RingHom.ker (CommRingCat.Hom.hom φ) ^ 2 = ⊥ →
        ∀ (g₁ g₂ : Spec R ⟶ X), Spec.map φ ≫ g₁ = Spec.map φ ≫ g₂ → g₁ ≫ f = g₂ ≫ f → g₁ = g₂
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
this✝ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
R : Type u
x✝¹ : CommRing R
x✝ : Algebra (↑Γ(Y, U)) R
I : Ideal R
hI : I ^ 2 = ⊥
g₁ g₂ : ↑Γ(X, V) →ₐ[↑Γ(Y, U)] R
hg₁g₂ : (Ideal.Quotient.mkₐ (↑Γ(Y, U)) I).comp g₁ = (Ideal.Quotient.mkₐ (↑Γ(Y, U)) I).comp g₂
hg₁ : Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom ↑g₁ = CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U))) R)
hg₂ : Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom ↑g₂ = CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U))) R)
this : CommRingCat.ofHom ↑g₁ = CommRingCat.ofHom ↑g₂
⊢ g₁ = g₂

Tactic:
exact AlgHom.ext fun x ↦ congr($this x)

Goal state after:
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: case mpr
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 y : S
left✝ : y ∈ R[x]
H : ∀ (z : S), y * z ∈ R[x]
⊢ ∃ y_1 ∈ conductor R x, (algebraMap S L) y_1 = (algebraMap S L) y

Tactic:
exact ⟨_, H, rfl⟩

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

Goal state before:
pp: case neg
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.denom * Polynomial.eval₂ f a y.denom) =
    Polynomial.eval₂ f a x.num * Polynomial.eval₂ f a y.num * Polynomial.eval₂ f a (x * y).denom

Tactic:
← Polynomial.eval₂_mul

Goal state after:
case neg
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.denom * y.denom) =
    Polynomial.eval₂ f a x.num * Polynomial.eval₂ f a y.num * Polynomial.eval₂ f a (x * y).denom
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case neg
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.denom * y.denom) =
    Polynomial.eval₂ f a x.num * Polynomial.eval₂ f a y.num * Polynomial.eval₂ f a (x * y).denom

Tactic:
← Polynomial.eval₂_mul

Goal state after:
case neg
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 * (x.denom * y.denom)) =
    Polynomial.eval₂ f a x.num * Polynomial.eval₂ f a y.num * Polynomial.eval₂ f a (x * y).denom
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case neg
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 * (x.denom * y.denom)) =
    Polynomial.eval₂ f a x.num * Polynomial.eval₂ f a y.num * Polynomial.eval₂ f a (x * y).denom

Tactic:
← Polynomial.eval₂_mul

Goal state after:
case neg
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 * (x.denom * y.denom)) =
    Polynomial.eval₂ f a (x.num * y.num) * Polynomial.eval₂ f a (x * y).denom
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case neg
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 * (x.denom * y.denom)) =
    Polynomial.eval₂ f a (x.num * y.num) * Polynomial.eval₂ f a (x * y).denom

Tactic:
← Polynomial.eval₂_mul

Goal state after:
case neg
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 * (x.denom * y.denom)) = Polynomial.eval₂ f a (x.num * y.num * (x * y).denom)
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case neg
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 * (x.denom * y.denom)) = Polynomial.eval₂ f a (x.num * y.num * (x * y).denom)

Tactic:
← Polynomial.eval₂_mul

Goal state after:
case neg
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 * (x.denom * y.denom)) = Polynomial.eval₂ f a (x.num * y.num * (x * y).denom)
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
f : L
h : Transcendental K f
⊢ ↑((algEquivOfTranscendental f h) X) = f

Tactic:
by
  simp [← algebraMap_X]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
⊢ (valuation K⟮X⟯ (idealX K)) RatFunc.X = exp (-1)

Tactic:
by
  rw [← RatFunc.algebraMap_X, valuation_of_algebraMap, intValuation_singleton
      _ (Polynomial.X_ne_zero) (idealX_span K)]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hpmon : IsIntegral R p.leadingCoeff
hp : p.Splits
hpr : ∀ (x : S), p.IsRoot x → IsIntegral R x
i : ℕ
m : Multiset S
hm : p = C p.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
x : S
hx : x ∈ m
⊢ p.IsRoot x

Tactic:
rw [IsRoot, hm, eval_mul, eval_multiset_prod, Multiset.prod_eq_zero, mul_zero]

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hpmon : IsIntegral R p.leadingCoeff
hp : p.Splits
hpr : ∀ (x : S), p.IsRoot x → IsIntegral R x
i : ℕ
m : Multiset S
hm : p = C p.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
x : S
hx : x ∈ m
⊢ 0 ∈ Multiset.map (eval x) (Multiset.map (fun x ↦ X - C x) m)
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
⊢ IsUnit (f.toRingHom ((algebraMap R (Localization.AtPrime p)) x))

Tactic:
suffices IsUnit (IsLocalization.mk' (M := q.primeCompl) (Localization.AtPrime q)
        (algebraMap _ _ x) 1) by simpa [IsLocalization.mk'_one] using! this
      simpa [IsLocalization.AtPrime.isUnit_mk'_iff]

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

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

Tactic:
intro f H n
    refine .of_map (g := (isEmptyAlgEquiv _ PEmpty).symm.toRingHom)
      (isEmptyAlgEquiv _ PEmpty).symm.injective
      (.of_comp (f := (isEmptyAlgEquiv _ PEmpty).toRingHom) ?_)
    convert! H
    · ext r m <;> simp [Subsingleton.elim m 0, C, X, monomial, coeff, map]
    · obtain rfl := Subsingleton.elim n 0
      have : constantCoeff = (isEmptyAlgEquiv S PEmpty).toRingHom := by aesop
      simpa [-EmbeddingLike.apply_eq_iff_eq, -isEmptyAlgEquiv_apply] using!
        congr((isEmptyAlgEquiv S PEmpty.{w + 1}).symm ($this f))

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
q : Ideal S
inst✝⁵ : q.IsPrime
inst✝⁴ : p.IsPrime
inst✝³ : q.LiesOver p
inst✝² : WeaklyQuasiFiniteAt R q
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
⊢ Module.Finite p.ResidueField q.ResidueField

Tactic:
by
  let r := q.map (Ideal.Quotient.mk ((q.under R).map (algebraMap R S)))
  have : r.LiesOver q :=
    ⟨.trans (by simp [← RingHom.ker_eq_comap_bot, Ideal.map_comap_le])
    (Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective _).symm⟩
  let := Localization.AtPrime.algebraOfLiesOver q r
  have : r.LiesOver p := .trans _ q _
  let := Localization.AtPrime.algebraOfLiesOver p r
  exact .of_injective (IsScalarTower.toAlgHom _ _ r.ResidueField).toLinearMap (RingHom.injective _)

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
inst✝ : P.IsPrime
I : Ideal R[X]
p : P.ResidueField[X]
hp : Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I = Ideal.span {p}
this✝¹ : Algebra (R ⧸ P)[X] P.ResidueField[X] := (mapRingHom (algebraMap (R ⧸ P) P.ResidueField)).toAlgebra
this✝ : IsLocalization (Submonoid.map C (R ⧸ P)⁰) P.ResidueField[X]
this : p ∈ Ideal.map (algebraMap (R ⧸ P)[X] P.ResidueField[X]) (Ideal.map (mapRingHom (algebraMap R (R ⧸ P))) I)
s : ↥(Submonoid.map C (R ⧸ P)⁰)
r : R[X]
hr' : r ∈ I
hr : (mapRingHom (algebraMap R (R ⧸ P))) r ∈ Ideal.map (mapRingHom (algebraMap R (R ⧸ P))) I
e : p * map (algebraMap (R ⧸ P) P.ResidueField) ↑s = map (algebraMap R P.ResidueField) r
⊢ ∃ p ∈ I, Ideal.span {map (algebraMap R P.ResidueField) p} = Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I

Tactic:
refine ⟨r, hr', le_antisymm ?_ ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
inst✝ : P.IsPrime
I : Ideal R[X]
p : P.ResidueField[X]
hp : Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I = Ideal.span {p}
this✝¹ : Algebra (R ⧸ P)[X] P.ResidueField[X] := (mapRingHom (algebraMap (R ⧸ P) P.ResidueField)).toAlgebra
this✝ : IsLocalization (Submonoid.map C (R ⧸ P)⁰) P.ResidueField[X]
this : p ∈ Ideal.map (algebraMap (R ⧸ P)[X] P.ResidueField[X]) (Ideal.map (mapRingHom (algebraMap R (R ⧸ P))) I)
s : ↥(Submonoid.map C (R ⧸ P)⁰)
r : R[X]
hr' : r ∈ I
hr : (mapRingHom (algebraMap R (R ⧸ P))) r ∈ Ideal.map (mapRingHom (algebraMap R (R ⧸ P))) I
e : p * map (algebraMap (R ⧸ P) P.ResidueField) ↑s = map (algebraMap R P.ResidueField) r
⊢ Ideal.span {map (algebraMap R P.ResidueField) r} ≤ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I

case refine_2
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
inst✝ : P.IsPrime
I : Ideal R[X]
p : P.ResidueField[X]
hp : Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I = Ideal.span {p}
this✝¹ : Algebra (R ⧸ P)[X] P.ResidueField[X] := (mapRingHom (algebraMap (R ⧸ P) P.ResidueField)).toAlgebra
this✝ : IsLocalization (Submonoid.map C (R ⧸ P)⁰) P.ResidueField[X]
this : p ∈ Ideal.map (algebraMap (R ⧸ P)[X] P.ResidueField[X]) (Ideal.map (mapRingHom (algebraMap R (R ⧸ P))) I)
s : ↥(Submonoid.map C (R ⧸ P)⁰)
r : R[X]
hr' : r ∈ I
hr : (mapRingHom (algebraMap R (R ⧸ P))) r ∈ Ideal.map (mapRingHom (algebraMap R (R ⧸ P))) I
e : p * map (algebraMap (R ⧸ P) P.ResidueField) ↑s = map (algebraMap R P.ResidueField) r
⊢ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I ≤ Ideal.span {map (algebraMap R P.ResidueField) r}
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: case refine_2
X : Scheme
U : X.AffineZariskiSite
P : Presieve U
x✝¹ : X.AffineZariskiSite
f : ↑Γ(X, U.toOpens)
hV : IsAffineOpen (X.basicOpen f)
x✝ : ⟨X.basicOpen f, hV⟩ ⟶ U
H : P { down := { down := ⋯ } }
⊢ U.presieveOfSections (sectionsOfPresieve P) { down := { down := ⋯ } }

Tactic:
exact ⟨_, H, rfl⟩

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✝ : RingHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
⊢ (↑(map φ hφ)).toFun 0 = 0

Tactic:
MonoidHom.toFun_eq_coe,

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✝ : RingHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
⊢ (map φ hφ) 0 = 0
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]
φ : R[X] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
x y : R⟮X⟯
⊢ (↑(liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ)).toFun (x + y) =
    (↑(liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ)).toFun x +
      (↑(liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ)).toFun y

Tactic:
simp only [ZeroHom.toFun_eq_coe, MonoidWithZeroHom.toZeroHom_coe]

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]
φ : R[X] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
x y : R⟮X⟯
⊢ (liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ) (x + y) =
    (liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ) x + (liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ) y