mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: R : Type u_3
S : Type u_4
F : Type u_5
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]⁰
n : R[X]
d : ↥R[X]⁰
⊢ (map φ hφ) { toFractionRing := Localization.mk n d } = { toFractionRing := Localization.mk (φ n) ⟨φ ↑d, ⋯⟩ }

Tactic:
simp only [map, MonoidHom.coe_mk, OneHom.coe_mk, liftOn_ofFractionRing_mk,
    Submonoid.mem_comap.mp (hφ d.2), ↓reduceDIte]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : CommRing B
inst✝¹ : Algebra R B
M : Submonoid R
inst✝ : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B)) :=
  (Algebra.TensorProduct.includeRight.comp (integralClosure R B).val).codRestrict
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this✝² : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B)) := φ.toAlgebra
this✝¹ : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B))
this✝ : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B))) (S ⊗[R] B)
this : IsLocalization (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M) ↥(integralClosure S (S ⊗[R] B))
⊢ ⇑(toIntegralClosure R S B) =
    ⇑(IsLocalization.algEquiv (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M) (S ⊗[R] ↥(integralClosure R B))
        ↥(integralClosure S (S ⊗[R] B)))

Tactic:
rw [← AlgHom.coe_restrictScalars' R, ← AlgEquiv.coe_restrictScalars R, ← AlgEquiv.coe_toAlgHom]

Goal state after:
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : CommRing B
inst✝¹ : Algebra R B
M : Submonoid R
inst✝ : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B)) :=
  (Algebra.TensorProduct.includeRight.comp (integralClosure R B).val).codRestrict
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this✝² : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B)) := φ.toAlgebra
this✝¹ : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B))
this✝ : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B))) (S ⊗[R] B)
this : IsLocalization (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M) ↥(integralClosure S (S ⊗[R] B))
⊢ ⇑(AlgHom.restrictScalars R (toIntegralClosure R S B)) =
    ⇑↑(AlgEquiv.restrictScalars R
          (IsLocalization.algEquiv (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
            (S ⊗[R] ↥(integralClosure R B)) ↥(integralClosure S (S ⊗[R] B))))
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Module.Finite R S
inst✝² : IsUnramifiedAt R Q
inst✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
this✝⁴ : p.IsPrime
this✝³ : Module p.ResidueField (p.Fiber S) := leftModule
this✝² : SMul p.ResidueField (p.Fiber S) := this✝³.toSMul
this✝¹ : IsScalarTower p.ResidueField (p.Fiber S) (p.Fiber S) := IsScalarTower.right
this✝ : Module.Finite p.ResidueField (p.Fiber S) := Module.Finite.base_change R p.ResidueField S
this : IsArtinianRing (p.Fiber S)
α : ↑(p.primesOver S) ≃o PrimeSpectrum (p.Fiber S) := PrimeSpectrum.primesOverOrderIsoFiber R S p
x : p.ResidueField ⊗[R] S
φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField :=
  TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯
hx0 : φ x ≠ 0
hx : p.ResidueField[φ x] = ⊤
r : p.Fiber S
hrQ : r ∉ (α ⟨Q, ⋯⟩).asIdeal
hrid : IsIdempotentElem r
hr : ∀ (q : Ideal (p.Fiber S)), q.IsPrime → q ≠ (α ⟨Q, ⋯⟩).asIdeal → r ∈ q
s : R
hsQ : s ∉ p
t : S
e : s • (r * x) = 1 ⊗ₜ[R] t
hsQ' : (algebraMap R Q.ResidueField) s ≠ 0
hrQ' : φ r = 1
e' : (algebraMap R Q.ResidueField) s * φ x = (algebraMap S Q.ResidueField) t
⊢ ∀ Q' ∈ (Ideal.under R Q).primesOver S, Q' ≠ Q → t ∈ Q'

Tactic:
rintro Q' ⟨_, _⟩ H
    let := Localization.AtPrime.algebraOfLiesOver p Q'
    have hsQ'' : algebraMap R Q'.ResidueField s ≠ 0 := by
      suffices s ∉ Q'.under _ by simpa [IsScalarTower.algebraMap_apply R S Q'.ResidueField]
      rwa [← Q'.over_def p]
    let φ' : p.Fiber S →ₐ[p.ResidueField] Q'.ResidueField := TensorProduct.lift
        (Algebra.ofId _ _) (IsScalarTower.toAlgHom _ _ _) fun _ _ ↦ .all _ _
    have H : φ' r = 0 := (hr (α ⟨Q', ⟨‹_›, ‹_›⟩⟩).asIdeal inferInstance (by
        rwa [ne_eq, ← PrimeSpectrum.ext_iff, EmbeddingLike.apply_eq_iff_eq, Subtype.mk.injEq]) :)
    rw [← Ideal.algebraMap_residueField_eq_zero]
    trans φ' (1 ⊗ₜ t)
    · simp [φ']
    · simpa [smul_def, H] using congr(φ' $e).symm

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

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : Module.Finite R S
inst✝ : IsUnramifiedAt R Q
x : S
hQ' : (Ideal.under (↥R[x]) Q).primesOver S = {Q}
hQ'Q : Function.Bijective ⇑(algebraMap (Ideal.under (↥R[x]) Q).ResidueField Q.ResidueField)
S' : Subalgebra R S := R[x]
Q' : Ideal ↥S' := Ideal.under (↥S') Q
this✝² : Algebra (Localization.AtPrime Q') (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver Q' Q
this✝¹ : Module.Finite (↥S') S
this✝ : IsUnramifiedAt (↥S') Q
hφ : Function.Bijective ⇑(Localization.localRingHom Q' Q ↑S'.val ⋯)
r : ↥R[x]
hrQ' : r ∉ Ideal.under (↥R[x]) Q
H : ∀ (r' : ↥R[x]), r ∣ r' → Function.Bijective ⇑(Localization.awayMap (algebraMap (↥R[x]) S) r')
this : Module.Finite R ↥S'
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
have : IsUnramifiedAt R Q' := .of_equiv <| .symm <| .ofBijective (IsScalarTower.toAlgHom _ _ _) hφ

Goal state after:
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : Module.Finite R S
inst✝ : IsUnramifiedAt R Q
x : S
hQ' : (Ideal.under (↥R[x]) Q).primesOver S = {Q}
hQ'Q : Function.Bijective ⇑(algebraMap (Ideal.under (↥R[x]) Q).ResidueField Q.ResidueField)
S' : Subalgebra R S := R[x]
Q' : Ideal ↥S' := Ideal.under (↥S') Q
this✝³ : Algebra (Localization.AtPrime Q') (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver Q' Q
this✝² : Module.Finite (↥S') S
this✝¹ : IsUnramifiedAt (↥S') Q
hφ : Function.Bijective ⇑(Localization.localRingHom Q' Q ↑S'.val ⋯)
r : ↥R[x]
hrQ' : r ∉ Ideal.under (↥R[x]) Q
H : ∀ (r' : ↥R[x]), r ∣ r' → Function.Bijective ⇑(Localization.awayMap (algebraMap (↥R[x]) S) r')
this✝ : Module.Finite R ↥S'
this : IsUnramifiedAt R Q'
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝²⁸ : CommRing R
inst✝²⁷ : CommRing S
inst✝²⁶ : Algebra R S
K : Type u_4
L : Type u_5
inst✝²⁵ : Field K
inst✝²⁴ : Field L
inst✝²³ : Algebra R K
inst✝²² : Algebra R L
inst✝²¹ : Algebra S L
inst✝²⁰ : Algebra K L
inst✝¹⁹ : IsScalarTower R K L
inst✝¹⁸ : IsScalarTower R S L
inst✝¹⁷ : IsFractionRing R K
inst✝¹⁶ : IsFractionRing S L
R' : Type u_6
S' : Type u_7
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : CommRing S'
inst✝¹³ : Algebra R R'
inst✝¹² : Algebra R' S'
inst✝¹¹ : Algebra R S'
inst✝¹⁰ : Algebra S' L
inst✝⁹ : Algebra R' L
inst✝⁸ : IsScalarTower R' S' L
inst✝⁷ : Algebra R' K
inst✝⁶ : IsScalarTower R' K L
inst✝⁵ : IsScalarTower R R' S'
inst✝⁴ : FaithfulSMul S' L
inst✝³ : IsIntegralClosure R' R K
inst✝² : IsScalarTower R R' K
f : S →ₐ[R] S'
hf₁ : Function.Surjective ⇑(TensorProduct.lift (ofId R' S') f ⋯)
hf₂ : (algebraMap S' L).comp f.toRingHom = algebraMap S L
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
hx : IsStronglyTranscendental R x
this✝¹ : IsDomain S'
this✝ : IsDomain R
this : Algebra.IsIntegral R R'
⊢ False

Tactic:
have : FaithfulSMul R' K := (faithfulSMul_iff_algebraMap_injective _ _).mpr
    (IsIntegralClosure.algebraMap_injective R' R K)

Goal state after:
R : Type u_1
S : Type u_2
inst✝²⁸ : CommRing R
inst✝²⁷ : CommRing S
inst✝²⁶ : Algebra R S
K : Type u_4
L : Type u_5
inst✝²⁵ : Field K
inst✝²⁴ : Field L
inst✝²³ : Algebra R K
inst✝²² : Algebra R L
inst✝²¹ : Algebra S L
inst✝²⁰ : Algebra K L
inst✝¹⁹ : IsScalarTower R K L
inst✝¹⁸ : IsScalarTower R S L
inst✝¹⁷ : IsFractionRing R K
inst✝¹⁶ : IsFractionRing S L
R' : Type u_6
S' : Type u_7
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : CommRing S'
inst✝¹³ : Algebra R R'
inst✝¹² : Algebra R' S'
inst✝¹¹ : Algebra R S'
inst✝¹⁰ : Algebra S' L
inst✝⁹ : Algebra R' L
inst✝⁸ : IsScalarTower R' S' L
inst✝⁷ : Algebra R' K
inst✝⁶ : IsScalarTower R' K L
inst✝⁵ : IsScalarTower R R' S'
inst✝⁴ : FaithfulSMul S' L
inst✝³ : IsIntegralClosure R' R K
inst✝² : IsScalarTower R R' K
f : S →ₐ[R] S'
hf₁ : Function.Surjective ⇑(TensorProduct.lift (ofId R' S') f ⋯)
hf₂ : (algebraMap S' L).comp f.toRingHom = algebraMap S L
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
hx : IsStronglyTranscendental R x
this✝² : IsDomain S'
this✝¹ : IsDomain R
this✝ : Algebra.IsIntegral R R'
this : FaithfulSMul R' K
⊢ False
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℕ
P : ↥R[X]_m
⊢ ↑((addLinearEquiv R m n).symm ((LinearMap.inl R (↥R[X]_m) ↥R[X]_n) P)) = ↑P

Tactic:
rw [← (basis ..).sum_repr P]
  simp [-LinearMap.coe_inl, addLinearEquiv_symm_apply_inl_basis]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : R[X]
m n : ℕ
⊢ resultant 0 g m n = 0 ^ n * g.coeff 0 ^ m

Tactic:
rw [resultant_comm, resultant_zero_right]
  cases n <;> simp

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin 0) R →ₐ[R] S
hf : f.Finite
⊢ Module.Finite R S

Tactic:
rw [← RingHom.finite_algebraMap]

Goal state after:
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin 0) R →ₐ[R] S
hf : f.Finite
⊢ (algebraMap R S).Finite
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case succ.e_a.e_a
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ (-1) ^ (m + 1 + n + m) = (-1) ^ (n + 1)

Tactic:
trans (-1) ^ (2 * m + (n + 1))
      · congr 1; lia
      · simp [pow_add]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.Opens
hU : IsAffineOpen U
⊢ (normalizationObjIso f hU).hom ≫ CommRingCat.ofHom (integralClosure ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U)).val.toRingHom =
    appLE (toNormalization f) (fromNormalization f ⁻¹ᵁ U) (f ⁻¹ᵁ U) ⋯

Tactic:
rw [appLE, f.toNormalization_app_preimage ⟨U, hU⟩, Category.assoc]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.Opens
hU : IsAffineOpen U
⊢ (normalizationObjIso f hU).hom ≫ CommRingCat.ofHom (integralClosure ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U)).val.toRingHom =
    (normalizationObjIso f ⋯).hom ≫
      (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑⟨U, hU⟩) ↑Γ(X, f ⁻¹ᵁ ↑⟨U, hU⟩)).val ≫ X.presheaf.map (eqToHom ⋯).op) ≫
        X.presheaf.map (homOfLE ⋯).op
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
n : ℕ
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg : natDegree 0 ≤ n
hf' : ¬f.natDegree = 0
⊢ f.resultant 0 f.natDegree n = (Multiset.map (fun x ↦ eval x 0) f.roots).prod

Tactic:
simp [← hf.natDegree_eq_card_roots, hf']

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case e'_2.e'_3
R : Type u_1
inst✝ : CommRing R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
⊢ X = X - C 0

Tactic:
simp [coeff_zero_eq_eval_zero]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case e'_3
R : Type u_1
inst✝ : CommRing R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
⊢ g.coeff 0 = eval 0 g

Tactic:
simp [coeff_zero_eq_eval_zero]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
⊢ (X ^ m).resultant g m n = g.coeff 0 ^ m

Tactic:
by
  convert! resultant_X_sub_C_pow_left 0 g m n hn <;> simp [coeff_zero_eq_eval_zero]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case e'_2.e'_4
R : Type u_1
inst✝ : CommRing R
f : R[X]
m n : ℕ
hm : f.natDegree ≤ m
⊢ X = X - C 0

Tactic:
simp [coeff_zero_eq_eval_zero]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case e'_3
R : Type u_1
inst✝ : CommRing R
f : R[X]
m n : ℕ
hm : f.natDegree ≤ m
⊢ f.coeff 0 = eval 0 f

Tactic:
simp [coeff_zero_eq_eval_zero]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]),
    g.natDegree ≠ 0 →
      IsDomain R →
        (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
          g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : ¬f = 0
hg0 : ¬g = 0
S : Type (max 0 u_1) := MvPolynomial R ℤ
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g

Tactic:
let φ : S →+* R := MvPolynomial.eval₂Hom (algebraMap _ _) id

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]),
    g.natDegree ≠ 0 →
      IsDomain R →
        (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
          g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : ¬f = 0
hg0 : ¬g = 0
S : Type (max 0 u_1) := MvPolynomial R ℤ
φ : S →+* R := MvPolynomial.eval₂Hom (algebraMap ℤ R) id
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case e'_3
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
q : { q // ↑q.1 * ↑q.2 = map (algebraMap R S) ↑p } :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ↑(↑q).1 = (mapRingHom f.toRingHom) ↑(factor₁ m k hn p)

Tactic:
simp [q, UniversalFactorizationRing.homEquiv,
          AlgHom.comp_toRingHom, ← Polynomial.map_map]

Goal state after:
case e'_3
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
q : { q // ↑q.1 * ↑q.2 = map (algebraMap R S) ↑p } :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case e'_4
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
q : { q // ↑q.1 * ↑q.2 = map (algebraMap R S) ↑p } :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ↑(↑q).2 = (mapRingHom f.toRingHom) ↑(factor₂ m k hn p)

Tactic:
simp [q, UniversalFactorizationRing.homEquiv,
          AlgHom.comp_toRingHom, ← Polynomial.map_map]

Goal state after:
case e'_4
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
q : { q // ↑q.1 * ↑q.2 = map (algebraMap R S) ↑p } :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
b₁ : Module.Basis (Fin (m + n)) R (↥R[X]_m × ↥R[X]_n) :=
  ((degreeLT.basis R m).prod (degreeLT.basis R n)).reindex finSumFinEquiv
b₂ : Module.Basis (Fin (m + n)) R ↥R[X]_(m + n) := degreeLT.basis R (m + n)
this :
  (Matrix.toLin b₂ b₂)
      ((LinearMap.toMatrix b₁ b₂) (f.sylvesterMap g hf hg) *
        ((LinearMap.toMatrix b₁ b₂) (f.sylvesterMap g hf hg)).adjugate) =
    (Matrix.toLin b₂ b₂) (((LinearMap.toMatrix b₁ b₂) (f.sylvesterMap g hf hg)).det • 1)
⊢ f.sylvesterMap g hf hg ∘ₗ f.adjSylvester g = f.resultant g m n • LinearMap.id

Tactic:
Matrix.toLin_mul b₂ b₁ b₂,

Goal state after:
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
b₁ : Module.Basis (Fin (m + n)) R (↥R[X]_m × ↥R[X]_n) :=
  ((degreeLT.basis R m).prod (degreeLT.basis R n)).reindex finSumFinEquiv
b₂ : Module.Basis (Fin (m + n)) R ↥R[X]_(m + n) := degreeLT.basis R (m + n)
this :
  (Matrix.toLin b₁ b₂) ((LinearMap.toMatrix b₁ b₂) (f.sylvesterMap g hf hg)) ∘ₗ
      (Matrix.toLin b₂ b₁) ((LinearMap.toMatrix b₁ b₂) (f.sylvesterMap g hf hg)).adjugate =
    (Matrix.toLin b₂ b₂) (((LinearMap.toMatrix b₁ b₂) (f.sylvesterMap g hf hg)).det • 1)
⊢ f.sylvesterMap g hf hg ∘ₗ f.adjSylvester g = f.resultant g m n • LinearMap.id
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : FiniteType R S
inst✝⁷ : CommRing R'
inst✝⁶ : Algebra R R'
inst✝⁵ : CommRing R''
inst✝⁴ : Algebra R R''
inst✝³ : Algebra R'' S
inst✝² : Algebra.IsIntegral R R''
inst✝¹ : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst✝ : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e : (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)) e₀ = e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' → P'' = Ideal.comap (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom P'
g : R''
hgq : (algebraMap R'' S) g ∉ q
hg : Function.Surjective ⇑(Localization.awayMap (algebraMap R'' S) g)
this✝ : Algebra.IsIntegral R' (Localization.Away e₀)
f : R'
hfP : f ∉ P
hf : (Localization.awayMapₐ (ofId R' (Localization.Away e)) f).Finite
φ : R' ⊗[R] S →ₐ[R'] Localization.Away f ⊗[R] S := TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)
algInst✝ : Algebra (R' ⊗[R] S) (Localization.Away f ⊗[R] S) := φ.toAlgebra
this : Submonoid.powers (f ⊗ₜ[R] 1) = algebraMapSubmonoid (R' ⊗[R] S) (Submonoid.powers f)
⊢ IsLocalization (algebraMapSubmonoid (R' ⊗[R] S) (Submonoid.powers f)) (Localization.Away f ⊗[R] S)

Tactic:
refine IsLocalization.tensorProduct_tensorProduct _ _ _ _ ?_

Goal state after:
R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : FiniteType R S
inst✝⁷ : CommRing R'
inst✝⁶ : Algebra R R'
inst✝⁵ : CommRing R''
inst✝⁴ : Algebra R R''
inst✝³ : Algebra R'' S
inst✝² : Algebra.IsIntegral R R''
inst✝¹ : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst✝ : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e : (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)) e₀ = e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' → P'' = Ideal.comap (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom P'
g : R''
hgq : (algebraMap R'' S) g ∉ q
hg : Function.Surjective ⇑(Localization.awayMap (algebraMap R'' S) g)
this✝ : Algebra.IsIntegral R' (Localization.Away e₀)
f : R'
hfP : f ∉ P
hf : (Localization.awayMapₐ (ofId R' (Localization.Away e)) f).Finite
φ : R' ⊗[R] S →ₐ[R'] Localization.Away f ⊗[R] S := TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)
algInst✝ : Algebra (R' ⊗[R] S) (Localization.Away f ⊗[R] S) := φ.toAlgebra
this : Submonoid.powers (f ⊗ₜ[R] 1) = algebraMapSubmonoid (R' ⊗[R] S) (Submonoid.powers f)
⊢ (algebraMap (R' ⊗[R] S) (Localization.Away f ⊗[R] S)).comp TensorProduct.includeRight.toRingHom =
    TensorProduct.includeRight.toRingHom
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : IsProper f
y : ↥Y
hx : (⇑f ⁻¹' {y}).Finite
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f))ᶜ)ᶜ, is_open' := ⋯ }
⊢ IsFinite (f ∣_ V)

Tactic:
suffices LocallyQuasiFinite (f ∣_ V) from .of_isProper_of_locallyQuasiFinite _

Goal state after:
case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : IsProper f
y : ↥Y
hx : (⇑f ⁻¹' {y}).Finite
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f))ᶜ)ᶜ, is_open' := ⋯ }
⊢ LocallyQuasiFinite (f ∣_ V)
Module: Mathlib.RingTheory.Ideal.CotangentBaseChange

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
I : Ideal S
inst✝ : Module.Flat R T
a : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom
f : (map a I).Cotangent →ₗ[T] T ⊗[R] S ⧸ map a I ^ 2 := ↑T (map a I).cotangentToQuotientSquare
g : T ⊗[R] I.Cotangent →ₗ[T] T ⊗[R] (S ⧸ I ^ 2) := (AlgebraTensorModule.lTensor T T) (↑R I.cotangentToQuotientSquare)
hₐ : T ⊗[R] (S ⧸ I ^ 2) ≃ₐ[T] T ⊗[R] S ⧸ map a I ^ 2 :=
  (Algebra.TensorProduct.tensorQuotientEquiv T S T (I ^ 2)).trans (quotientEquivAlgOfEq T ⋯)
⊢ Function.Injective ⇑(f ∘ₗ tensorCotangentHom R T I)

Tactic:
have : f ∘ₗ tensorCotangentHom R T I = hₐ.toLinearMap ∘ₗ g := by
    ext x
    obtain ⟨x, rfl⟩ := I.toCotangent_surjective x
    dsimp [f, g, hₐ]
    rw [tensorCotangentHom_tmul, one_smul, Ideal.toCotangent_to_quotient_square]
    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
I : Ideal S
inst✝ : Module.Flat R T
a : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom
f : (map a I).Cotangent →ₗ[T] T ⊗[R] S ⧸ map a I ^ 2 := ↑T (map a I).cotangentToQuotientSquare
g : T ⊗[R] I.Cotangent →ₗ[T] T ⊗[R] (S ⧸ I ^ 2) := (AlgebraTensorModule.lTensor T T) (↑R I.cotangentToQuotientSquare)
hₐ : T ⊗[R] (S ⧸ I ^ 2) ≃ₐ[T] T ⊗[R] S ⧸ map a I ^ 2 :=
  (Algebra.TensorProduct.tensorQuotientEquiv T S T (I ^ 2)).trans (quotientEquivAlgOfEq T ⋯)
this : f ∘ₗ tensorCotangentHom R T I = hₐ.toLinearMap ∘ₗ g
⊢ Function.Injective ⇑(f ∘ₗ tensorCotangentHom R T I)