mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝² : Module.Finite R S
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt R Q
h✝ : Nontrivial S
this✝ : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra (Localization.AtPrime P) (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : R[x] = ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (aeval x).toRingHom
hx' : Function.Surjective ⇑(aeval x)
p : R[X]
hpI : p ∈ I
hp :
  Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I
hI' : Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I = RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom
m : P.ResidueField[X] := minpoly P.ResidueField ((algebraMap S Q.ResidueField) x)
hm : Prime m
hmp₁ : m ∣ Polynomial.map (algebraMap R P.ResidueField) p
hmp₂ : ¬m ^ 2 ∣ Polynomial.map (algebraMap R P.ResidueField) p
q : R[X] := minpoly R x ^ (p.natDegree + 2) + p
⊢ (minpoly R x).leadingCoeff ^ (p.natDegree + 2) ≠ 0

Tactic:
by simp [minpoly.monic hRx]

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.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 (1 ⊗ₜ[R] (aeval 𝓟.x) g) = e ((aeval (1 ⊗ₜ[R] 𝓟.x)) (Polynomial.map (algebraMap R B) g))

Tactic:
← Algebra.TensorProduct.includeRight_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]
⊢ e (Algebra.TensorProduct.includeRight ((aeval 𝓟.x) g)) = e ((aeval (1 ⊗ₜ[R] 𝓟.x)) (Polynomial.map (algebraMap R B) g))
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℕ
i : Fin m
⊢ ((fun x ↦ (x, 0)) ∘ ⇑(basis R m)) i = ((basis R m) i, 0)

Tactic:
Function.comp_apply

Goal state after:
R : Type u_1
inst✝ : Semiring R
m n : ℕ
i : Fin m
⊢ ((basis R m) i, 0) = ((basis R m) i, 0)
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℕ
i : Fin n
⊢ (Prod.mk 0 ∘ ⇑(basis R n)) i = (0, (basis R n) i)

Tactic:
Function.comp_apply

Goal state after:
R : Type u_1
inst✝ : Semiring R
m n : ℕ
i : Fin n
⊢ (0, (basis R n) i) = (0, (basis R n) i)
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
V : Y.Opensᵒᵖ
x : ↑Γ(X, f ⁻¹ᵁ Opposite.unop V)
hx : x ∈ integralClosure ↑Γ(Y, Opposite.unop V) ↑Γ(X, f ⁻¹ᵁ Opposite.unop V)
U : Y.Opens
i : V ⟶ Opposite.op U
⊢ (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) x ∈
    integralClosure ↑Γ(Y, Opposite.unop (Opposite.op U)) ↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U))

Tactic:
obtain ⟨V, rfl⟩ := Opposite.op_surjective V

Goal state after:
X Y : Scheme
f : X ⟶ Y
U V : Y.Opens
x : ↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V))
hx : x ∈ integralClosure ↑Γ(Y, Opposite.unop (Opposite.op V)) ↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V))
i : Opposite.op V ⟶ Opposite.op U
⊢ (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) x ∈
    integralClosure ↑Γ(Y, Opposite.unop (Opposite.op U)) ↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U))
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
i : ℕ
hi : i < f.natDegree - 1 + f.natDegree
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
⊢ f.sylvesterDeriv.updateRow ⟨2 * f.natDegree - 2, ⋯⟩ (f.leadingCoeff • f.sylvesterDeriv ⟨2 * f.natDegree - 2, ⋯⟩)
      ⟨i, hi⟩ ⟨j, hj⟩ =
    (derivative f).sylvester f (f.natDegree - 1) f.natDegree ⟨i, hi⟩ ⟨j, hj⟩

