mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

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

Tactic:
have H : pullback.snd f ι ⁻¹' {pullback.snd f ι x} =
        pullback.fst f ι ⁻¹' f ⁻¹' {f (pullback.fst f ι x)} := by
      rw [← Set.preimage_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, ← Scheme.Hom.comp_apply,
        pullback.condition]
      simp [← Set.image_singleton, Set.preimage_comp, Set.preimage_image_eq _ ι.injective]

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

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
p : K[X]
⊢ ∀ {q a : K[X]},
    q ≠ 0 →
      a ≠ 0 →
        (if a * q = 0 then (0, 1)
          else
            let r := gcd (a * p) (a * q);
            (C (a * q / r).leadingCoeff⁻¹ * (a * p / r), C (a * q / r).leadingCoeff⁻¹ * (a * q / r))) =
          if q = 0 then (0, 1)
          else
            let r := gcd p q;
            (C (q / r).leadingCoeff⁻¹ * (p / r), C (q / r).leadingCoeff⁻¹ * (q / r))

Tactic:
q

Goal state after:
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q : K[X]
⊢ ∀ {a : K[X]},
    q ≠ 0 →
      a ≠ 0 →
        (if a * q = 0 then (0, 1)
          else
            let r := gcd (a * p) (a * q);
            (C (a * q / r).leadingCoeff⁻¹ * (a * p / r), C (a * q / r).leadingCoeff⁻¹ * (a * q / r))) =
          if q = 0 then (0, 1)
          else
            let r := gcd p q;
            (C (q / r).leadingCoeff⁻¹ * (p / r), C (q / r).leadingCoeff⁻¹ * (q / r))
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: 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
P : StandardEtalePair R
x : S
h : P.HasMap x
⊢ {C P.f, Y * C P.g - 1} ⊆ ↑(RingHom.ker (aevalAeval x ↑⋯.unit⁻¹))

Tactic:
by simp [Set.pair_subset_iff, h.1]

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

Goal state before:
pp: case refine_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
P : StandardEtalePair R
⊢ (IsLocalization.Away.liftAlgHom ((AdjoinRoot.mk P.f) P.g) ⋯).comp
      (P.lift ((algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g))) (AdjoinRoot.root P.f)) ⋯) =
    AlgHom.id R P.Ring

Tactic:
· ext; simp

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

Goal state before:
pp: case hb
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)) := ⋯
this✝² : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B)) := ⋯
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))
x : ↥(integralClosure R B)
⊢ ↑(((AlgHom.restrictScalars R (AlgHom.restrictScalars R (toIntegralClosure R S B))).comp
          Algebra.TensorProduct.includeRight)
        x) =
    ↑(((AlgHom.restrictScalars R
              ↑(AlgEquiv.restrictScalars R
                  (IsLocalization.algEquiv (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
                    (S ⊗[R] ↥(integralClosure R B)) ↥(integralClosure S (S ⊗[R] B))))).comp
          Algebra.TensorProduct.includeRight)
        x)

Tactic:
dsimp [toIntegralClosure]

Goal state after:
case hb
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))
x : ↥(integralClosure R B)
⊢ 1 ⊗ₜ[R] ↑x =
    ↑((IsLocalization.algEquiv (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M) (S ⊗[R] ↥(integralClosure R B))
          ↥(integralClosure S (S ⊗[R] B)))
        (1 ⊗ₜ[R] x))
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
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
y : B
hy : IsIntegral R y
⊢ ∃ g, φ (derivative f) * y = φ g ∧ ∀ (i : ℕ), IsIntegral R (g.coeff i)

Tactic:
cases subsingleton_or_nontrivial B

Goal state after:
case inl
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
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
y : B
hy : IsIntegral R y
h✝ : Subsingleton B
⊢ ∃ g, φ (derivative f) * y = φ g ∧ ∀ (i : ℕ), IsIntegral R (g.coeff i)

case inr
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
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
y : B
hy : IsIntegral R y
h✝ : Nontrivial B
⊢ ∃ g, φ (derivative f) * y = φ g ∧ ∀ (i : ℕ), IsIntegral R (g.coeff i)
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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hp : φ p * t ∈ φ.range
⊢ ∃ q n, IsIntegral R (p.leadingCoeff ^ n • t - φ q)

Tactic:
set a := p.leadingCoeff
  let R' := Localization.Away a
  let S' := Localization.Away (algebraMap R S a)
  let : Algebra R' S' := (Localization.awayMap (algebraMap R S) a).toAlgebra
  have : IsScalarTower R R' S' := .of_algebraMap_eq (by
    simp +zetaDelta [RingHom.algebraMap_toAlgebra, IsLocalization.Away.map, ← algebraMap_apply R S])
  have ha : IsUnit (algebraMap R R' a) := IsLocalization.Away.algebraMap_isUnit a
  have H : (aeval ((algebraMap S S') (φ X))).toRingHom.comp (mapRingHom (algebraMap R R')) =
    (algebraMap S S').comp φ := by ext <;>
      simp [-Polynomial.algebraMap_apply, ← Polynomial.algebraMap_eq, ← algebraMap_apply]
  obtain ⟨q, hq⟩ := exists_isIntegral_sub_of_isIntegralElem_of_mul_mem_range (R := R')
    (aeval (algebraMap S S' (φ X))) (algebraMap S S' t) (C ha.unit⁻¹.1 * p.map (algebraMap _ _)) (by
      obtain ⟨q, hqm, hq⟩ := ht
      refine ⟨q.map (mapRingHom (algebraMap _ _)), hqm.map _, ?_⟩
      rw [eval₂_map, H, ← hom_eval₂, ← AlgHom.toRingHom_eq_coe, hq, map_zero]) (by
      nontriviality R'
      simp [Monic, leadingCoeff_C_mul_of_isUnit,
        leadingCoeff_map_of_leadingCoeff_ne_zero _ ha.ne_zero, a]) (by
      obtain ⟨r, hr : φ r = _⟩ := hp
      use C ha.unit⁻¹.1 * mapRingHom (algebraMap R R') r
      simp [aeval_algebraMap_apply, aeval_algHom_apply, hr, mul_assoc])
  obtain ⟨_, ⟨n, rfl⟩, e⟩ := IsLocalization.integerNormalization_spec (.powers a) q
  generalize IsLocalization.integerNormalization (.powers a) q = q' at e
  have : IsIntegral R' ((algebraMap S S') (a ^ n • t - φ q')) := by
    have : algebraMap S S' (φ q') = (algebraMap R S' a) ^ n * aeval (algebraMap S S' (φ X)) q := by
      simpa [Algebra.smul_def, aeval_algebraMap_apply, aeval_algHom_apply, ← algebraMap_apply] using
        congr(aeval (algebraMap S S' (φ X)) $e)
    simpa [Algebra.smul_def, ← mul_sub, ← algebraMap_apply, this] using
      (isIntegral_algebraMap (A := S') (x := algebraMap R R' a ^ n)).mul hq
  obtain ⟨⟨_, m, rfl⟩, hm⟩ := this.exists_multiple_integral_of_isLocalization (.powers a) _
  simp only [Algebra.smul_def, Submonoid.smul_def, algebraMap_apply R S S', ← map_mul] at hm
  obtain ⟨_, ⟨k, rfl⟩, hk⟩ := IsLocalization.exists_isIntegral_smul_of_isIntegral_map (.powers a) hm
  refine ⟨C a ^ (k + m) * q', k + m + n, ?_⟩
  convert! hk using 1
  simp only [Algebra.smul_def, map_pow, ← Polynomial.algebraMap_eq, map_mul, AlgHom.commutes]
  ring

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℕ
PQ : ↥R[X]_m × ↥R[X]_n
⊢ ↑((addLinearEquiv R m n).symm PQ) = ↑PQ.1 + X ^ m * ↑PQ.2

Tactic:
by
  rw [X_pow_mul, addLinearEquiv_symm_apply]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f g : R[X]
m n : ℕ
φ : R →+* S
⊢ (map φ f).resultant (map φ g) m n = φ (f.resultant g m n)

Tactic:
by
  simp [resultant, Polynomial.sylvester_map_map, RingHom.map_det]

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

Goal state before:
pp: case succ.e_a.right
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
i : Fin (m + (n + 1))
j : Fin (n + 1)
this : (Fin.castAdd (n + 1) (Fin.last m)).succAbove (Fin.cast ⋯ (Fin.natAdd m j)) = Fin.natAdd (m + 1) j
⊢ Fin.addCases (fun j₁ ↦ if ↑j₁ ≤ ↑i ∧ ↑i ≤ ↑j₁ + (n + 1) then g.coeff (↑i - ↑j₁) else 0)
      (fun j₁ ↦ if ↑j₁ ≤ ↑i ∧ ↑i ≤ ↑j₁ + (m + 1) then f.coeff (↑i - ↑j₁) else 0)
      ((Fin.castAdd (n + 1) (Fin.last m)).succAbove (Fin.cast ⋯ (Fin.natAdd m j))) =
    Fin.addCases (fun j₁ ↦ if ↑j₁ ≤ ↑i ∧ ↑i ≤ ↑j₁ + (n + 1) then g.coeff (↑i - ↑j₁) else 0)
      (fun j₁ ↦ if ↑j₁ ≤ ↑i ∧ ↑i ≤ ↑j₁ + m then f.coeff (↑i - ↑j₁) else 0) (Fin.natAdd m j)

Tactic:
simp only [ite_and, this, Fin.addCases_right]

Goal state after:
case succ.e_a.right
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
i : Fin (m + (n + 1))
j : Fin (n + 1)
this : (Fin.castAdd (n + 1) (Fin.last m)).succAbove (Fin.cast ⋯ (Fin.natAdd m j)) = Fin.natAdd (m + 1) j
⊢ (if ↑j ≤ ↑i then if ↑i ≤ ↑j + (m + 1) then f.coeff (↑i - ↑j) else 0 else 0) =
    if ↑j ≤ ↑i then if ↑i ≤ ↑j + m then f.coeff (↑i - ↑j) else 0 else 0
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case refine_3
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : adjoin R ↑s = ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : S → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := ⟨r, ⋯⟩
this :
  (IsScalarTower.toAlgHom R S (Localization.Away ((adjoin R t).val r'))).range ≤
    (Localization.awayMapₐ (adjoin R t).val r').range
x : S
n : ℕ
y : Localization.Away r'
hy :
  (Localization.awayMap (adjoin R t).val.toRingHom r') y =
    (IsScalarTower.toAlgHom R S (Localization.Away ((adjoin R t).val r'))).toRingHom x
⊢ (Localization.awayMap (adjoin R t).val.toRingHom r') (y * Localization.Away.invSelf r' ^ n) =
    IsLocalization.mk' (Localization.Away ((adjoin R t).val.toRingHom r')) x
      ⟨(fun x ↦ (adjoin R t).val.toRingHom r' ^ x) n, ⋯⟩

Tactic:
simp only [map_mul, map_pow, hy]

Goal state after:
case refine_3
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : adjoin R ↑s = ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : S → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := ⟨r, ⋯⟩
this :
  (IsScalarTower.toAlgHom R S (Localization.Away ((adjoin R t).val r'))).range ≤
    (Localization.awayMapₐ (adjoin R t).val r').range
x : S
n : ℕ
y : Localization.Away r'
hy :
  (Localization.awayMap (adjoin R t).val.toRingHom r') y =
    (IsScalarTower.toAlgHom R S (Localization.Away ((adjoin R t).val r'))).toRingHom x
⊢ (IsScalarTower.toAlgHom R S (Localization.Away ((adjoin R t).val r'))).toRingHom x *
      (Localization.awayMap (adjoin R t).val.toRingHom r') (Localization.Away.invSelf r') ^ n =
    IsLocalization.mk' (Localization.Away ((adjoin R t).val.toRingHom r')) x ⟨(adjoin R t).val.toRingHom r' ^ n, ⋯⟩
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg0 : ¬g = 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (f g : R[X]) (n : ℕ),
    g.natDegree ≤ n →
      f.Splits →
        IsField R →
          f.Monic → ¬g = 0 → g.Monic → f.resultant g f.natDegree n = (Multiset.map (fun x ↦ eval x g) f.roots).prod
hgm : ¬g.Monic
inst : Field R := hR.toField
⊢ f.resultant g f.natDegree n = (Multiset.map (fun x ↦ eval x g) f.roots).prod

Tactic:
have := this f (C g.leadingCoeff⁻¹ * g) n (by simpa [hg0, natDegree_C_mul]) hf hR hfm (by simpa)
      (by rw [Monic, ← coeff_natDegree, natDegree_C_mul (by simp [hg0]), coeff_C_mul]; simp [hg0])

Goal state after:
case neg.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg0 : ¬g = 0
this✝ :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (f g : R[X]) (n : ℕ),
    g.natDegree ≤ n →
      f.Splits →
        IsField R →
          f.Monic → ¬g = 0 → g.Monic → f.resultant g f.natDegree n = (Multiset.map (fun x ↦ eval x g) f.roots).prod
hgm : ¬g.Monic
inst : Field R := hR.toField
this :
  f.resultant (C g.leadingCoeff⁻¹ * g) f.natDegree n =
    (Multiset.map (fun x ↦ eval x (C g.leadingCoeff⁻¹ * g)) f.roots).prod
⊢ f.resultant g f.natDegree n = (Multiset.map (fun x ↦ eval x g) f.roots).prod
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr.e_a
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
h✝ : Nontrivial R
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
⊢ (aeval (universalFactorizationMapPresentation R n m k hn).val)
      ((Polynomial.map (↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inl)))
            (freeMonic R m)).resultant
        (Polynomial.map (↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inr)))
          (freeMonic R k))
        m k) =
    (Polynomial.map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m)).resultant
      (Polynomial.map (↑Algebra.TensorProduct.includeRight) (freeMonic R k))

Tactic:
rw [← (aeval _).coe_toRingHom, ← Polynomial.resultant_map_map,
    Polynomial.map_map, Polynomial.map_map]

Goal state after:
case inr.e_a
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
h✝ : Nontrivial R
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
⊢ (Polynomial.map
          ((↑(aeval (universalFactorizationMapPresentation R n m k hn).val)).comp
            ↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inl)))
          (freeMonic R m)).resultant
      (Polynomial.map
        ((↑(aeval (universalFactorizationMapPresentation R n m k hn).val)).comp
          ↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inr)))
        (freeMonic R k))
      m k =
    (Polynomial.map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m)).resultant
      (Polynomial.map (↑Algebra.TensorProduct.includeRight) (freeMonic R k))
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FiniteType R S
p : Ideal R
inst✝³ : p.IsPrime
q✝ : Ideal S
inst✝² : q✝.IsPrime
inst✝¹ : q✝.LiesOver p
inst✝ : QuasiFiniteAt R q✝
s : S
hsq : s ∉ q✝
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q✝ → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (q' : Ideal ↥(integralClosure R S)),
    q'.IsPrime → q' ≠ Ideal.under (↥(integralClosure R S)) q✝ → q'.LiesOver p → ⟨s, hRs⟩ ∈ q'
f : R[X] := X * minpoly R s
q : p.ResidueField[X]
hq :
  Polynomial.map (algebraMap R p.ResidueField) (minpoly R s) =
    (X - C 0) ^ rootMultiplicity 0 (Polynomial.map (algebraMap R p.ResidueField) (minpoly R s)) * q
hq' : ¬X - C 0 ∣ q
⊢ ∃ m f b,
    f.Monic ∧
      b.Monic ∧
        IsCoprime (X ^ (m + 1)) b ∧ Polynomial.map (algebraMap R p.ResidueField) f = X ^ (m + 1) * b ∧ (aeval s) f = 0

Tactic:
have hqm : q.Monic := by
      simpa [((minpoly.monic hRs).map _).leadingCoeff] using! congr(leadingCoeff $hq).symm

Goal state after:
R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FiniteType R S
p : Ideal R
inst✝³ : p.IsPrime
q✝ : Ideal S
inst✝² : q✝.IsPrime
inst✝¹ : q✝.LiesOver p
inst✝ : QuasiFiniteAt R q✝
s : S
hsq : s ∉ q✝
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q✝ → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (q' : Ideal ↥(integralClosure R S)),
    q'.IsPrime → q' ≠ Ideal.under (↥(integralClosure R S)) q✝ → q'.LiesOver p → ⟨s, hRs⟩ ∈ q'
f : R[X] := X * minpoly R s
q : p.ResidueField[X]
hq :
  Polynomial.map (algebraMap R p.ResidueField) (minpoly R s) =
    (X - C 0) ^ rootMultiplicity 0 (Polynomial.map (algebraMap R p.ResidueField) (minpoly R s)) * q
hq' : ¬X - C 0 ∣ q
hqm : q.Monic
⊢ ∃ m f b,
    f.Monic ∧
      b.Monic ∧
        IsCoprime (X ^ (m + 1)) b ∧ Polynomial.map (algebraMap R p.ResidueField) f = X ^ (m + 1) * b ∧ (aeval s) f = 0
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
x : ↥X
hx : QuasiFiniteAt f x
T : Scheme
fT : T ⟶ Y
left✝¹ : Etale fT
u : ↥T
hu : fT u = f x
V W : (pullback f fT).Opens
v : ↥V
hVW : IsCompl V W
left✝ : IsFinite (V.ι ≫ pullback.snd f fT)
hv₂ : (pullback.fst f fT) ↑v = x
U : (normalization (pullback.snd f fT)).Opens
hU : (toNormalization (pullback.snd f fT)) ↑v ∈ U
right✝ : IsIso (toNormalization (pullback.snd f fT) ∣_ U)
fTn : normalization (pullback.snd f fT) ⟶ normalization f :=
  normalizationPullback f fT ≫ pullback.fst (fromNormalization f) fT
U' : (normalization f).Opens := { carrier := ⇑fTn '' U.carrier, is_open' := ⋯ }
fTnU : ↑U ⟶ ↑U' := resLE fTn U' U ⋯
this : Surjective fTnU
H : toNormalization (pullback.snd f fT) ⁻¹ᵁ U ≤ pullback.fst f fT ⁻¹ᵁ toNormalization f ⁻¹ᵁ U'
⊢ IsPullback
    (pullback.map f fT (fromNormalization f) fT (toNormalization f) (𝟙 T) (𝟙 Y) ⋯ ⋯ ≫
      pullback.snd (fromNormalization f) fT)
    (pullback.fst f fT) fT (toNormalization f ≫ fromNormalization f)

Tactic:
simpa using (.flip <| .of_hasPullback ..)

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: case refine_1
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
x : ↥X
hx : QuasiFiniteAt f x
T : Scheme
fT : T ⟶ Y
left✝¹ : Etale fT
u : ↥T
hu : fT u = f x
V W : (pullback f fT).Opens
v : ↥V
hVW : IsCompl V W
left✝ : IsFinite (V.ι ≫ pullback.snd f fT)
hv₂ : (pullback.fst f fT) ↑v = x
U : (normalization (pullback.snd f fT)).Opens
hU : (toNormalization (pullback.snd f fT)) ↑v ∈ U
right✝ : IsIso (toNormalization (pullback.snd f fT) ∣_ U)
fTn : normalization (pullback.snd f fT) ⟶ normalization f :=
  normalizationPullback f fT ≫ pullback.fst (fromNormalization f) fT
U' : (normalization f).Opens := { carrier := ⇑fTn '' U.carrier, is_open' := ⋯ }
fTnU : ↑U ⟶ ↑U' := resLE fTn U' U ⋯
this : Surjective fTnU
H✝ : toNormalization (pullback.snd f fT) ⁻¹ᵁ U ≤ pullback.fst f fT ⁻¹ᵁ toNormalization f ⁻¹ᵁ U'
H :
  IsPullback (pullback.map f fT (fromNormalization f) fT (toNormalization f) (𝟙 T) (𝟙 Y) ⋯ ⋯) (pullback.fst f fT)
    (pullback.fst (fromNormalization f) fT) (toNormalization f)
⊢ IsPullback (toNormalization (pullback.snd f fT)) (pullback.fst f fT) fTn (toNormalization f)

Tactic:
exact .of_iso' H (.refl _) (asIso <| f.normalizationPullback fT) (.refl _) (.refl _)
        (by cat_disch) (by simp) (by simp [fTn]) (by simp)

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Descent

Goal state before:
pp: case h
R : Type u_1
inst✝⁶ : CommRing R
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : FaithfullyFlat R T
inst✝ : Module.Finite T (T ⊗[R] M)
n : ℕ
s : Fin n → T ⊗[R] M
hs : Submodule.span T (Set.range s) = ⊤
k : Fin n → ℕ
t : (i : Fin n) → Fin (k i) → T
m : (i : Fin n) → Fin (k i) → M
h : ∀ (i : Fin n), s i = ∑ j, t i j ⊗ₜ[R] m i j
f₀ : ((i : Fin n) × Fin (k i) → R) →ₗ[R] M := ⋯
i : Fin n
⊢ ((AlgebraTensorModule.lTensor T T) f₀) (∑ j, t i j ⊗ₜ[R] (Pi.basisFun R ((i : Fin n) × Fin (k i))) ⟨i, j⟩) = s i

Tactic:
simp [f₀, -Pi.basisFun_equivFun, -Pi.basisFun_apply, h i]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f], IsAffineHom f → IsOpen {x | QuasiFiniteAt f x}
H : ¬IsAffineHom f
x : ↥X
hx : x ∈ {x | QuasiFiniteAt f x}
U : Y.Opens
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : X.Opens
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ (f ⁻¹ᵁ U).carrier
⊢ ∃ t ⊆ {x | QuasiFiniteAt f x}, IsOpen t ∧ x ∈ t

Tactic:
have inst : IsAffineHom (f.resLE U V hVU) :=
      have : IsAffine _ := hU
      have : IsAffine _ := hV
      isAffineHom_of_isAffine _

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f], IsAffineHom f → IsOpen {x | QuasiFiniteAt f x}
H : ¬IsAffineHom f
x : ↥X
hx : x ∈ {x | QuasiFiniteAt f x}
U : Y.Opens
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : X.Opens
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ (f ⁻¹ᵁ U).carrier
inst : IsAffineHom (resLE f U V hVU)
⊢ ∃ t ⊆ {x | QuasiFiniteAt f x}, IsOpen t ∧ x ∈ t
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X✝ Y✝ S✝ : Scheme
f✝ : X✝ ⟶ S✝
inst✝¹ : LocallyOfFiniteType f✝
X Y S : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
⊢ Scheme.Hom.quasiFiniteLocus ((Scheme.Hom.quasiFiniteLocus f).ι ≫ f) = ⊤

Tactic:
Scheme.Hom.quasiFiniteLocus_comp,

Goal state after:
X✝ Y✝ S✝ : Scheme
f✝ : X✝ ⟶ S✝
inst✝¹ : LocallyOfFiniteType f✝
X Y S : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
⊢ (Scheme.Hom.quasiFiniteLocus f).ι ⁻¹ᵁ Scheme.Hom.quasiFiniteLocus f = ⊤
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
β : r ≫ g ⟶ h
⊢ 𝟙 (r ≫ g) ⊗≫ rightZigzag adj.unit adj.counit ▷ g ⊗≫ β = β

Tactic:
rw [adj.right_triangle]
        bicategory

Goal state after: