mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: case h₂
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : (algebraMap R T).IsStandardSmooth
⊢ (algebraMap S (S ⊗[R] T)).IsStandardSmooth

Tactic:
replace h : Algebra.IsStandardSmooth R T := by
      rw [RingHom.IsStandardSmooth] at h; convert! h; ext; simp_rw [Algebra.smul_def]; rfl

Goal state after:
case h₂
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmooth R T
⊢ (algebraMap S (S ⊗[R] T)).IsStandardSmooth
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
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
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 • σ' ↑σ
ι : Type u_3
x✝ : Fintype ι
v : ι → K
hv : LinearIndependent k v
⊢ LinearIndependent k fun x ↦ v x ^ p

Tactic:
simpa only [Finset.coe_image, Finset.coe_univ, Set.image_univ, linearIndepOn_range_iff
      hv.injective] using! H (Finset.univ.image v) (by simpa using! hv.linearIndepOn_id)

Goal state after:
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
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
n : ι
inst✝ : ExpChar k p
ha : adjoin k (Set.range a) = ⊤
ha' : IsTranscendenceBasis k fun i ↦ a ↑i
i : ι
hi : (IsTranscendenceBasis k fun j ↦ a ↑j) ∧ IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
⊢ Set.range a ⊆ ↑(restrictScalars k (separableClosure (↥(adjoin k (a '' {i}ᶜ))) K))

Tactic:
rintro _ ⟨x, rfl⟩

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
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
n : ι
inst✝ : ExpChar k p
ha : adjoin k (Set.range a) = ⊤
ha' : IsTranscendenceBasis k fun i ↦ a ↑i
i : ι
hi : (IsTranscendenceBasis k fun j ↦ a ↑j) ∧ IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
x : ι
⊢ a x ∈ ↑(restrictScalars k (separableClosure (↥(adjoin k (a '' {i}ᶜ))) K))
Module: Mathlib.RingTheory.RingHom.QuasiFinite

Goal state before:
pp: R S : Type u_6
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
H : ∀ (r : ↥s), (fun {R S} [CommRing R] [CommRing S] ↦ QuasiFinite) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
P : Ideal R
x✝ : P.IsPrime
⊢ Module.Finite P.ResidueField (P.Fiber S)

Tactic:
have (r : s) : Module.Finite P.ResidueField (P.Fiber (Localization.Away r.1)) := by
    have : Algebra.QuasiFinite R (Localization.Away r.1) := quasiFinite_algebraMap.mp (H r)
    infer_instance

Goal state after:
R S : Type u_6
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
H : ∀ (r : ↥s), (fun {R S} [CommRing R] [CommRing S] ↦ QuasiFinite) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
P : Ideal R
x✝ : P.IsPrime
this : ∀ (r : ↥s), Module.Finite P.ResidueField (P.Fiber (Localization.Away ↑r))
⊢ Module.Finite P.ResidueField (P.Fiber S)
Module: Mathlib.FieldTheory.RatFunc.Defs

Goal state before:
pp: case neg
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
P : Sort v
p q : K[X]
f : K[X] → K[X] → P
f0 : ∀ (p : K[X]), f p 0 = f 0 1
H' : ∀ {p q p' q' : K[X]}, q ≠ 0 → q' ≠ 0 → q' * p = q * p' → f p q = f p' q'
H : ∀ {p q p' q' : K[X]}, q ∈ K[X]⁰ → q' ∈ K[X]⁰ → q' * p = q * p' → f p q = f p' q'
hq : ¬q = 0
⊢ (RatFunc.mk p q).liftOn f H = f p q

Tactic:
· simp only [mk_eq_localization_mk _ hq, liftOn_ofFractionRing_mk]

Goal state after:
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: case refine_2
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)
f : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I →+* S ⧸ Ideal.map (algebraMap R S) I :=
  Ideal.Quotient.lift (Ideal.map (algebraMap R ↥R[x]) I)
    ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) ⋯
y : S ⧸ Ideal.map (algebraMap R S) I
z : S
hz : (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) z = y
this : ∃ x_1 ∈ conductor R x, (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) x_1 = y
⊢ ∃ a, ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) a = y

Tactic:
obtain ⟨u, hu, hu'⟩ := this
      use ⟨u, conductor_subset_adjoin hu⟩
      simp only [← hu']
      rfl

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

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p q : K[X]
⊢ RatFunc.mk p q = (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q

Tactic:
by
  simp only [mk_eq_div', ofFractionRing_div, ofFractionRing_algebraMap]

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

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
⊢ (algebraMap K[X] K⟮X⟯) x.num / (algebraMap K[X] K⟮X⟯) x.denom = x

Tactic:
by
  classical
  induction x using RatFunc.induction_on with | _ p q hq
  have q_div_ne_zero : q / gcd p q ≠ 0 := right_div_gcd_ne_zero hq
  rw [num_div p q, denom_div p hq, map_mul, map_mul, mul_div_mul_left,
    div_eq_div_iff, ← map_mul, ← map_mul, mul_comm _ q, ←
    EuclideanDomain.mul_div_assoc, ← EuclideanDomain.mul_div_assoc, mul_comm]
  · apply gcd_dvd_right
  · apply gcd_dvd_left
  · exact algebraMap_ne_zero q_div_ne_zero
  · exact algebraMap_ne_zero hq
  · refine algebraMap_ne_zero (mt Polynomial.C_eq_zero.mp ?_)
    exact inv_ne_zero (Polynomial.leadingCoeff_ne_zero.mpr q_div_ne_zero)

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
s : Set S
hs : Ideal.span s = ⊤
Sᵣ : ↑s → Type u_4
inst✝⁴ : (r : ↑s) → CommRing (Sᵣ r)
inst✝³ : (r : ↑s) → Algebra S (Sᵣ r)
inst✝² : (r : ↑s) → Algebra R (Sᵣ r)
inst✝¹ : ∀ (r : ↑s), IsScalarTower R S (Sᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Sᵣ r)
H : ∀ (r : ↑s), Function.Bijective ⇑(toIntegralClosure R (Sᵣ r) B)
this :
  ∀ (r : ↑s),
    IsLocalizedModule.Away (↑r)
      (Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R ↥(integralClosure R B))).toLinearMap
r : ↑s
⊢ ∀ (x : ↥(integralClosure S (S ⊗[R] B))),
    ((Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R B)).comp (integralClosure S (S ⊗[R] B)).val) x ∈
      Subalgebra.restrictScalars S (integralClosure (Sᵣ r) (Sᵣ r ⊗[R] B))

Tactic:
simp only [AlgHom.coe_comp, Subalgebra.coe_val, Function.comp_apply,
      Subalgebra.mem_restrictScalars, Subtype.forall, mem_integralClosure_iff]

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
s : Set S
hs : Ideal.span s = ⊤
Sᵣ : ↑s → Type u_4
inst✝⁴ : (r : ↑s) → CommRing (Sᵣ r)
inst✝³ : (r : ↑s) → Algebra S (Sᵣ r)
inst✝² : (r : ↑s) → Algebra R (Sᵣ r)
inst✝¹ : ∀ (r : ↑s), IsScalarTower R S (Sᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Sᵣ r)
H : ∀ (r : ↑s), Function.Bijective ⇑(toIntegralClosure R (Sᵣ r) B)
this :
  ∀ (r : ↑s),
    IsLocalizedModule.Away (↑r)
      (Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R ↥(integralClosure R B))).toLinearMap