Tactic:
sylvesterDeriv,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
i : ℕ
hi : i < f.natDegree - 1 + f.natDegree
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
⊢ (if hn : f.natDegree = 0 then 0
        else
          ((derivative f).sylvester f (f.natDegree - 1) f.natDegree).updateRow ⟨2 * f.natDegree - 2, ⋯⟩ fun j ↦
            if ↑j = f.natDegree - 2 then 1 else if ↑j = 2 * f.natDegree - 2 then ↑f.natDegree else 0).updateRow
      ⟨2 * f.natDegree - 2, ⋯⟩
      (f.leadingCoeff •
        (if hn : f.natDegree = 0 then 0
          else
            ((derivative f).sylvester f (f.natDegree - 1) f.natDegree).updateRow ⟨2 * f.natDegree - 2, ⋯⟩ fun j ↦
              if ↑j = f.natDegree - 2 then 1 else if ↑j = 2 * f.natDegree - 2 then ↑f.natDegree else 0)
          ⟨2 * f.natDegree - 2, ⋯⟩)
      ⟨i, hi⟩ ⟨j, hj⟩ =
    (derivative f).sylvester f (f.natDegree - 1) f.natDegree ⟨i, hi⟩ ⟨j, hj⟩
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
r : R
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (C r * g) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
i : ℕ
IH : i ≤ m → (M i).det = r ^ i * M₂.det
hi : i + 1 ≤ m
this : (M i).updateCol ⟨i, ⋯⟩ (r • fun j ↦ M i j ⟨i, ⋯⟩) = M (i + 1)
⊢ r * ((M i).updateCol ⟨i, ⋯⟩ fun j ↦ M i j ⟨i, ⋯⟩).det = r * (M i).det

Tactic:
Matrix.updateCol_eq_self

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
r : R
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (C r * g) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
i : ℕ
IH : i ≤ m → (M i).det = r ^ i * M₂.det
hi : i + 1 ≤ m
this : (M i).updateCol ⟨i, ⋯⟩ (r • fun j ↦ M i j ⟨i, ⋯⟩) = M (i + 1)
⊢ r * (M i).det = r * (M i).det
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 : ℕ
⊢ f.sylvester g (m + 1) (n + 1) (Fin.last (m + 1 + n)) (Fin.castAdd (n + 1) (Fin.last m)) = g.coeff (n + 1)

Tactic:
simp only [sylvester, Set.mem_Icc, Matrix.of_apply, Fin.val_last, Fin.addCases_left]
      rw [if_pos (by lia)]
      simp [add_assoc, add_comm 1]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
m n : ℕ
r : R
⊢ f.resultant (C r) m n = f.coeff m ^ n * r ^ m

Tactic:
rw [← zero_add n, resultant_add_right_deg _ _ _ _ _ (by simp)]

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R[X]
m n : ℕ
r : R
⊢ f.coeff m ^ n * f.resultant (C r) m 0 = f.coeff m ^ (0 + n) * r ^ m
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
inst✝⁴ : QuasiCompact f✝
inst✝³ : QuasiSeparated f✝
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : Smooth g
x : ↥(pullback (fromNormalization f) g)
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : (pullback.snd (fromNormalization f) g ≫ g) x ∈ ↑U
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : (pullback.snd (fromNormalization f) g) x ∈ ↑V
hVU : V ≤ g ⁻¹ᵁ U
W : (pullback (fromNormalization f) g).Opens := pullback.snd (fromNormalization f) g ⁻¹ᵁ V
⊢ IsIso (app (normalizationPullback f g) W)

