mathlib-initiative/mathlib-tactics huggingface dataset:
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
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
r : σ
⊢ Extension.Cotangent.mk
      ⟨((localizationAway S D.gbar).toComp D.presLeft.toGenerators).toExtensionHom.toAlgHom ↑(D.kerGen r), ⋯⟩ =
    Extension.Cotangent.mk ⟨D.pres.relation (Sum.inr r), ⋯⟩

Tactic:
simp only [Extension.Hom.toAlgHom_apply, Hom.toExtensionHom_toRingHom, AlgHom.toRingHom_eq_coe]

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
r : σ
⊢ Extension.Cotangent.mk ⟨↑((localizationAway S D.gbar).toComp D.presLeft.toGenerators).toAlgHom ↑(D.kerGen r), ⋯⟩ =
    Extension.Cotangent.mk ⟨D.pres.relation (Sum.inr r), ⋯⟩
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
⊢ (aeval a) F'' = 0

Tactic:
have : (aeval a).toLinearMap ∘ₗ (AddMonoidAlgebra.coeffLinearEquiv _).symm.toLinearMap ∘ₗ
      Finsupp.lmapDomain k k (fun s : F.support ↦ σ' s) =
        (Finsupp.linearCombination k fun s : F.support ↦ aeval a (monomial (σ' s) (1 : k))) := by
      ext v; simp [monomial]

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
this :
  ((aeval a).toLinearMap ∘ₗ ↑(AddMonoidAlgebra.coeffLinearEquiv k).symm ∘ₗ Finsupp.lmapDomain k k fun s ↦ σ' ↑s) =
    Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)
⊢ (aeval a) F'' = 0
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent

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

Tactic:
have : LinearMap.lTensor S (Algebra.linearMap R T) =
      Algebra.linearMap S (S ⊗[R] T) ∘ₗ (AlgebraTensorModule.rid R S S).toLinearMap := by
    ext; simp

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : FaithfullyFlat R S
H : Function.Injective ⇑(algebraMap S (S ⊗[R] T))
this :
  LinearMap.lTensor S (Algebra.linearMap R T) = ↑R (Algebra.linearMap S (S ⊗[R] T) ∘ₗ ↑(AlgebraTensorModule.rid R S S))
⊢ Function.Injective ⇑(algebraMap R T)
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent

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

Tactic:
have : LinearMap.lTensor S (Algebra.linearMap R T) =
      Algebra.linearMap S (S ⊗[R] T) ∘ₗ (AlgebraTensorModule.rid R S S).toLinearMap := by
    ext; simp

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : FaithfullyFlat R S
H : Function.Surjective ⇑(algebraMap S (S ⊗[R] T))
this :
  LinearMap.lTensor S (Algebra.linearMap R T) = ↑R (Algebra.linearMap S (S ⊗[R] T) ∘ₗ ↑(AlgebraTensorModule.rid R S S))
⊢ Function.Surjective ⇑(algebraMap R T)
Module: Mathlib.AlgebraicGeometry.Morphisms.Descent

Goal state before:
pp: case a
P P' : MorphismProperty Scheme
inst✝³ : P'.RespectsIso
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H : ∀ {R : CommRingCat} {S X : Scheme} (f : Spec R ⟶ S) (g : X ⟶ S), P' f → P (pullback.fst f g) → P g
X Y Z T : Scheme
inst✝ : IsAffine T
p : T ⟶ X
hp : P' p
f : X ⟶ Z
g : Y ⟶ Z
h : P' f
hf : P (pullback.fst f g)
⊢ P' ((T.isoSpec.inv ≫ p) ≫ f)

Tactic:
rw [Category.assoc, P'.cancel_left_of_respectsIso]
    exact P'.comp_mem _ _ hp h

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
x : S
I : Ideal R
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a ↦ a • (algebraMap R S) i) = z
⊢ ((algebraMap R S) p * l.sum fun i a ↦ a • (algebraMap R S) i) ∈
    ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)

Tactic:
mul_comm,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a ↦ a • (algebraMap R S) i) = z
⊢ (l.sum fun i a ↦ a • (algebraMap R S) i) * (algebraMap R S) p ∈
    ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)
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
x : S
I : Ideal R
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a ↦ a • (algebraMap R S) i) = z
a : R
ha : a ∈ I
⊢ l a * ((algebraMap R S) a * (algebraMap R S) p) ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)

Tactic:
mul_comm,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a ↦ a • (algebraMap R S) i) = z
a : R
ha : a ∈ I
⊢ (algebraMap R S) a * (algebraMap R S) p * l a ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsReduced S
x : S
hx : IsStronglyTranscendental R x
q : Ideal S
hq : q ∈ minimalPrimes S
⊢ IsStronglyTranscendental R ((Ideal.Quotient.mk q) x)

Tactic:
by
  refine Ideal.Quotient.mk_surjective.forall.mpr fun u p e ↦ ?_
  rw [← Ideal.Quotient.algebraMap_eq, aeval_algebraMap_apply, Ideal.Quotient.algebraMap_eq,
    ← map_mul, Ideal.Quotient.eq_zero_iff_mem] at e
  have := hq.1.1
  have : Ring.KrullDimLE 0 (Localization.AtPrime q) := .of_isLocalization _ hq _
  let : Field (Localization.AtPrime q) := Ring.KrullDimLE.isField_of_isReduced.toField
  obtain ⟨⟨m, hmq⟩, hm⟩ := (IsLocalization.map_eq_zero_iff q.primeCompl (Localization.AtPrime q)
    (aeval x p * u)).mp (by rw [← Ideal.mem_bot, ← IsLocalRing.maximalIdeal_eq_bot,
      ← Localization.AtPrime.map_eq_maximalIdeal]; exact Ideal.mem_map_of_mem _ e)
  ext i
  simp only [coeff_mul_C, coeff_map, coeff_zero, ← Ideal.Quotient.mk_algebraMap, ← map_mul,
    Ideal.Quotient.eq_zero_iff_mem]
  have : algebraMap R S (p.coeff i) * u * m = 0 := by
    simpa [← mul_assoc] using congr(($(hx (u * m) p (by linear_combination hm))).coeff i)
  exact (Ideal.IsPrime.mem_or_mem_of_mul_eq_zero ‹_› (by linear_combination this)).resolve_left hmq

Goal state after:
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
z : S
hz : z ∈ R[x]
hy : ⟨z, hz⟩ ∈ comap (algebraMap (↥R[x]) S) (Ideal.map (algebraMap R S) I)
⊢ ⟨z, hz⟩ ∈ Ideal.map (algebraMap R ↥R[x]) I

Tactic:
obtain ⟨p, hp, q, hq, hpq⟩ := Submodule.mem_sup.mp ((Ideal.eq_top_iff_one _).mp hx)

Goal state after:
case a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
z : S
hz : z ∈ R[x]
hy : ⟨z, hz⟩ ∈ comap (algebraMap (↥R[x]) S) (Ideal.map (algebraMap R S) I)
p : R
hp : p ∈ comap (algebraMap R S) (conductor R x)
q : R
hq : q ∈ I
hpq : p + q = 1
⊢ ⟨z, hz⟩ ∈ Ideal.map (algebraMap R ↥R[x]) I
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
Γ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
hv : IsTrivialOn K v
hle : v RatFunc.X ≤ 1
p : K[X]
i : ℕ
h0 : ¬p.coeff i = 0
⊢ i ∈ Finset.range (p.natDegree + 1) → v ((algebraMap K[X] K⟮X⟯) ((monomial i) (p.coeff i))) ≤ 1

Tactic:
· rw [← RatFunc.coePolynomial]
    simp_all [pow_le_one', ← RatFunc.algebraMap_eq_C, hv.eq_one _ h0]

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
inst✝¹ : IsDomain R
inst✝ : FaithfulSMul R S
p : S[X]
hp : IsAlmostIntegral R[X] p
i : ℕ
⊢ IsAlmostIntegral R (p.coeff i)

Tactic:
have H {q : S[X]} (hq : IsAlmostIntegral R[X] q) : IsAlmostIntegral R q.leadingCoeff := by
    obtain ⟨p, hp, hp'⟩ := hq
    refine ⟨p.leadingCoeff, by simpa using hp, fun n ↦ ?_⟩
    obtain ⟨r, hr⟩ := hp' n
    simp only [Algebra.smul_def, algebraMap_def, coe_mapRingHom] at hr ⊢
    by_cases h : algebraMap R S p.leadingCoeff * q.leadingCoeff ^ n = 0
    · simp [h]
    have h' : q.leadingCoeff ^ n ≠ 0 := by aesop
    use r.leadingCoeff
    simp only [← leadingCoeff_map_of_injective (FaithfulSMul.algebraMap_injective R S), hr] at h ⊢
    rw [← leadingCoeff_pow' h'] at h ⊢
    rw [leadingCoeff_mul' h]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDomain R
inst✝ : FaithfulSMul R S
p : S[X]
hp : IsAlmostIntegral R[X] p
i : ℕ
H : ∀ {q : S[X]}, IsAlmostIntegral R[X] q → IsAlmostIntegral R q.leadingCoeff
⊢ IsAlmostIntegral R (p.coeff i)
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
f : MvPolynomial σ S
H : ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)
⊢ IsIntegral (MvPolynomial σ R) f

Tactic:
← f.support_sum_monomial_coeff

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 : ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)
⊢ IsIntegral (MvPolynomial σ R) (∑ v ∈ f.support, (monomial v) (coeff v f))
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 Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
h₂ : Ideal.under R P = Ideal.under R Q
inst✝ : WeaklyQuasiFiniteAt R Q
this : (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R Q))) P).IsPrime
⊢ Ideal.under R (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R Q))) P) =
    Ideal.under R (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R Q))) Q)

Tactic:
by
      rw [← Ideal.under_under (B := S), ← Ideal.under_under (A := R) (B := S) (C := S ⧸ _)]
      dsimp [Ideal.under] at h₂ ⊢
      simp [Ideal.map_comap_le]
      simp [Ideal.map_comap_le, ← h₂]

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 S
inst✝⁴ : p.IsPrime
inst✝³ : QuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p))) p)
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra R A
q : Ideal (A ⊗[R] S)
inst✝ : q.IsPrime
hq : p = Ideal.comap TensorProduct.includeRight.toRingHom q
φ : A ⊗[R] S →ₐ[A] (A ⧸ Ideal.under A q) ⊗[R] (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R p)) :=
  TensorProduct.map (Ideal.Quotient.mkₐ A (Ideal.under A q))
    (Ideal.Quotient.mkₐ R (Ideal.map (algebraMap R S) (Ideal.under R p)))
hφ₁ : Function.Surjective ⇑φ
hφ₂ : RingHom.ker φ.toRingHom = Ideal.map (algebraMap A (A ⊗[R] S)) (Ideal.under A q)
hφ₃ :
  φ.comp TensorProduct.includeRight.toRingHom =
    TensorProduct.includeRight.comp (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p)))
this : (Ideal.map φ.toRingHom q).IsPrime
⊢ p ⊔ Ideal.comap (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p))) ⊥ =
    Ideal.comap (TensorProduct.includeRight.comp (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p))))
      (Ideal.map φ.toRingHom q)

Tactic:
← RingHom.ker_eq_comap_bot,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal S
inst✝⁴ : p.IsPrime
inst✝³ : QuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p))) p)
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra R A
q : Ideal (A ⊗[R] S)
inst✝ : q.IsPrime
hq : p = Ideal.comap TensorProduct.includeRight.toRingHom q
φ : A ⊗[R] S →ₐ[A] (A ⧸ Ideal.under A q) ⊗[R] (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R p)) :=
  TensorProduct.map (Ideal.Quotient.mkₐ A (Ideal.under A q))
    (Ideal.Quotient.mkₐ R (Ideal.map (algebraMap R S) (Ideal.under R p)))
hφ₁ : Function.Surjective ⇑φ
hφ₂ : RingHom.ker φ.toRingHom = Ideal.map (algebraMap A (A ⊗[R] S)) (Ideal.under A q)
hφ₃ :
  φ.comp TensorProduct.includeRight.toRingHom =
    TensorProduct.includeRight.comp (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p)))
this : (Ideal.map φ.toRingHom q).IsPrime
⊢ p ⊔ RingHom.ker (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p))) =
    Ideal.comap (TensorProduct.includeRight.comp (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p))))
      (Ideal.map φ.toRingHom q)
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 S
inst✝⁴ : p.IsPrime
inst✝³ : QuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p))) p)
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra R A
q : Ideal (A ⊗[R] S)
inst✝ : q.IsPrime
hq : p = Ideal.comap TensorProduct.includeRight.toRingHom q
φ : A ⊗[R] S →ₐ[A] (A ⧸ Ideal.under A q) ⊗[R] (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R p)) :=
  TensorProduct.map (Ideal.Quotient.mkₐ A (Ideal.under A q))
    (Ideal.Quotient.mkₐ R (Ideal.map (algebraMap R S) (Ideal.under R p)))
hφ₁ : Function.Surjective ⇑φ
hφ₂ : RingHom.ker φ.toRingHom = Ideal.map (algebraMap A (A ⊗[R] S)) (Ideal.under A q)
hφ₃ :
  φ.comp TensorProduct.includeRight.toRingHom =
    TensorProduct.includeRight.comp (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p)))
this : (Ideal.map φ.toRingHom q).IsPrime
⊢ p = Ideal.comap TensorProduct.includeRight.toRingHom (q ⊔ Ideal.comap φ.toRingHom ⊥)

Tactic:
← RingHom.ker_eq_comap_bot,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal S
inst✝⁴ : p.IsPrime
inst✝³ : QuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p))) p)
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra R A
q : Ideal (A ⊗[R] S)
inst✝ : q.IsPrime
hq : p = Ideal.comap TensorProduct.includeRight.toRingHom q
φ : A ⊗[R] S →ₐ[A] (A ⧸ Ideal.under A q) ⊗[R] (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R p)) :=
  TensorProduct.map (Ideal.Quotient.mkₐ A (Ideal.under A q))
    (Ideal.Quotient.mkₐ R (Ideal.map (algebraMap R S) (Ideal.under R p)))
hφ₁ : Function.Surjective ⇑φ
hφ₂ : RingHom.ker φ.toRingHom = Ideal.map (algebraMap A (A ⊗[R] S)) (Ideal.under A q)
hφ₃ :
  φ.comp TensorProduct.includeRight.toRingHom =
    TensorProduct.includeRight.comp (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p)))
this : (Ideal.map φ.toRingHom q).IsPrime
⊢ p = Ideal.comap TensorProduct.includeRight.toRingHom (q ⊔ RingHom.ker φ.toRingHom)
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
⊢ ∀ {U V : X.AffineZariskiSite} (f : (toOpensFunctor X).obj U ⟶ (toOpensFunctor X).obj V),
    Sieve.functorPushforward (toOpensFunctor X) ((toOpensFunctor X).imageSieve f) ∈
      (Opens.grothendieckTopology ↥X) ((toOpensFunctor X).obj U)

Tactic:
intro U V h x hx

