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

Goal state before:
pp: case f
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) (p / gcd p q) / (algebraMap K[X] K⟮X⟯) (q / gcd p q) =
    (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q

pp: case f.hc
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) (C (q / gcd p q).leadingCoeff⁻¹) ≠ 0

Tactic:
div_eq_div_iff,

Goal state after:
case f
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) (p / gcd p q) * (algebraMap K[X] K⟮X⟯) q =
    (algebraMap K[X] K⟮X⟯) p * (algebraMap K[X] K⟮X⟯) (q / gcd p q)

case f.hb
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) (q / gcd p q) ≠ 0

case f.hd
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) q ≠ 0

case f.hc
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) (C (q / gcd p q).leadingCoeff⁻¹) ≠ 0
Module: Mathlib.RingTheory.Etale.StandardEtale

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
P : StandardEtalePair R
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
hf : (aeval x) P.f ∈ I
a : S
ha : (aeval x) P.g * a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e : (aeval x) (derivative P.f) * (aeval x) p₁ + (aeval x) P.f * (aeval x) p₂ = (aeval x) P.g ^ n
ε : S
hεI : ε ∈ I
b : S
hb : (aeval x) (derivative P.f) * b = 1 + ε
this✝ : (aeval x) P.f ^ 2 = 0
this : (aeval x) P.f * ε = 0
⊢ IsUnit ((aeval ((Ideal.Quotient.mk I) x + (Ideal.Quotient.mk I) ((aeval x) P.f * -b))) P.g)

Tactic:
Ideal.Quotient.eq_zero_iff_mem.mpr (I.mul_mem_right _ hf),

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
hf : (aeval x) P.f ∈ I
a : S
ha : (aeval x) P.g * a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e : (aeval x) (derivative P.f) * (aeval x) p₁ + (aeval x) P.f * (aeval x) p₂ = (aeval x) P.g ^ n
ε : S
hεI : ε ∈ I
b : S
hb : (aeval x) (derivative P.f) * b = 1 + ε
this✝ : (aeval x) P.f ^ 2 = 0
this : (aeval x) P.f * ε = 0
⊢ IsUnit ((aeval ((Ideal.Quotient.mk I) x + 0)) P.g)
Module: Mathlib.FieldTheory.RatFunc.Basic

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

Tactic:
neg_div,

Goal state after:
K : Type u
inst✝ : Field K
x : K⟮X⟯
⊢ -x = -((algebraMap K[X] K⟮X⟯) x.num / (algebraMap K[X] K⟮X⟯) x.denom)
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
P : Ideal R
inst✝ : P.IsPrime
x : S
hx : R[x] = ⊤
⊢ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) (RingHom.ker (aeval x).toRingHom) =
    RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom

Tactic:
by
  have hx' : Function.Surjective (aeval (R := R) x) :=
    (AlgHom.range_eq_top _).mp ((adjoin_singleton_eq_range_aeval R x).symm.trans hx)
  let I := RingHom.ker (aeval (R := R) x).toRingHom
  let e : P.Fiber S ≃ₐ[P.ResidueField]
      P.ResidueField[X] ⧸ I.map (mapRingHom (algebraMap _ P.ResidueField)) :=
    Polynomial.fiberEquivQuotient (aeval (R := R) x) hx' _
  rw [← RingHom.ker_comp_of_injective _ (f := e.toRingHom) e.injective]
  convert! Ideal.mk_ker.symm
  ext a
  · dsimp [-TensorProduct.algebraMap_apply]
    rw [aeval_C, AlgEquiv.commutes]
    simp [← Ideal.Quotient.mk_algebraMap, I]
  · simpa [e] using! Polynomial.fiberEquivQuotient_tmul _ hx' P 1 X

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case mem
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
hp : φ p * t ∈ conductor R (φ X)
algInst✝ : Algebra R[X] S := φ.toAlgebra
algebraizeInst✝ : Module.Finite R[X] S
this : IsScalarTower R R[X] S
n : S → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Submodule.span R[X] ↑s = ⊤
x✝ x : S
h : x ∈ ↑s
⊢ (p.leadingCoeff ^ (s.sup n - n x) * p.leadingCoeff ^ n x) • (t * x) ∈ φ.range

Tactic:
mul_smul

Goal state after:
case mem
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
hp : φ p * t ∈ conductor R (φ X)
algInst✝ : Algebra R[X] S := φ.toAlgebra
algebraizeInst✝ : Module.Finite R[X] S
this : IsScalarTower R R[X] S
n : S → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Submodule.span R[X] ↑s = ⊤
x✝ x : S
h : x ∈ ↑s
⊢ p.leadingCoeff ^ (s.sup n - n x) • p.leadingCoeff ^ n x • (t * x) ∈ φ.range
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)
⊢ (M (i + 1)).det = r ^ (i + 1) * M₂.det

Tactic:
by
        rw [pow_succ', mul_assoc, ← IH (by lia), ← this, Matrix.det_updateCol_smul,
          Matrix.updateCol_eq_self]

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

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

Tactic:
· simp [pow_add]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: case e_a
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst✝ : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U : (directedCover Y).I₀
i : ↑Γ(Y, ↑U)
⊢ ↑((CommRingCat.Hom.hom
          (appLE f₂ (↑U) (f₂ ⁻¹ᵁ ↑U) ⋯ ≫
            CommRingCat.ofHom
              ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ ↑U) (f ⁻¹ᵁ toOpens U) ⋯)).codRestrict
                (integralClosure ↑Γ(Y, toOpens U) ↑Γ(X, f ⁻¹ᵁ toOpens U)) ⋯)))
        i) =
    ↑((CommRingCat.Hom.hom ((normalizationDiagramMap f).app (Opposite.op (toOpens U)))) i)

Tactic:
dsimp [normalizationDiagram, normalizationDiagramMap, RingHom.algebraMap_toAlgebra]

Goal state after:
case e_a
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst✝ : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U : (directedCover Y).I₀
i : ↑Γ(Y, ↑U)
⊢ (CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ ↑U) (f ⁻¹ᵁ toOpens U) ⋯))
      ((CommRingCat.Hom.hom (appLE f₂ (↑U) (f₂ ⁻¹ᵁ ↑U) ⋯)) i) =
    (CommRingCat.Hom.hom (app f (toOpens U))) i
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case a.convert_2.mul_X
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
f : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  eval₂Hom (↑(universalFactorizationMap R n m k hn)) (Sum.elim (fun x ↦ X x ⊗ₜ[R] 1) fun x ↦ 1 ⊗ₜ[R] X x)
H : ∀ (i : Fin m ⊕ Fin k), (tensorEquivSum R (Fin m) (Fin k) R) (f (X i)) = X i
p : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)
i : Fin m ⊕ Fin k
a✝ :
  p - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) (f p)) ∈
    Ideal.span
      (Set.range fun i ↦
        C (X i) - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X i))))
⊢ (p - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) (f p))) * X i ∈
    Ideal.span
      (Set.range fun i ↦
        C (X i) - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X i))))

Tactic:
exact Ideal.mul_mem_right _ _ ‹_›

Goal state after:
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
this : IsIso (pushoutSection ⋯ hVU ⋯ ⋯)
⊢ IsIso (app (normalizationPullback f g) W)

Tactic:
rw [← @isIso_comp_left_iff _ _ _ _ _ _ _ this,
    ← isIso_comp_left_iff (pushout.congrHom f.fromNormalization.app_eq_appLE rfl).hom]

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 ((pushout.congrHom ⋯ ⋯).hom ≫ pushoutSection ⋯ hVU ⋯ ⋯ ≫ app (normalizationPullback f g) W)
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsSeparated f
x : ↥X
s : ↥S
h : f x = s
hx : Scheme.Hom.QuasiFiniteAt f x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hUV : V ≤ f ⁻¹ᵁ U
this✝⁵ : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).FiniteType
algInst✝ : Algebra ↑Γ(S, U) ↑Γ(X, V) := ⋯
algebraizeInst✝ : Algebra.FiniteType ↑Γ(S, U) ↑Γ(X, V)
this✝⁴ : (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal.LiesOver (IsAffineOpen.primeIdealOf hU ⟨f x, hxU⟩).asIdeal
this✝³ : Algebra.QuasiFiniteAt (↑Γ(S, U)) (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
R : Type u
w✝⁷ : CommRing R
w✝⁶ : Algebra (↑Γ(S, U)) R
w✝⁵ : Algebra.Etale (↑Γ(S, U)) R
P : Ideal R
w✝⁴ : P.IsPrime
w✝³ : P.LiesOver (IsAffineOpen.primeIdealOf hU ⟨f x, hxU⟩).asIdeal
e : R ⊗[↑Γ(S, U)] ↑Γ(X, V)
w✝² : IsIdempotentElem e
P' : Ideal (R ⊗[↑Γ(S, U)] ↑Γ(X, V))
w✝¹ : P'.IsPrime
w✝ : P'.LiesOver P
hP' : Ideal.comap Algebra.TensorProduct.includeRight.toRingHom P' = (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
heP' : e ∉ P'
left✝ : Module.Finite R (Localization.Away e)
this✝² : (algebraMap R (Localization.Away e)).Finite
φ : Γ(S, U) ⟶ CommRingCat.of R := ⋯
hφ : (CommRingCat.Hom.hom φ).Etale
this✝¹ : Etale (Spec.map φ)
e₁ : Spec (CommRingCat.of (R ⊗[↑Γ(S, U)] ↑Γ(X, V))) ≅ pullback (Spec.map (Scheme.Hom.appLE f U V hUV)) (Spec.map φ) := ⋯
he₁ :
  e₁.hom ≫ pullback.fst (Spec.map (Scheme.Hom.appLE f U V hUV)) (Spec.map φ) =
    Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeRight.toRingHom)
g : Spec (CommRingCat.of (R ⊗[↑Γ(S, U)] ↑Γ(X, V))) ⟶ pullback f (Spec.map φ ≫ IsAffineOpen.fromSpec hU) := ⋯
W₁ : (pullback f (Spec.map φ ≫ IsAffineOpen.fromSpec hU)).Opens := ⋯
this✝ : IsFinite (W₁.ι ≫ pullback.snd f (Spec.map φ ≫ IsAffineOpen.fromSpec hU))
this : IsFinite W₁.ι
W₂ : (pullback f (Spec.map φ ≫ IsAffineOpen.fromSpec hU)).Opens := ⋯
⊢ (IsAffineOpen.fromSpec hV) { asIdeal := Ideal.comap Algebra.TensorProduct.includeRight.toRingHom P', isPrime := ⋯ } =
    x

Tactic:
convert! hV.fromSpec_primeIdealOf ⟨x, hxV⟩

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
x : ↥X
hx : QuasiFiniteAt f x
⊢ ∃ V, (toNormalization f) x ∈ V ∧ IsIso (toNormalization f ∣_ V)

Tactic:
obtain ⟨T, fT, _, ⟨u, hu⟩, V, W, v, hVW, _, hv₂⟩ := exists_etale_isCompl_of_quasiFiniteAt _ rfl hx

Goal state after:
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
⊢ ∃ V, (toNormalization f) x ∈ V ∧ IsIso (toNormalization f ∣_ V)
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
W : TopologicalSpace.Opens ↥X
hW : W ∈ X.affineOpens
hxW : x ∈ ↑W
hWV : W ≤ toNormalization f ⁻¹ᵁ V y
this✝ : IsAffine ↑W
V' : (normalization f).Opens := opensRange (X.homOfLE hWV ≫ toNormalization f ∣_ V y ≫ (V y).ι)
hV' : IsAffineOpen V'
hV'V : V' ≤ V y
this : (toNormalization f ⁻¹ᵁ V y).ι ⁻¹ᵁ toNormalization f ⁻¹ᵁ V' = (toNormalization f ⁻¹ᵁ V y).ι ⁻¹ᵁ W
⊢ toNormalization f ⁻¹ᵁ V' = W

Tactic:
simpa only [image_preimage_eq_opensRange_inf, Opens.opensRange_ι, ← preimage_inf,
        inf_eq_right.mpr, hV'V, hWV] using congr((f.toNormalization ⁻¹ᵁ V y).ι ''ᵁ $this)

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
⊢ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r ≤ f ⁻¹ᵁ U

Tactic:
Scheme.basicOpen_le,

Goal state after:
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
⊢ toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ U ≤ f ⁻¹ᵁ U
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
⊢ Submodule.FG I

Tactic:
rw [← Module.Finite.iff_fg]

Goal state after:
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
⊢ Module.Finite R ↥I
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsClosedImmersion f ↔ IsProper f ∧ Mono f

Tactic:
have (_ : Mono f) (_ : IsProper f) : LocallyQuasiFinite f := inferInstance
  rw [IsClosedImmersion.iff_isFinite_and_mono, IsFinite.iff_isProper_and_locallyQuasiFinite]
  aesop

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

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

Tactic:
Scheme.Hom.quasiFiniteAt_comp_iff

Goal state after:
case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : IsProper f
y : ↥Y
hx : (⇑f ⁻¹' {y}).Finite
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f))ᶜ)ᶜ, is_open' := ⋯ }
x : ↥↑(f ⁻¹ᵁ V)
this : Scheme.Hom.QuasiFiniteAt (f ∣_ V) x
⊢ x ∈ ↑(Scheme.Hom.quasiFiniteLocus (f ∣_ V)) ↔ x ∈ ↑⊤
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'
⊢ x' ≫ (GrpObj.mulRight x').inv ≫ (GrpObj.mulRight y').hom = y'

Tactic:
rw [← Category.assoc, ← Iso.eq_comp_inv]

Goal state after:
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'
⊢ x' ≫ (GrpObj.mulRight x').inv = y' ≫ (GrpObj.mulRight y').inv
Module: Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
p : a ⟶ b
f g h : b ⟶ c
pf : a ⟶ c
η : f ≅ g
θ : g ≅ h
η_f : p ≫ f ≅ pf
η_g : p ≫ g ≅ pf
η_h : p ≫ h ≅ pf
ih_η : p ◁ η ≪≫ η_g = η_f
ih_θ : p ◁ θ ≪≫ η_h = η_g
⊢ p ◁ (η ≪≫ θ) ≪≫ η_h = η_f

Tactic:
← ih_η,

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
p : a ⟶ b
f g h : b ⟶ c
pf : a ⟶ c
η : f ≅ g
θ : g ≅ h
η_f : p ≫ f ≅ pf
η_g : p ≫ g ≅ pf
η_h : p ≫ h ≅ pf
ih_η : p ◁ η ≪≫ η_g = η_f
ih_θ : p ◁ θ ≪≫ η_h = η_g
⊢ p ◁ (η ≪≫ θ) ≪≫ η_h = p ◁ η ≪≫ η_g
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: case e'_3
R✝¹ R✝ A : CommRingCat
X M G : Scheme
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Bialgebra R T
e_1✝ :
  ((OverClass.asOver (pullback (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))) (Spec (of S)) ⊗
          OverClass.asOver (pullback (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))) (Spec (of S))).left ⟶
      Spec (of T)) =
    (((Over.pullback (Spec.map (ofHom (algebraMap R S)))).obj (Over.mk (Spec.map (ofHom (algebraMap R T)))) ⊗
          (Over.pullback (Spec.map (ofHom (algebraMap R S)))).obj (Over.mk (Spec.map (ofHom (algebraMap R T))))).left ⟶
      Spec (of T))
⊢ (Over.Hom.left
          ((Hom.asOver
                (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ≪≫ pullbackSpecIso' R S T).hom
                (Spec (of S)) ⊗ₘ
              Hom.asOver
                (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ≪≫ pullbackSpecIso' R S T).hom
                (Spec (of S))) ≫
            μ) ≫
        (pullbackSpecIso' R S T).inv) ≫
      pullback.snd (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R)) =
    (Over.Hom.left
          (Hom.asOver
              (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ≪≫ pullbackSpecIso' R S T).hom
              (Spec (of S)) ⊗ₘ
            Hom.asOver
              (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ≪≫ pullbackSpecIso' R S T).hom
              (Spec (of S))) ≫
        (pullbackSpecIso S (S ⊗[R] T) (S ⊗[R] T)).hom ≫
          Spec.map (ofHom (mapRingHom (algebraMap R S) includeRight.toRingHom includeRight.toRingHom ⋯ ⋯)) ≫
            (pullbackSpecIso R T T).inv) ≫
      (pullbackSpecIso R T T).hom ≫ Spec.map (ofHom (Bialgebra.comulAlgHom R T).toRingHom)

Tactic:
simp [pullbackSpecIso', specOverSpec_over, OverClass.asOver, Hom.asOver, ← Spec.map_comp,
          OverClass.asOverHom, mul_spec_asOver_spec_left, ← CommRingCat.ofHom_comp,
          ← Bialgebra.comul_includeRight]

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₂
⊢ 𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
        g₂ ◁ ((g₁ ≫ f₁) ◁ adj₂.unit ≫ adj₁.counit ▷ (f₂ ≫ g₂)) ▷ g₁ ⊗≫ adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁) =
    𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      g₂ ◁ rightZigzag adj₁.unit adj₁.counit ⊗≫ rightZigzag adj₂.unit adj₂.counit ▷ g₁ ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁)

Tactic:
rw [whisker_exchange]

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₂
⊢ 𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
        g₂ ◁ (adj₁.counit ▷ 𝟙 b ≫ 𝟙 b ◁ adj₂.unit) ▷ g₁ ⊗≫ adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁) =
    𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      g₂ ◁ rightZigzag adj₁.unit adj₁.counit ⊗≫ rightZigzag adj₂.unit adj₂.counit ▷ 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
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
β : r ≫ g ⟶ h
⊢ 𝟙 (r ≫ g) ⊗≫ r ◁ adj.unit ▷ g ⊗≫ ((r ≫ l) ◁ β ≫ adj.counit ▷ h) ⊗≫ 𝟙 h =
    𝟙 (r ≫ g) ⊗≫ rightZigzag adj.unit adj.counit ▷ g ⊗≫ β

Tactic:
rw [whisker_exchange]

Goal state after:
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) ⊗≫ r ◁ adj.unit ▷ g ⊗≫ (adj.counit ▷ (r ≫ g) ≫ 𝟙 c ◁ β) ⊗≫ 𝟙 h =
    𝟙 (r ≫ g) ⊗≫ rightZigzag adj.unit adj.counit ▷ g ⊗≫ β
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 : a ⟶ b
h : a ⟶ c
γ : g ⟶ h ≫ r
⊢ 𝟙 g ⊗≫ (g ◁ adj.unit ≫ γ ▷ (l ≫ r)) ⊗≫ h ◁ adj.counit ▷ r ⊗≫ 𝟙 (h ≫ r) =
    𝟙 g ⊗≫ γ ⊗≫ h ◁ rightZigzag adj.unit adj.counit ⊗≫ 𝟙 (h ≫ r)

Tactic:
rw [whisker_exchange]

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