Tactic:
have := isIso_pushoutSection_of_isQuasiSeparated_of_flat_right
    (.of_hasPullback f.fromNormalization g) hVU le_rfl (UY := W)
    (by simp_rw [W, ← Scheme.Hom.comp_preimage, pullback.condition, Scheme.Hom.comp_preimage,
      ← Scheme.Hom.preimage_inf, inf_eq_right.mpr hVU]) hU hV
    (hU.preimage f.fromNormalization).isCompact (hU.preimage f.fromNormalization).isQuasiSeparated

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
inst✝⁴ : QuasiCompact f✝
inst✝³ : QuasiSeparated f✝
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : Smooth g
x : ↥(pullback (fromNormalization f) g)
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : (pullback.snd (fromNormalization f) g ≫ g) x ∈ ↑U
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : (pullback.snd (fromNormalization f) g) x ∈ ↑V
hVU : V ≤ g ⁻¹ᵁ U
W : (pullback (fromNormalization f) g).Opens := pullback.snd (fromNormalization f) g ⁻¹ᵁ V
this : IsIso (pushoutSection ⋯ hVU ⋯ ⋯)
⊢ IsIso (app (normalizationPullback f g) W)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
⊢ ∃ n, f.resultant g ∣ f.leadingCoeff ^ n

Tactic:
obtain rfl | hf := eq_or_ne f 0

Goal state after:
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
g : R[X]
H : IsCoprime 0 g
⊢ ∃ n, resultant 0 g ∣ leadingCoeff 0 ^ n

case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
⊢ ∃ n, f.resultant g ∣ f.leadingCoeff ^ n
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
⊢ f.resultant g ≠ 0

Tactic:
obtain rfl | hf := eq_or_ne f 0

Goal state after:
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
g : R[X]
H : IsCoprime 0 g
⊢ resultant 0 g ≠ 0

case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
⊢ f.resultant g ≠ 0
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g

Tactic:
obtain rfl | hf := eq_or_ne f 0

Goal state after:
case inl
R : Type u_1
inst✝ : CommRing R
g : R[X]
r : R
⊢ (scaleRoots 0 r).resultant (g.scaleRoots r) (natDegree 0) g.natDegree =
    r ^ (natDegree 0 * g.natDegree) * resultant 0 g

case inr
R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
hf : f ≠ 0
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: K : Type u_2
inst✝ : Field K
f g : K[X]
⊢ f.resultant g = 0 ↔ (f ≠ 0 ∨ g ≠ 0) ∧ ¬IsCoprime f g

Tactic:
obtain rfl | hf := eq_or_ne f 0

Goal state after:
case inl
K : Type u_2
inst✝ : Field K
g : K[X]
⊢ resultant 0 g = 0 ↔ (0 ≠ 0 ∨ g ≠ 0) ∧ ¬IsCoprime 0 g

case inr
K : Type u_2
inst✝ : Field K
f g : K[X]
hf : f ≠ 0
⊢ f.resultant g = 0 ↔ (f ≠ 0 ∨ g ≠ 0) ∧ ¬IsCoprime f g
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
i j : Fin 3
⊢ (Matrix.reindex e e) f.sylvesterDeriv i j =
    !![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] i j

Tactic:
fin_cases i <;> fin_cases j <;>
      simp [e, sylvesterDeriv, sylvester, coeff_derivative, mul_comm, Fin.addCases,
        one_add_one_eq_two, hf, Fin.cast]

Goal state after:
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'
m : ℕ
f : R[X]
b : p.ResidueField[X]
hfm : f.Monic
hbm : b.Monic
hab : IsCoprime (X ^ (m + 1)) b
hfab : Polynomial.map (algebraMap R p.ResidueField) f = X ^ (m + 1) * b
hf : (aeval s) f = 0
R' : Type u
w✝⁴ : CommRing R'
w✝³ : Algebra R R'
w✝² : Etale R R'
P : Ideal R'
w✝¹ : P.IsPrime
w✝ : P.LiesOver p
a' b' : R'[X]
hP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
ha'm : a'.Monic
hb'm : b'.Monic
hfab' : Polynomial.map (algebraMap R R') f = a' * b'
c d : R'[X]
hcd : c * a' + d * b' = 1
ha' :
  Polynomial.map (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯).toRingHom (X ^ (m + 1)) =
    Polynomial.map (algebraMap R' P.ResidueField) a'
hb' :
  Polynomial.map (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯).toRingHom b =
    Polynomial.map (algebraMap R' P.ResidueField) b'
s₀ : ↥(integralClosure R S) := ⟨s, hRs⟩
hfs₀ : (aeval s₀) f = 0
s' : R' ⊗[R] S := 1 ⊗ₜ[R] s
hs'f : (aeval s') f = 0
hs₀'f : (aeval (1 ⊗ₜ[R] s₀)) f = 0
e₀ : R' ⊗[R] ↥(integralClosure R S) := (aeval (1 ⊗ₜ[R] s₀)) (c * a')
he₀ : IsIdempotentElem e₀
e : R' ⊗[R] S := (aeval s') (c * a')
φ : R' ⊗[R] ↥(integralClosure R S) →ₐ[R'] R' ⊗[R] S := TensorProduct.map (AlgHom.id R' R') (integralClosure R S).val
he₀e : φ e₀ = e
he : IsIdempotentElem e
P' : ↑(P.primesOver (R' ⊗[R] S)) := (Ideal.fiberIsoOfBijectiveResidueField hP).symm ⟨q, ⋯⟩
this✝ : Algebra (Localization.AtPrime P) (Localization.AtPrime ↑P') := Localization.AtPrime.algebraOfLiesOver P ↑P'
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom ↑P' = q
hs'P' : s' ∉ ↑P'
ha'P' : (aeval s') a' ∉ ↑P'
hb'P' : (aeval s') b' ∈ ↑P'
heP' : e ∉ ↑P'
P'' : Ideal (R' ⊗[R] ↥(integralClosure R S))
x✝¹ : P''.IsPrime
x✝ : P''.LiesOver P
this : (Ideal.comap φ.toRingHom ↑P').LiesOver P
H : Ideal.comap TensorProduct.includeRight.toRingHom P'' ≠ Ideal.comap (integralClosure R S).val.toRingHom q
⊢ (Ideal.comap TensorProduct.includeRight.toRingHom P'').LiesOver p

Tactic:
by simp [Ideal.liesOver_iff, Ideal.under,
      Ideal.comap_comap, Ideal.over_def P p, Ideal.over_def P'' P, ← IsScalarTower.algebraMap_eq]

Goal state after:
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'
m : ℕ
f : R[X]
b : p.ResidueField[X]
hfm : f.Monic
hbm : b.Monic
hab : IsCoprime (X ^ (m + 1)) b
hfab : Polynomial.map (algebraMap R p.ResidueField) f = X ^ (m + 1) * b
hf : (aeval s) f = 0
R' : Type u
w✝⁴ : CommRing R'
w✝³ : Algebra R R'
w✝² : Etale R R'
P : Ideal R'
w✝¹ : P.IsPrime
w✝ : P.LiesOver p
a' b' : R'[X]
hP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
ha'm : a'.Monic
hb'm : b'.Monic
hfab' : Polynomial.map (algebraMap R R') f = a' * b'
c d : R'[X]
hcd : c * a' + d * b' = 1
ha' :
  Polynomial.map (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯).toRingHom (X ^ (m + 1)) =
    Polynomial.map (algebraMap R' P.ResidueField) a'
hb' :
  Polynomial.map (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯).toRingHom b =
    Polynomial.map (algebraMap R' P.ResidueField) b'
s₀ : ↥(integralClosure R S) := ⟨s, hRs⟩
hfs₀ : (aeval s₀) f = 0
s' : R' ⊗[R] S := 1 ⊗ₜ[R] s
hs'f : (aeval s') f = 0
hs₀'f : (aeval (1 ⊗ₜ[R] s₀)) f = 0
e₀ : R' ⊗[R] ↥(integralClosure R S) := (aeval (1 ⊗ₜ[R] s₀)) (c * a')
he₀ : IsIdempotentElem e₀
e : R' ⊗[R] S := (aeval s') (c * a')
φ : R' ⊗[R] ↥(integralClosure R S) →ₐ[R'] R' ⊗[R] S := TensorProduct.map (AlgHom.id R' R') (integralClosure R S).val
he₀e : φ e₀ = e
he : IsIdempotentElem e
P' : ↑(P.primesOver (R' ⊗[R] S)) := (Ideal.fiberIsoOfBijectiveResidueField hP).symm ⟨q, ⋯⟩
this : Algebra (Localization.AtPrime P) (Localization.AtPrime ↑P') := Localization.AtPrime.algebraOfLiesOver P ↑P'
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom ↑P' = q
hs'P' : s' ∉ ↑P'
ha'P' : (aeval s') a' ∉ ↑P'
hb'P' : (aeval s') b' ∈ ↑P'
heP' : e ∉ ↑P'
P'' : Ideal (R' ⊗[R] S)
x✝¹ : P''.IsPrime
x✝ : P''.LiesOver P
H : Ideal.comap TensorProduct.includeRight.toRingHom P'' ≠ q
⊢ (Ideal.comap TensorProduct.includeRight.toRingHom P'').LiesOver p

Tactic:
by simp [Ideal.liesOver_iff, Ideal.under,
      Ideal.comap_comap, Ideal.over_def P p, Ideal.over_def P'' P, ← IsScalarTower.algebraMap_eq]

Goal state after:
Module: Mathlib.RingTheory.Ideal.CotangentBaseChange

Goal state before:
pp: case add
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
a✝ : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom
x y : T ⊗[R] ↥(Submodule.restrictScalars R I)
a : T ⊗[R] I.Cotangent
ha :
  (tensorCotangentHom R T I) a =
    (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent
      ⟨(LinearMap.lTensor T (Submodule.restrictScalars R I).subtype) x, ⋯⟩
b : T ⊗[R] I.Cotangent
hb :
  (tensorCotangentHom R T I) b =
    (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent
      ⟨(LinearMap.lTensor T (Submodule.restrictScalars R I).subtype) y, ⋯⟩
⊢ ∃ a,
    (tensorCotangentHom R T I) a =
      (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent
        ⟨(LinearMap.lTensor T (Submodule.restrictScalars R I).subtype) (x + y), ⋯⟩

Tactic:
exact ⟨a + b, by simp only [map_add, ha, hb]; rfl⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent

Goal state before:
pp: X : Scheme
Z : Set ↥X
hZ : Z ∈ irreducibleComponents ↥X
inst✝ : IsNoetherian X
⊢ Z = ↑(Hom.ker (X.irreducibleComponentOpen Z).ι).support

Tactic:
Hom.support_ker,

Goal state after:
X : Scheme
Z : Set ↥X
hZ : Z ∈ irreducibleComponents ↥X
inst✝ : IsNoetherian X
⊢ Z = closure (Set.range ⇑(X.irreducibleComponentOpen Z).ι)
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : StrictlyUnitaryPseudofunctor B C
G : StrictlyUnitaryPseudofunctor C D
x✝ : B
⊢ (F.comp G.toPseudofunctor).mapId x✝ = eqToIso ⋯

Tactic:
ext
    simp [StrictlyUnitaryPseudofunctor.mapId_eq_eqToIso,
      PrelaxFunctor.map₂_eqToHom]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ leftZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) =
    𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      adj₁.unit ▷ (f₁ ≫ f₂) ⊗≫
        f₁ ◁ (adj₂.unit ▷ (g₁ ≫ f₁) ≫ (f₂ ≫ g₂) ◁ adj₁.counit) ▷ f₂ ⊗≫ (f₁ ≫ f₂) ◁ adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c)

Tactic:
dsimp only [compUnit, compCounit]

Goal state after:
B : Type u₁
inst✝ : Bicategory B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ leftZigzag (adj₁.unit ⊗≫ f₁ ◁ adj₂.unit ▷ g₁ ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ g₂ ≫ g₁))
      (𝟙 ((g₂ ≫ g₁) ≫ f₁ ≫ f₂) ⊗≫ g₂ ◁ adj₁.counit ▷ f₂ ⊗≫ adj₂.counit) =
    𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      adj₁.unit ▷ (f₁ ≫ f₂) ⊗≫
        f₁ ◁ (adj₂.unit ▷ (g₁ ≫ f₁) ≫ (f₂ ≫ g₂) ◁ adj₁.counit) ▷ f₂ ⊗≫ (f₁ ≫ f₂) ◁ adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c)
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ rightZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) =
    𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
        g₂ ◁ ((g₁ ≫ f₁) ◁ adj₂.unit ≫ adj₁.counit ▷ (f₂ ≫ g₂)) ▷ g₁ ⊗≫ adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁)

Tactic:
dsimp only [compUnit, compCounit]

Goal state after:
B : Type u₁
inst✝ : Bicategory B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ rightZigzag (adj₁.unit ⊗≫ f₁ ◁ adj₂.unit ▷ g₁ ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ g₂ ≫ g₁))
      (𝟙 ((g₂ ≫ g₁) ≫ f₁ ≫ f₂) ⊗≫ g₂ ◁ adj₁.counit ▷ f₂ ⊗≫ adj₂.counit) =
    𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
        g₂ ◁ ((g₁ ≫ f₁) ◁ adj₂.unit ≫ adj₁.counit ▷ (f₂ ≫ g₂)) ▷ g₁ ⊗≫ adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁)
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g ≫ l₂ ⟶ l₁ ≫ h
β : l₃ ⟶ l₂
⊢ rightAdjointSquareConjugate.vcomp ((mateEquiv adj₁ adj₂) α) ((conjugateEquiv adj₂ adj₃) β) =
    𝟙 (r₁ ≫ g) ⊗≫
      rightAdjointSquare.vcomp ((mateEquiv adj₁ adj₂) α) ((mateEquiv adj₂ adj₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)) ⊗≫
        𝟙 (h ≫ r₃)

Tactic:
dsimp only [conjugateEquiv_apply, rightAdjointSquareConjugate.vcomp,
        rightAdjointSquare.vcomp]

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d : B
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g ≫ l₂ ⟶ l₁ ≫ h
β : l₃ ⟶ l₂
⊢ (mateEquiv adj₁ adj₂) α ≫ h ◁ ((ρ_ r₂).inv ≫ (mateEquiv adj₂ adj₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫ (λ_ r₃).hom) =
    𝟙 (r₁ ≫ g) ⊗≫
      ((α_ r₁ g (𝟙 c)).inv ≫
          (mateEquiv adj₁ adj₂) α ▷ 𝟙 c ≫
            (α_ h r₂ (𝟙 c)).hom ≫ h ◁ (mateEquiv adj₂ adj₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫ (α_ h (𝟙 d) r₃).inv) ⊗≫
        𝟙 (h ≫ r₃)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : ↥(unop U)) → at ↑x
ha : (isLocallyFraction 𝒜).pred a
hb : (isLocallyFraction 𝒜).pred b
x : ↥(unop U)
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal 𝒜).pred fun x ↦ (a + b) (i x)

Tactic:
rcases ha x with ⟨Va, ma, ia, ja, ⟨ra, ra_mem⟩, ⟨sa, sa_mem⟩, hwa, wa⟩

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : ↥(unop U)) → at ↑x
ha : (isLocallyFraction 𝒜).pred a
hb : (isLocallyFraction 𝒜).pred b
x : ↥(unop U)
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ unop U
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
hwa : ∀ (x : ↥Va), ↑⟨sa, sa_mem⟩ ∉ (↑x).asHomogeneousIdeal
wa :
  ∀ (x : ↥Va),
    (fun x ↦ a (ia x)) x =
      HomogeneousLocalization.mk { deg := ja, num := ⟨ra, ra_mem⟩, den := ⟨sa, sa_mem⟩, den_mem := ⋯ }
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal 𝒜).pred fun x ↦ (a + b) (i x)