Goal state after:
X : Scheme
U V : X.AffineZariskiSite
h : (toOpensFunctor X).obj U ⟶ (toOpensFunctor X).obj V
x : ↥X
hx : x ∈ (toOpensFunctor X).obj U
⊢ ∃ U_1 f, (Sieve.functorPushforward (toOpensFunctor X) ((toOpensFunctor X).imageSieve h)).arrows f ∧ x ∈ U_1
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case H.H
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]⁰
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
hq : φ ↑q ∈ S[X]⁰
hq' : φ ↑q' ∈ S[X]⁰
hqq' : φ ↑(q * q') ∈ S[X]⁰
⊢ { toFractionRing := Localization.mk (φ p * φ p') ⟨φ ↑q * φ ↑q', ⋯⟩ } =
    { toFractionRing := Localization.mk (φ p * φ p') (⟨φ ↑q, hq⟩ * ⟨φ ↑q', hq'⟩) }

Tactic:
Submonoid.mk_mul_mk

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
U : (X.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯).toPreZeroHypercover.1
⊢ ⇑(colimit.desc F (cocone X)) ⁻¹' ↑↑U = ↑(Hom.opensRange (colimit.ι F U))

Tactic:
← Scheme.Hom.coe_preimage

Goal state after:
X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
U : (X.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯).toPreZeroHypercover.1
⊢ ↑(colimit.desc F (cocone X) ⁻¹ᵁ ↑U) = ↑(Hom.opensRange (colimit.ι F U))
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case H.H.refine_3
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
y✝ a' : R[X] × ↥R[X]⁰
h : φ y✝.1 / φ ↑y✝.2 = φ a'.1 / φ ↑a'.2
this : y✝.1 * ↑a'.2 = a'.1 * ↑y✝.2
⊢ ↑(a'.1, a'.2).2 * (y✝.1, y✝.2).1 = ↑(y✝.1, y✝.2).2 * (a'.1, a'.2).1

Tactic:
mul_comm,

Goal state after:
case H.H.refine_3
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
y✝ a' : R[X] × ↥R[X]⁰
h : φ y✝.1 / φ ↑y✝.2 = φ a'.1 / φ ↑a'.2
this : ↑a'.2 * y✝.1 = a'.1 * ↑y✝.2
⊢ ↑(a'.1, a'.2).2 * (y✝.1, y✝.2).1 = ↑(y✝.1, y✝.2).2 * (a'.1, a'.2).1
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: case e'_2
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X : Scheme} {x : ↥X} (R : CommRingCat) {f : X ⟶ Spec R} [LocallyOfFiniteType f],
    (∃ S, X = Spec S) → (QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩})
hX : ¬∃ S, X = Spec S
i : X.affineCover.I₀
x : ↥(X.affineCover.X i)
ι : X.affineCover.X i ⟶ X := ⋯
⊢ IsOpen {⟨(X.affineCover.f i) x, ⋯⟩} ↔ IsOpen {⟨x, ⋯⟩}

Tactic:
rw [((f ⁻¹' {f (ι x)}).restrictPreimage_isOpenEmbedding
      ι.isOpenEmbedding).isOpen_iff_image_isOpen, Set.image_singleton]

Goal state after:
case e'_2
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X : Scheme} {x : ↥X} (R : CommRingCat) {f : X ⟶ Spec R} [LocallyOfFiniteType f],
    (∃ S, X = Spec S) → (QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩})
hX : ¬∃ S, X = Spec S
i : X.affineCover.I₀
x : ↥(X.affineCover.X i)
ι : X.affineCover.X i ⟶ X := X.affineCover.f i
⊢ IsOpen {⟨(X.affineCover.f i) x, ⋯⟩} ↔ IsOpen {(⇑f ⁻¹' {f (ι x)}).restrictPreimage ⇑ι ⟨x, ⋯⟩}
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case left.e_a.e_6
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
hdivq : C a.leadingCoeff⁻¹ * gcd p q ∣ q
⊢ a.leadingCoeff⁻¹ * (gcd p q).leadingCoeff / q.leadingCoeff * a.leadingCoeff⁻¹⁻¹ =
    (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹

Tactic:
mul_comm,

Goal state after:
case left.e_a.e_6
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
hdivq : C a.leadingCoeff⁻¹ * gcd p q ∣ q
⊢ a.leadingCoeff⁻¹⁻¹ * (a.leadingCoeff⁻¹ * (gcd p q).leadingCoeff / q.leadingCoeff) =
    (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case left.e_a.e_6
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
hdivq : C a.leadingCoeff⁻¹ * gcd p q ∣ q
⊢ 1 * ((gcd p q).leadingCoeff / q.leadingCoeff) = (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹

Tactic:
one_mul,

Goal state after:
case left.e_a.e_6
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
hdivq : C a.leadingCoeff⁻¹ * gcd p q ∣ q
⊢ (gcd p q).leadingCoeff / q.leadingCoeff = (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case right.e_a.e_6
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
hdivq : C a.leadingCoeff⁻¹ * gcd p q ∣ q
⊢ a.leadingCoeff⁻¹ * (gcd p q).leadingCoeff / q.leadingCoeff * a.leadingCoeff⁻¹⁻¹ =
    (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹

Tactic:
mul_comm,

Goal state after:
case right.e_a.e_6
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
hdivq : C a.leadingCoeff⁻¹ * gcd p q ∣ q
⊢ a.leadingCoeff⁻¹⁻¹ * (a.leadingCoeff⁻¹ * (gcd p q).leadingCoeff / q.leadingCoeff) =
    (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