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

Goal state before:
pp: case pos
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]
hRS : integralClosure R S = ⊥
hφ : φ.Finite
p : R[X]
i : ℕ
hi : i = p.natDegree
n : ℕ
hn : (φ p * t) ^ n ∈ conductor R (φ X)
k : ℕ
hk : (p ^ n).leadingCoeff ^ k • t ^ n ∈ conductor R (φ X)
hpn : p.leadingCoeff ^ n = 0
⊢ p.coeff i • t ∈ (conductor R (φ X)).radical

Tactic:
use n; simp [_root_.smul_pow, hpn, hi]

Goal state after:
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:
rw [sylvesterDeriv, dif_neg hn]

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
⊢ (((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 •
        ((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: case succ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (g + f * (monomial k) r) 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 = M₂.det
hi : i + 1 ≤ m
⊢ (M (i + 1)).det = (M i).det

Tactic:
← Matrix.det_updateCol_add_smul_self (i := ⟨i, by lia⟩)
        (j := ⟨i + k + m, by lia⟩) (c := -r) (M (i + 1)) (by simp; lia)

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (g + f * (monomial k) r) 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 = M₂.det
hi : i + 1 ≤ m
⊢ ((M (i + 1)).updateCol ⟨i, ⋯⟩ fun k_1 ↦ M (i + 1) k_1 ⟨i, ⋯⟩ + -r • M (i + 1) k_1 ⟨i + k + m, ⋯⟩).det = (M i).det
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr
K : Type u_3
inst✝ : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
this :
  ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
    f.Monic →
      g.Monic →
        f.Splits →
          g.Splits →
            g.natDegree ≤ f.natDegree → f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
hfg : ¬g.natDegree ≤ f.natDegree
⊢ f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod

pp: K : Type u_3
inst✝ : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
hfg : g.natDegree ≤ f.natDegree
⊢ f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod

Tactic:
· trans ((f.roots ×ˢ g.roots).map fun ij ↦ (-1) * (ij.2 - ij.1)).prod
    · rw [resultant_comm, this g f hg hf hg' hf' (le_of_not_ge hfg), ← Multiset.map_swap_product,
        Multiset.map_map, Multiset.prod_map_mul]
      simp [hf'.natDegree_eq_card_roots, hg'.natDegree_eq_card_roots]
    · simp

Goal state after:
K : Type u_3
inst✝ : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
hfg : g.natDegree ≤ f.natDegree
⊢ f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case pos
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
p : R[X]
hp : p ∈ R[X]_m
q : R[X]
hq : q ∈ R[X]_n
hf' : f = 0
⊢ (f * ↑(⟨p, hp⟩, ⟨q, hq⟩).2).degree < ↑(m + n)

Tactic:
simp_all

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

Goal state before:
pp: case pos
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
p : R[X]
hp : p ∈ R[X]_m
q : R[X]
hq : q ∈ R[X]_n
hg' : g = 0
⊢ (g * ↑(⟨p, hp⟩, ⟨q, hq⟩).1).degree < ↑(m + n)

Tactic:
simp_all

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

Goal state before:
pp: case inl
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m
⊢ (if ↑j ≤ ↑i then g.coeff (↑i - ↑j) else 0) = if ↑j ≤ ↑i ∧ ↑i ≤ ↑j + n then g.coeff (↑i - ↑j) else 0

Tactic:
ite_and

Goal state after:
case inl
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m
⊢ (if ↑j ≤ ↑i then g.coeff (↑i - ↑j) else 0) = if ↑j ≤ ↑i then if ↑i ≤ ↑j + n then g.coeff (↑i - ↑j) else 0 else 0
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin n
⊢ (if ↑j ≤ ↑i then f.coeff (↑i - ↑j) else 0) = if ↑j ≤ ↑i ∧ ↑i ≤ ↑j + m then f.coeff (↑i - ↑j) else 0

Tactic:
ite_and

Goal state after:
case inr
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin n
⊢ (if ↑j ≤ ↑i then f.coeff (↑i - ↑j) else 0) = if ↑j ≤ ↑i then if ↑i ≤ ↑j + m then f.coeff (↑i - ↑j) else 0 else 0
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u
S : Type v
T : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra.FiniteType R T
inst✝¹ : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg : Function.Surjective ⇑(awayMapₐ f g)
p : Ideal R
inst✝ : p.IsPrime
hgp : IsUnit (1 ⊗ₜ[R] g)
this✝¹ : IsClosed (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})
q : PrimeSpectrum S
hq : q ∈ PrimeSpectrum.zeroLocus {g}
e : PrimeSpectrum.comap (algebraMap R S) q = { asIdeal := p, isPrime := inst✝ }
this✝ : q.asIdeal.LiesOver p
this :
  1 ⊗ₜ[R] g ∉
    RingHom.ker
      (Algebra.TensorProduct.lift
          (Ideal.ResidueField.mapₐ { asIdeal := p, isPrime := inst✝ }.asIdeal (↑⟨q, e⟩).asIdeal (Algebra.ofId R S) ⋯)
          (IsScalarTower.toAlgHom R S (↑⟨q, e⟩).asIdeal.ResidueField) ⋯).toRingHom
⊢ False

Tactic:
simp_all

Goal state after:
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₀)
⊢ Function.Surjective
    ⇑(Localization.awayMapₐ
        (Localization.awayMapₐ (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)) e₀)
        ((algebraMap (R' ⊗[R] R'') (Localization.Away e₀)) (1 ⊗ₜ[R] g)))

Tactic:
by
    apply Localization.awayMap_awayMap_surjective
    refine Localization.awayMap_surjective_iff.mpr fun a ↦ ?_
    induction a with
    | zero => use 0; simp
    | tmul a b =>
      obtain ⟨b', m, e : _ = _⟩ := Localization.awayMap_surjective_iff.mp hg b
      refine ⟨e₀ ^ m * a ⊗ₜ b', m, ?_⟩
      simp [e, mul_pow, mul_assoc]
    | add a b ha hb =>
      obtain ⟨xa, ma, ea⟩ := ha
      obtain ⟨xb, mb, eb⟩ := hb
      refine ⟨(e₀ * 1 ⊗ₜ[R] g) ^ mb * xa + (e₀ * 1 ⊗ₜ[R] g) ^ ma * xb, ma + mb, ?_⟩
      dsimp at ea eb ⊢
      simp only [map_add, map_mul, map_pow, Algebra.TensorProduct.map_tmul, AlgHom.coe_id, id_eq,
        ea, eb, pow_add]
      ring

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV✝ : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this✝ : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
U : Y.Opens
r : ↑Γ(normalization f, fromNormalization f ⁻¹ᵁ U)
hU : IsAffineOpen U
hr : IsAffineOpen (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r)
hxV : x ∈ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
hrV : (normalization f).basicOpen r ≤ V y
W : X.Opens := toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
H✝ : W ≤ f ⁻¹ᵁ U
H' :
  appLE (fromNormalization f) U ((normalization f).basicOpen r) ⋯ ≫
      app (toNormalization f) ((normalization f).basicOpen r) =
    appLE f U W H✝
H : (toNormalization f ∣_ V y) ⁻¹ᵁ (V y).ι ⁻¹ᵁ (normalization f).basicOpen r = opensRange (X.homOfLE ⋯)
this :
  IsIso
    (appLE (toNormalization f) ((V y).ι ''ᵁ opensRange ((normalization f).homOfLE hrV))
      ((toNormalization f ⁻¹ᵁ V y).ι ''ᵁ (toNormalization f ∣_ V y) ⁻¹ᵁ opensRange ((normalization f).homOfLE hrV)) ⋯)
⊢ IsIso
    (appLE (toNormalization f) ((normalization f).basicOpen r) (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r) ⋯)

Tactic:
convert! this <;>
      simp [Scheme.Hom.image_preimage_eq_opensRange_inf, -Scheme.preimage_basicOpen,
        f.toNormalization.preimage_mono, hrV, H]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R S
I : Ideal R
hI : (Ideal.map (algebraMap R S) I).FG
f : S ⊗[R] ↥I →ₗ[S] S := ↑(AlgebraTensorModule.rid R S S) ∘ₗ (AlgebraTensorModule.lTensor S S) (Submodule.subtype I)
hf : Function.Injective ⇑f
this✝ : Ideal.map (algebraMap R S) I = f.range
e : S ⊗[R] ↥I ≃ₗ[S] ↥(Ideal.map (algebraMap R S) I) :=
  LinearEquiv.ofInjective f hf ≪≫ₗ LinearEquiv.ofEq f.range (Ideal.map (algebraMap R S) I) ⋯
this : Module.Finite S (S ⊗[R] ↥I)
⊢ Module.Finite R ↥I

Tactic:
apply Module.Finite.of_finite_tensorProduct_of_faithfullyFlat S

Goal state after:
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
a : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom
x : T ⊗[R] S
hx : x ∈ map Algebra.TensorProduct.includeRight.toRingHom I
⊢ ∃ a, (tensorCotangentHom R T I) a = (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent ⟨x, hx⟩

Tactic:
obtain ⟨y, rfl⟩ := I.map_includeRight_eq.le hx

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
a : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom
y : T ⊗[R] ↥(Submodule.restrictScalars R I)
hx :
  (LinearMap.lTensor T (Submodule.restrictScalars R I).subtype) y ∈ map Algebra.TensorProduct.includeRight.toRingHom I
⊢ ∃ a,
    (tensorCotangentHom R T I) a =
      (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent
        ⟨(LinearMap.lTensor T (Submodule.restrictScalars R I).subtype) y, hx⟩
Module: Mathlib.RingTheory.Etale.Descent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Module.FaithfullyFlat R T
inst✝ : Etale T (T ⊗[R] S)
⊢ Etale R S

Tactic:
rw [Etale.iff_formallyUnramified_and_smooth]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Module.FaithfullyFlat R T
inst✝ : Etale T (T ⊗[R] S)
⊢ FormallyUnramified R S ∧ Smooth R S
Module: Mathlib.RingTheory.Etale.Descent

Goal state before:
pp: R S T : Type u_1
x✝⁴ : CommRing R
x✝³ : CommRing S
x✝² : CommRing T
x✝¹ : Algebra R S
x✝ : Algebra R T
h : Module.FaithfullyFlat R S
h' : Algebra.Smooth S (S ⊗[R] T)
⊢ Algebra.Smooth R T

Tactic:
exact .of_smooth_tensorProduct_of_faithfullyFlat S

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

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst✝³ : LocallyOfFiniteType f
inst✝² : GrpObj (Over.mk f)
inst✝¹ : IsReduced G
inst✝ : IsAlgClosed K
this✝ : JacobsonSpace ↥G
this : Nonempty ↥G
H : (↑(Scheme.Hom.smoothLocus f))ᶜ.Nonempty
x : ↥G
hx : x ∈ (↑(Scheme.Hom.smoothLocus f))ᶜ
hxc : x ∈ closedPoints ↥G
y : ↥G
hy : y ∈ Scheme.Hom.smoothLocus f
hyc : y ∈ closedPoints ↥G
x' : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ Over.mk f := Over.homMk ↑((pointEquivClosedPoint f).symm ⟨x, hxc⟩) ⋯
y' : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ Over.mk f := Over.homMk ↑((pointEquivClosedPoint f).symm ⟨y, hyc⟩) ⋯
α : Over.mk f ≅ Over.mk f := (GrpObj.mulRight x').symm ≪≫ GrpObj.mulRight y'
hα : x' ≫ α.hom = y'
⊢ (Over.Hom.left α.hom) x = y

Tactic:
simpa [x', y', pointEquivClosedPoint] using congr(($hα).left (IsLocalRing.closedPoint K))

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize

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

Tactic:
simp_all

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize

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

Tactic:
by
  simp_all

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: X S T : Scheme
f : X ⟶ S
g : T ⟶ S
inst✝² : IsAffine T
t : ↥T
inst✝¹ : Flat f
inst✝ : IsFinite f
⊢ finrank f (g t) = IsAffine.finrank (pullback.snd f g) t

Tactic:
let i := S.affineOpenCover.f (S.affineOpenCover.idx (g t))

Goal state after:
X S T : Scheme
f : X ⟶ S
g : T ⟶ S
inst✝² : IsAffine T
t : ↥T
inst✝¹ : Flat f
inst✝ : IsFinite f
i : Spec (S.affineOpenCover.X (S.affineOpenCover.idx (g t))) ⟶ S := S.affineOpenCover.f (S.affineOpenCover.idx (g t))
⊢ finrank f (g t) = IsAffine.finrank (pullback.snd f g) t
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
x : ↥X
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f] (x : ↥X), (∃ R, Y = Spec R) → 1 ≤ finrank f (f x)
hY : ¬∃ R, Y = Spec R
R : CommRingCat
g : Spec R ⟶ Y
hg : IsOpenImmersion g
y : ↥(Spec R)
hy : g y = f x
⊢ 1 ≤ finrank (pullback.snd f g) y

Tactic:
obtain ⟨z, hzl, hzr⟩ := Scheme.Pullback.exists_preimage_pullback (f := f) (g := g) x y hy.symm

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
x : ↥X
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f] (x : ↥X), (∃ R, Y = Spec R) → 1 ≤ finrank f (f x)
hY : ¬∃ R, Y = Spec R
R : CommRingCat
g : Spec R ⟶ Y
hg : IsOpenImmersion g
y : ↥(Spec R)
hy : g y = f x
z : ↥(pullback f g)
hzl : (pullback.fst f g) z = x
hzr : (pullback.snd f g) z = y
⊢ 1 ≤ finrank (pullback.snd f g) y
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Infinite σ
this : ringKrullDim (MvPolynomial σ R) = ⊤
⊢ ringKrullDim R + ⊤ ≤ ringKrullDim (MvPolynomial σ R)

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: case pos
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : K
ha : a = 0
⊢ (ordFrac R) a =
    (MonoidWithZero.inverse.comp
        (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)).toMonoidWithZeroHom)
      a

Tactic:
simp_all

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
l : a ⟶ b
r : b ⟶ a
adj : l ⊣ r
⊢ (mateEquiv adj adj) ((λ_ l).hom ≫ (ρ_ l).inv) = (ρ_ r).hom ≫ (λ_ r).inv

Tactic:
by
  simp [← cancel_mono (λ_ r).hom,
    ← conjugateEquiv_id adj, conjugateEquiv_apply]

Goal state after:
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 : (x : ↥(unop U)) → at ↑x
ha : (isLocallyFraction 𝒜).pred a
x : ↥(unop U)
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal 𝒜).pred fun x ↦ (-a) (i x)

Tactic:
by
  rcases ha x with ⟨V, m, i, j, ⟨r, r_mem⟩, ⟨s, s_mem⟩, nin, hy⟩
  refine ⟨V, m, i, j, ⟨-r, neg_mem r_mem⟩, ⟨s, s_mem⟩, nin, fun y => ?_⟩
  simp only [ext_iff_val, val_mk] at hy
  simp only [Pi.neg_apply, ext_iff_val, val_neg, hy, val_mk, neg_mk]

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Radical

Goal state before:
pp: case homogeneous_mem_or_mem.refine_2
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : I.IsPrime
x y : A
hx : IsHomogeneousElem 𝒜 x
hy : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal
H : x ∈ I ∨ y ∈ I
⊢ y ∈ I → y ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal

Tactic:
· exact Ideal.mem_homogeneousCore_of_homogeneous_of_mem hy

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a : A
n : ℕ
hn : a ∈ 𝒜 n
⊢ a ∈ carrier f_deg q ↔
    HomogeneousLocalization.mk { deg := m * n, num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal

Tactic:
by
  trans (HomogeneousLocalization.mk ⟨m * n, ⟨proj 𝒜 n a ^ m, by rw [← smul_eq_mul]; mem_tac⟩,
    ⟨f ^ n, by rw [mul_comm]; mem_tac⟩, ⟨_, rfl⟩⟩ : A⁰_ f) ∈ q.asIdeal
  · refine ⟨fun h ↦ h n, fun h i ↦ if hi : i = n then hi ▸ h else ?_⟩
    convert! zero_mem q.asIdeal
    apply HomogeneousLocalization.val_injective
    simp only [proj_apply, decompose_of_mem_ne _ hn (Ne.symm hi), zero_pow hm.ne',
      HomogeneousLocalization.val_mk, Localization.mk_zero, HomogeneousLocalization.val_zero]
  · simp only [proj_apply, decompose_of_mem_same _ hn]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: case convert_4.add
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ n, f i ∈ 𝒜 n
hf : Algebra.adjoin (↥(𝒜 0)) (Set.range f) = ⊤
x✝ x y : A
hx : x ∈ Algebra.adjoin (↥(𝒜 0)) (Set.range f)
hy : y ∈ Algebra.adjoin (↥(𝒜 0)) (Set.range f)
a✝¹ : x - (GradedRing.projZeroRingHom 𝒜) x ∈ Ideal.span (Set.range f)
a✝ : y - (GradedRing.projZeroRingHom 𝒜) y ∈ Ideal.span (Set.range f)
⊢ x + y - (GradedRing.projZeroRingHom 𝒜) (x + y) ∈ Ideal.span (Set.range f)

Tactic:
rw [map_add, add_sub_add_comm]
    exact add_mem ‹_› ‹_›

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
⊢ Away 𝒜 f →+* Away 𝒜 x

Tactic:
let e := RingEquiv.ofLeftInverse (f := algebraMap (Away 𝒜 x) (Localization.Away x))
    (h := (val_injective _).hasLeftInverse.choose_spec)

Goal state after:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
e✝ : ι
f g : A
hg : g ∈ 𝒜 e✝
x : A
hx : x = f * g
e : Away 𝒜 x ≃+* ↥(algebraMap (Away 𝒜 x) (Localization.Away x)).range := RingEquiv.ofLeftInverse ⋯
⊢ Away 𝒜 f →+* Away 𝒜 x
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
a : Away 𝒜 f
⊢ val ((awayMap 𝒜 hg hx) a) = (awayMapAux 𝒜 ⋯) a

Tactic:
let e := RingEquiv.ofLeftInverse (f := algebraMap (Away 𝒜 x) (Localization.Away x))
    (h := (val_injective _).hasLeftInverse.choose_spec)

Goal state after:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
e✝ : ι
f g : A
hg : g ∈ 𝒜 e✝
x : A
hx : x = f * g
a : Away 𝒜 f
e : Away 𝒜 x ≃+* ↥(algebraMap (Away 𝒜 x) (Localization.Away x)).range := RingEquiv.ofLeftInverse ⋯
⊢ val ((awayMap 𝒜 hg hx) a) = (awayMapAux 𝒜 ⋯) a
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
U : (Spec R).Opens
f : ↑R
hf : U ≤ PrimeSpectrum.basicOpen f
⊢ Function.Bijective ⇑((algebraMap (↑R) (Module.End ↑R ↑Γ(M, U))) f)

Tactic:
have : ⇑((algebraMap R (Module.End ↑R ↑Γ(M, U))) f) =
      algebraMap (Γ(Spec R, U)) (Module.End Γ(Spec R, U) Γ(M, U))
        (((Spec R).presheaf.map (homOfLE hf).op) <| algebraMap R _ f) :=
    rfl

Goal state after:
R : CommRingCat
M : (Spec R).Modules
U : (Spec R).Opens
f : ↑R
hf : U ≤ PrimeSpectrum.basicOpen f
this :
  ⇑((algebraMap (↑R) (Module.End ↑R ↑Γ(M, U))) f) =
    ⇑((algebraMap (↑Γ(Spec R, U)) (Module.End ↑Γ(Spec R, U) ↑Γ(M, U)))
        ((ConcreteCategory.hom ((Spec R).presheaf.map (homOfLE hf).op))
          ((algebraMap ↑R ↑Γ(Spec R, PrimeSpectrum.basicOpen f)) f)))
⊢ Function.Bijective ⇑((algebraMap (↑R) (Module.End ↑R ↑Γ(M, U))) f)