r : ↑s
⊢ ∀ (a : S ⊗[R] B),
    IsIntegral S a → IsIntegral (Sᵣ r) ((Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R B)) a)
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
inst✝ : Algebra.IsStandardEtale R S
𝓟 : StandardEtalePresentation R S
n : ℕ
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := ⋯
e : B ⊗[R] S ≃ₐ[B] Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g) := ⋯
a : AdjoinRoot 𝓟'.f
m : ℕ
hx✝ :
  IsIntegral S
    ((Algebra.TensorProduct.comm R B S)
      (e.symm
        (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
          ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
hx :
  ∀ (m_1 : ℕ),
    IsIntegral R
      ((aeval 𝓟.x) 𝓟.g ^ (n + m_1) •
        (Algebra.TensorProduct.comm R B S)
          (e.symm
            (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
              ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
hfg : IsIntegral R ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)
g : R[X]
⊢ e ((aeval (1 ⊗ₜ[R] 𝓟.x)) (Polynomial.map (algebraMap R B) g)) =
    (algebraMap (AdjoinRoot 𝓟'.f) (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)))
      ((AdjoinRoot.mk 𝓟'.f) (Polynomial.map (algebraMap R B) g))

Tactic:
rw [← e.eq_symm_apply]

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
inst✝ : Algebra.IsStandardEtale R S
𝓟 : StandardEtalePresentation R S
n : ℕ
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := 𝓟.baseChange
e : B ⊗[R] S ≃ₐ[B] Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g) := 𝓟'.equivRing.trans 𝓟'.equivAwayAdjoinRoot
a : AdjoinRoot 𝓟'.f
m : ℕ
hx✝ :
  IsIntegral S
    ((Algebra.TensorProduct.comm R B S)
      (e.symm
        (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
          ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
hx :
  ∀ (m_1 : ℕ),
    IsIntegral R
      ((aeval 𝓟.x) 𝓟.g ^ (n + m_1) •
        (Algebra.TensorProduct.comm R B S)
          (e.symm
            (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
              ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
hfg : IsIntegral R ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)
g : R[X]
⊢ (aeval (1 ⊗ₜ[R] 𝓟.x)) (Polynomial.map (algebraMap R B) g) =
    e.symm
      ((algebraMap (AdjoinRoot 𝓟'.f) (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)))
        ((AdjoinRoot.mk 𝓟'.f) (Polynomial.map (algebraMap R B) g)))
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
inst✝² : IsReduced S
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
left✝ : IsDomain S
right✝ : FaithfulSMul R S
this✝ : IsDomain R
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
R' : Subalgebra R K := integralClosure R K
S' : Subalgebra (↥R') L := adjoin ↥R' ↑(algebraMap S L).range
f : S →ₐ[R] ↥S' := (IsScalarTower.toAlgHom R S L).codRestrict (Subalgebra.restrictScalars R S') ⋯
g : ↥R' ⊗[R] S →ₐ[↥R'] ↥S' := TensorProduct.lift (ofId ↥R' ↥S') f ⋯
⊢ Subalgebra.map S'.val g.range = S'.val.range

Tactic:
refine le_antisymm (Set.image_subset_range S'.val g.range) ?_

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsReduced S
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
left✝ : IsDomain S
right✝ : FaithfulSMul R S
this✝ : IsDomain R
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
R' : Subalgebra R K := integralClosure R K
S' : Subalgebra (↥R') L := adjoin ↥R' ↑(algebraMap S L).range
f : S →ₐ[R] ↥S' := (IsScalarTower.toAlgHom R S L).codRestrict (Subalgebra.restrictScalars R S') ⋯
g : ↥R' ⊗[R] S →ₐ[↥R'] ↥S' := TensorProduct.lift (ofId ↥R' ↥S') f ⋯
⊢ S'.val.range ≤ Subalgebra.map S'.val g.range
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h✝² : j = f.natDegree - 2
h✝¹ : ¬j < f.natDegree - 1
h✝ : j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2
⊢ f.coeff f.natDegree =
    f.coeff (2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1) * (↑(2 * f.natDegree - 2 - (j - (f.natDegree - 1))) + 1)

Tactic:
rw [← Nat.cast_one (R := R), ← Nat.cast_add, show f.natDegree = 1 by lia]
      norm_num

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
inst✝ : Algebra.Smooth R S
⊢ Function.Bijective ⇑(toIntegralClosure R S B)

Tactic:
have (m : PrimeSpectrum S) : ∃ f ∉ m.asIdeal,
      Function.Bijective (toIntegralClosure R (Localization.Away f) B) := by
    obtain ⟨f, hfm, n, _, _, _⟩ :=
      Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial (R := R) (p := m.asIdeal)
    exact ⟨f, hfm, toIntegralClosure_bijective_of_tower (S := MvPolynomial (Fin n) R)
      toIntegralClosure_mvPolynomial_bijective toIntegralClosure_bijective_of_isStandardEtale⟩

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
inst✝ : Algebra.Smooth R S
this : ∀ (m : PrimeSpectrum S), ∃ f ∉ m.asIdeal, Function.Bijective ⇑(toIntegralClosure R (Localization.Away f) B)
⊢ Function.Bijective ⇑(toIntegralClosure R S B)
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
this : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
⊢ toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ ↑U = f ⁻¹ᵁ ↑U

Tactic:
simp [← Scheme.Hom.comp_preimage]

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.affineOpens
this : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
⊢ toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ ↑U =
    (f ⁻¹ᵁ ↑U).ι ''ᵁ ((f ⁻¹ᵁ ↑U).ι ≫ toNormalization f) ⁻¹ᵁ fromNormalization f ⁻¹ᵁ ↑U

Tactic:
simp [← Scheme.Hom.comp_preimage]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
m : ℕ
r : R
hf : f.natDegree ≤ m
⊢ f.resultant (X + C r) m 1 = (-1) ^ m * eval (-r) f

Tactic:
← resultant_X_sub_C_right f m (-r) hf,

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R[X]
m : ℕ
r : R
hf : f.natDegree ≤ m
⊢ f.resultant (X + C r) m 1 = f.resultant (X - C (-r)) m 1
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
this : Algebra ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (app f U)).toAlgebra
⊢ f ⁻¹ᵁ U ≤ toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ U

Tactic:
simp [← Scheme.Hom.comp_preimage]

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

Goal state before:
pp: case neg
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
H : ¬g.natDegree = 0
⊢ 0 ^ g.natDegree * g.coeff 0 ^ (g * r).natDegree =
    (Multiset.map (fun ij ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots)).prod

Tactic:
simp only [zero_pow H]
        rw [hg'.natDegree_eq_card_roots, Multiset.card_eq_zero,
          Multiset.eq_zero_iff_forall_notMem, not_forall_not] at H
        obtain ⟨x, hx⟩ := H
        rw [Multiset.prod_eq_zero, zero_mul]
        simp only [Multiset.mem_map, Prod.exists]
        exact ⟨x, x, Multiset.mem_product.mpr (by simp_all [hg.ne_zero]), by simp⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst✝ : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U : (normalizationOpenCover f).I₀
this✝¹ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝ : IsAffineHom f₁
this : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
⊢ f ⁻¹ᵁ ↑U ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ ↑U

Tactic:
simp only [← Scheme.Hom.comp_preimage, f₀, Category.assoc,
        hf₁, toNormalization_fromNormalization]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst✝ : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U : (normalizationOpenCover f).I₀
this✝¹ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝ : IsAffineHom f₁
this : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
⊢ f ⁻¹ᵁ ↑U ≤ f ⁻¹ᵁ ↑U
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst✝ : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U : (normalizationOpenCover f).I₀
this✝¹ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝ : IsAffineHom f₁
this : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
h₁ : f ⁻¹ᵁ ↑U ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₁' : f ⁻¹ᵁ ↑U = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₂ : fromNormalization f ⁻¹ᵁ ↑U = f₁ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₂' : fromNormalization f ⁻¹ᵁ ↑U = f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U
⊢ f ⁻¹ᵁ ↑U = toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ ↑U

Tactic:
simp [← Scheme.Hom.comp_preimage]

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

Goal state before:
pp: case neg.inr
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hf' : f.Splits
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : ¬g.natDegree = 0
hr : r ≠ 0
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g

Tactic:
conv_lhs => rw [← natDegree_scaleRoots f r, ← natDegree_scaleRoots g r]

Goal state after:
case neg.inr
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hf' : f.Splits
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : ¬g.natDegree = 0
hr : r ≠ 0
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) (f.scaleRoots r).natDegree =
    r ^ (f.natDegree * g.natDegree) * f.resultant g
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
P : Ideal R
inst✝ : P.IsPrime
p : R[X]
f g : P.ResidueField[X]
hp : p.Monic
hf : f.Monic
hg : g.Monic
H : map (algebraMap R P.ResidueField) p = f * g
Hpq : IsCoprime f g
⊢ p.natDegree = f.natDegree + g.natDegree

Tactic:
by simpa [hf.natDegree_mul hg, hp.natDegree_map] using congr(($H).natDegree)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝¹⁰ : Nonempty ↥G.left
this✝⁹ : IsProper (G ⊗ G).hom
this✝⁸ : JacobsonSpace ↥(G ⊗ G).left
this✝⁷ : Surjective G.hom
this✝⁶ : IsProper (Over.Hom.left (fst G G))
this✝⁵ : Surjective (Over.Hom.left (fst G G))
this✝⁴ : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this✝³ : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝² : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝¹ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this✝ : IsProper (Over.Hom.left γ)
H✝ : ⇑(Over.Hom.left γ) '' ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} ⊆ {(Over.Hom.left (lift η η)) point}
U : G.left.Opens
hηU : (Over.Hom.left η) point ∈ U
H : IsFinite ((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U)
x : ↥U
this : ⇑U.ι ⁻¹' {↑x} = {x}
⊢ ⇑(pullback.fst G.hom G.hom) ⁻¹' {↑x} ∩ Set.range ⇑(Over.Hom.left γ) ⊆
    ⇑(((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ⁻¹ᵁ U).ι ≫
          Scheme.Hom.imageι (Over.Hom.left γ)) ''
      ⇑(Over.Hom.left (fst G G)) ∘
          ⇑(((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ⁻¹ᵁ U).ι ≫
              Scheme.Hom.imageι (Over.Hom.left γ)) ⁻¹'
        {↑x}

Tactic:
Set.preimage_comp,

Goal state after:
K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝¹⁰ : Nonempty ↥G.left
this✝⁹ : IsProper (G ⊗ G).hom
this✝⁸ : JacobsonSpace ↥(G ⊗ G).left
this✝⁷ : Surjective G.hom
this✝⁶ : IsProper (Over.Hom.left (fst G G))
this✝⁵ : Surjective (Over.Hom.left (fst G G))
this✝⁴ : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this✝³ : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝² : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝¹ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this✝ : IsProper (Over.Hom.left γ)
H✝ : ⇑(Over.Hom.left γ) '' ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} ⊆ {(Over.Hom.left (lift η η)) point}
U : G.left.Opens
hηU : (Over.Hom.left η) point ∈ U
H : IsFinite ((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U)
x : ↥U
this : ⇑U.ι ⁻¹' {↑x} = {x}
⊢ ⇑(pullback.fst G.hom G.hom) ⁻¹' {↑x} ∩ Set.range ⇑(Over.Hom.left γ) ⊆
    ⇑(((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ⁻¹ᵁ U).ι ≫
          Scheme.Hom.imageι (Over.Hom.left γ)) ''
      ⇑(((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ⁻¹ᵁ U).ι ≫
            Scheme.Hom.imageι (Over.Hom.left γ)) ⁻¹'
        ⇑(Over.Hom.left (fst G G)) ⁻¹' {↑x}
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: case zero
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Extension R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
t : T
⊢ 0 = t • (CotangentSpace.map (toBaseChange T)) 0

Tactic:
LinearMap.map_zero,

Goal state after:
case zero
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Extension R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
t : T
⊢ 0 = t • 0
Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g : a ⟶ c
h i : b ⟶ c
j : a ⟶ c
k : c ⟶ d
α : g ≅ f ≫ h
η : h ⟶ i
ηs : f ≫ i ⟶ j
η₁ : h ≫ k ⟶ i ≫ k
η₂ : f ≫ h ≫ k ⟶ f ≫ i ≫ k
ηs₁ : (f ≫ i) ≫ k ⟶ j ≫ k
ηs₂ : f ≫ i ≫ k ⟶ j ≫ k
η₃ : f ≫ h ≫ k ⟶ j ≫ k
η₄ : (f ≫ h) ≫ k ⟶ j ≫ k
η₅ : g ≫ k ⟶ j ≫ k
e_η₁ : ((Iso.refl h).hom ≫ η ≫ (Iso.refl i).hom) ▷ k = η₁
e_η₂ : f ◁ η₁ = η₂
e_ηs₁ : ηs ▷ k = ηs₁
e_ηs₂ : (α_ f i k).inv ≫ ηs₁ = ηs₂
e_η₃ : η₂ ≫ ηs₂ = η₃
e_η₄ : (α_ f h k).hom ≫ η₃ = η₄
e_η₅ : (α ▷ᵢ k).hom ≫ η₄ = η₅
⊢ (α.hom ≫ f ◁ η ≫ ηs) ▷ k = η₅

Tactic:
simp at e_η₁ e_η₅
  simp [e_η₁, e_η₂, e_ηs₁, e_ηs₂, e_η₃, e_η₄, e_η₅]

Goal state after: