mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: case hfst
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P✝ Q✝ W : MorphismProperty C
A X✝ Y✝ Z✝ : C
fst : A ⟶ X✝
snd : A ⟶ Y✝
f✝ : X✝ ⟶ Z✝
g✝ : Y✝ ⟶ Z✝
inst✝⁴ : HasPullbacks C
P Q : MorphismProperty C
inst✝³ : P.DescendsAlong Q
inst✝² : P.RespectsIso
inst✝¹ : Q.IsStableUnderBaseChange
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : Q f
hfst : P.diagonal (pullback.fst f g)
heq :
  pullback.fst (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g) =
    (pullbackSymmetry (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g)).hom ≫
      (pullbackRightPullbackFstIso (pullback.snd g g ≫ g) f (pullback.diagonal g)).hom ≫
        (pullback.congrHom ⋯ ⋯).hom ≫
          (pullbackSymmetry g f).hom ≫ pullback.diagonal (pullback.fst f g) ≫ (diagonalObjPullbackFstIso f g).hom
⊢ P
    ((pullbackRightPullbackFstIso (pullback.snd g g ≫ g) f (pullback.diagonal g)).hom ≫
      (pullback.congrHom ⋯ ⋯).hom ≫
        (pullbackSymmetry g f).hom ≫ pullback.diagonal (pullback.fst f g) ≫ (diagonalObjPullbackFstIso f g).hom)

Tactic:
rw [cancel_left_of_respectsIso (P := P)]

Goal state after:
case hfst
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P✝ Q✝ W : MorphismProperty C
A X✝ Y✝ Z✝ : C
fst : A ⟶ X✝
snd : A ⟶ Y✝
f✝ : X✝ ⟶ Z✝
g✝ : Y✝ ⟶ Z✝
inst✝⁴ : HasPullbacks C
P Q : MorphismProperty C
inst✝³ : P.DescendsAlong Q
inst✝² : P.RespectsIso
inst✝¹ : Q.IsStableUnderBaseChange
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : Q f
hfst : P.diagonal (pullback.fst f g)
heq :
  pullback.fst (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g) =
    (pullbackSymmetry (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g)).hom ≫
      (pullbackRightPullbackFstIso (pullback.snd g g ≫ g) f (pullback.diagonal g)).hom ≫
        (pullback.congrHom ⋯ ⋯).hom ≫
          (pullbackSymmetry g f).hom ≫ pullback.diagonal (pullback.fst f g) ≫ (diagonalObjPullbackFstIso f g).hom
⊢ P
    ((pullback.congrHom ⋯ ⋯).hom ≫
      (pullbackSymmetry g f).hom ≫ pullback.diagonal (pullback.fst f g) ≫ (diagonalObjPullbackFstIso f g).hom)
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: case hfst
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P✝ Q✝ W : MorphismProperty C
A X✝ Y✝ Z✝ : C
fst : A ⟶ X✝
snd : A ⟶ Y✝
f✝ : X✝ ⟶ Z✝
g✝ : Y✝ ⟶ Z✝
inst✝⁴ : HasPullbacks C
P Q : MorphismProperty C
inst✝³ : P.DescendsAlong Q
inst✝² : P.RespectsIso
inst✝¹ : Q.IsStableUnderBaseChange
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : Q f
hfst : P.diagonal (pullback.fst f g)
heq :
  pullback.fst (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g) =
    (pullbackSymmetry (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g)).hom ≫
      (pullbackRightPullbackFstIso (pullback.snd g g ≫ g) f (pullback.diagonal g)).hom ≫
        (pullback.congrHom ⋯ ⋯).hom ≫
          (pullbackSymmetry g f).hom ≫ pullback.diagonal (pullback.fst f g) ≫ (diagonalObjPullbackFstIso f g).hom
⊢ P
    ((pullback.congrHom ⋯ ⋯).hom ≫
      (pullbackSymmetry g f).hom ≫ pullback.diagonal (pullback.fst f g) ≫ (diagonalObjPullbackFstIso f g).hom)

Tactic:
rw [cancel_left_of_respectsIso (P := P)]

Goal state after:
case hfst
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P✝ Q✝ W : MorphismProperty C
A X✝ Y✝ Z✝ : C
fst : A ⟶ X✝
snd : A ⟶ Y✝
f✝ : X✝ ⟶ Z✝
g✝ : Y✝ ⟶ Z✝
inst✝⁴ : HasPullbacks C
P Q : MorphismProperty C
inst✝³ : P.DescendsAlong Q
inst✝² : P.RespectsIso
inst✝¹ : Q.IsStableUnderBaseChange
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : Q f
hfst : P.diagonal (pullback.fst f g)
heq :
  pullback.fst (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g) =
    (pullbackSymmetry (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g)).hom ≫
      (pullbackRightPullbackFstIso (pullback.snd g g ≫ g) f (pullback.diagonal g)).hom ≫
        (pullback.congrHom ⋯ ⋯).hom ≫
          (pullbackSymmetry g f).hom ≫ pullback.diagonal (pullback.fst f g) ≫ (diagonalObjPullbackFstIso f g).hom
⊢ P ((pullbackSymmetry g f).hom ≫ pullback.diagonal (pullback.fst f g) ≫ (diagonalObjPullbackFstIso f g).hom)
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: case hfst
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P✝ Q✝ W : MorphismProperty C
A X✝ Y✝ Z✝ : C
fst : A ⟶ X✝
snd : A ⟶ Y✝
f✝ : X✝ ⟶ Z✝
g✝ : Y✝ ⟶ Z✝
inst✝⁴ : HasPullbacks C
P Q : MorphismProperty C
inst✝³ : P.DescendsAlong Q
inst✝² : P.RespectsIso
inst✝¹ : Q.IsStableUnderBaseChange
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : Q f
hfst : P.diagonal (pullback.fst f g)
heq :
  pullback.fst (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g) =
    (pullbackSymmetry (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g)).hom ≫
      (pullbackRightPullbackFstIso (pullback.snd g g ≫ g) f (pullback.diagonal g)).hom ≫
        (pullback.congrHom ⋯ ⋯).hom ≫
          (pullbackSymmetry g f).hom ≫ pullback.diagonal (pullback.fst f g) ≫ (diagonalObjPullbackFstIso f g).hom
⊢ P ((pullbackSymmetry g f).hom ≫ pullback.diagonal (pullback.fst f g) ≫ (diagonalObjPullbackFstIso f g).hom)

Tactic:
rw [cancel_left_of_respectsIso (P := P)]

Goal state after:
case hfst
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P✝ Q✝ W : MorphismProperty C
A X✝ Y✝ Z✝ : C
fst : A ⟶ X✝
snd : A ⟶ Y✝
f✝ : X✝ ⟶ Z✝
g✝ : Y✝ ⟶ Z✝
inst✝⁴ : HasPullbacks C
P Q : MorphismProperty C
inst✝³ : P.DescendsAlong Q
inst✝² : P.RespectsIso
inst✝¹ : Q.IsStableUnderBaseChange
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : Q f
hfst : P.diagonal (pullback.fst f g)
heq :
  pullback.fst (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g) =
    (pullbackSymmetry (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g)).hom ≫
      (pullbackRightPullbackFstIso (pullback.snd g g ≫ g) f (pullback.diagonal g)).hom ≫
        (pullback.congrHom ⋯ ⋯).hom ≫
          (pullbackSymmetry g f).hom ≫ pullback.diagonal (pullback.fst f g) ≫ (diagonalObjPullbackFstIso f g).hom
⊢ P (pullback.diagonal (pullback.fst f g) ≫ (diagonalObjPullbackFstIso f g).hom)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Projective R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (W'⁄B).dblY (⇑↑f ∘ P) = ↑f ((W'⁄A).dblY P)

Tactic:
← map_dblY,

Goal state after:
R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Projective R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (W'⁄B).dblY (⇑↑f ∘ P) = ((W'⁄A).map ↑f).dblY (⇑↑f ∘ P)
Module: Mathlib.AlgebraicGeometry.Morphisms.Descent

Goal state before:
pp: case inr.refine_1
P P' : MorphismProperty Scheme
inst✝³ : P'.IsStableUnderBaseChange
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
inst✝ : IsZariskiLocalAtTarget P
H :
  ∀ {R S : CommRingCat} {Y : Scheme} (φ : R ⟶ S) (g : Y ⟶ Spec R),
    P' (Spec.map φ) → P (pullback.fst (Spec.map φ) g) → P g
R : CommRingCat
X Y✝ : Scheme
f : X ⟶ Spec R
g : Y✝ ⟶ Spec R
hf : (P' ⊓ @QuasiCompact) f
h : P (pullback.fst f g)
this : ∀ {X : Scheme} (f : X ⟶ Spec R), (P' ⊓ @QuasiCompact) f → P (pullback.fst f g) → (∃ T, X = Spec T) → P g
hX : ¬∃ T, X = Spec T
x✝ : CompactSpace ↥X
Y : Scheme
p : Y ⟶ X
hsurj : Surjective p
hP' : IsLocalIso p
hY : IsAffine Y
⊢ (P' ⊓ @QuasiCompact) (p ≫ f)

Tactic:
exact ⟨P'.comp_mem _ _ (H₁ _ ⟨hP', hsurj⟩) hf.1, inferInstance⟩

Goal state after:
Module: Mathlib.RingTheory.RingHom.QuasiFinite

Goal state before:
pp: T : Type u_3
inst✝² : CommRing T
R : Type u_4
S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : S →+* T
g : R →+* S
h : (f.comp g).QuasiFinite
algInst✝² : Algebra S T := f.toAlgebra
algInst✝¹ : Algebra R S := g.toAlgebra
algInst✝ : Algebra R T := (f.comp g).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝ : Algebra.QuasiFinite R T
⊢ f.QuasiFinite

Tactic:
exact .of_restrictScalars R S T

Goal state after:
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
M : Submonoid S
inst✝¹ : IsLocalization M T
inst✝ : IsScalarTower R S T
x : S
h : IsStronglyTranscendental R x
p : R[X]
u : S
s : ↥M
hp : (aeval ((algebraMap S T) x)) p * IsLocalization.mk' T u s = 0
a : S
haM : a ∈ M
e : a * ((aeval x) p * u) = 0
⊢ map (algebraMap R T) p * C (a • (algebraMap S T) u) = 0

Tactic:
simpa [map_map, ← IsScalarTower.algebraMap_eq, Algebra.smul_def] using
      congr(map (algebraMap S T) $(h (a * u) p (by linear_combination e)))

Goal state after:
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
L : Type u_3
inst✝⁴ : CommRing L
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : FaithfulSMul S L
x : S
y : L
⊢ y ∈ coeSubmodule L (conductor R x) ↔ ∀ (z : S), y * (algebraMap S L) z ∈ R[(algebraMap S L) x]

Tactic:
trans ∀ z, y * (algebraMap S L) z ∈ (R[x]).map (IsScalarTower.toAlgHom R S L)
  · simp only [coeSubmodule, Submodule.mem_map, linearMap_apply, Subalgebra.mem_map,
      IsScalarTower.coe_toAlgHom']
    constructor
    · rintro ⟨y, hy, rfl⟩ z
      exact ⟨_, hy z, map_mul _ _ _⟩
    · intro H
      obtain ⟨y, _, e⟩ := H 1
      rw [map_one, mul_one] at e
      subst e
      simp only [← map_mul, (FaithfulSMul.algebraMap_injective S L).eq_iff,
        exists_eq_right] at H
      exact ⟨_, H, rfl⟩
  · rw [AlgHom.map_adjoin, Set.image_singleton]; rfl

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal

Goal state before:
pp: case inr.refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal R
x : S
h✝ : Nontrivial R
p : (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x}))[X]
hp : p.Monic
q : R[X] := ∑ i ∈ Finset.range (p.natDegree + 1), C ((↑(p.coeff i)).coeff (p.natDegree - i)) * X ^ i
hq : q.natDegree = p.natDegree
e :
  (eval₂ (algebraMap (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) S[X]) (C x * X) p).coeff p.natDegree =
    coeff 0 p.natDegree
⊢ (aeval x) q = 0

Tactic:
simp only [eval₂_eq_sum_range, finsetSum_coeff, coeff_zero] at e

Goal state after:
case inr.refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal R
x : S
h✝ : Nontrivial R
p : (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x}))[X]
hp : p.Monic
q : R[X] := ∑ i ∈ Finset.range (p.natDegree + 1), C ((↑(p.coeff i)).coeff (p.natDegree - i)) * X ^ i
hq : q.natDegree = p.natDegree
e :
  ∑ b ∈ Finset.range (p.natDegree + 1),
      ((algebraMap (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) S[X]) (p.coeff b) * (C x * X) ^ b).coeff
        p.natDegree =
    0
⊢ (aeval x) q = 0
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
I : Ideal R
x : S
hx : x ∈ Ideal.map (algebraMap R S) I
p : R[X]
hp : p.Monic
e : (aeval x) p = 0
h : ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)
⊢ ∃ p, p.Monic ∧ (aeval x) p = 0 ∧ ∀ (i : ℕ), i ≠ p.natDegree → p.coeff i ∈ I

Tactic:
refine ⟨p, hp, e, fun i hi ↦ ?_⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
I : Ideal R
x : S
hx : x ∈ Ideal.map (algebraMap R S) I
p : R[X]
hp : p.Monic
e : (aeval x) p = 0
h : ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)
i : ℕ
hi : i ≠ p.natDegree
⊢ p.coeff i ∈ I
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
I : Ideal R
x : S
hx : x ∈ Ideal.map (algebraMap R S) I
p : R[X]
hp : p.Monic
e : (aeval x) p = 0
h : ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)
i : ℕ
hi : i ≠ p.natDegree
⊢ p.coeff i ∈ I

Tactic:
obtain hi | hi := hi.lt_or_gt

Goal state after:
case inl
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
I : Ideal R
x : S
hx : x ∈ Ideal.map (algebraMap R S) I
p : R[X]
hp : p.Monic
e : (aeval x) p = 0
h : ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)
i : ℕ
hi✝ : i ≠ p.natDegree
hi : i < p.natDegree
⊢ p.coeff i ∈ I

case inr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
I : Ideal R
x : S
hx : x ∈ Ideal.map (algebraMap R S) I
p : R[X]
hp : p.Monic
e : (aeval x) p = 0
h : ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)
i : ℕ
hi✝ : i ≠ p.natDegree
hi : p.natDegree < i
⊢ p.coeff i ∈ I
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: case e'_5
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
f : MvPolynomial PEmpty.{w + 1} S
H : (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)).IsIntegralElem f
n : PEmpty.{w + 1} →₀ ℕ
⊢ ((isEmptyAlgEquiv S PEmpty.{w + 1}).symm.toRingEquiv.toRingHom.comp (algebraMap R S)).comp
      (isEmptyAlgEquiv R PEmpty.{w + 1}).toRingEquiv.toRingHom =
    algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)

pp: case e'_6
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
f : MvPolynomial PEmpty.{w + 1} S
H : (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)).IsIntegralElem f
n : PEmpty.{w + 1} →₀ ℕ
⊢ (isEmptyAlgEquiv S PEmpty.{w + 1}).symm.toRingEquiv.toRingHom (coeff n f) = f

Tactic:
· ext r m <;> simp [Subsingleton.elim m 0, C, X, monomial, coeff, map]

Goal state after:
case e'_6
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
f : MvPolynomial PEmpty.{w + 1} S
H : (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)).IsIntegralElem f
n : PEmpty.{w + 1} →₀ ℕ
⊢ (isEmptyAlgEquiv S PEmpty.{w + 1}).symm.toRingEquiv.toRingHom (coeff n f) = f
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ @LocallyQuasiFinite = affineLocally fun {R S} [CommRing R] [CommRing S] ↦ RingHom.QuasiFinite

Tactic:
ext X Y f
    simp [locallyQuasiFinite_iff, affineLocally_iff_affineOpens_le, affineOpens]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
U V : X.AffineZariskiSite
h : (toOpensFunctor X).obj U ⟶ (toOpensFunctor X).obj V
x : ↥X
hx : x ∈ (toOpensFunctor X).obj U
f : ↑Γ(X, ↑V)
hfU : X.basicOpen f ≤ (toOpensFunctor X).obj U
hxf : ↑⟨x, hx⟩ ∈ X.basicOpen f
⊢ ∃ U_1 f, (Sieve.functorPushforward (toOpensFunctor X) ((toOpensFunctor X).imageSieve h)).arrows f ∧ x ∈ U_1

Tactic:
exact ⟨X.basicOpen f, homOfLE hfU, ⟨V.basicOpen f,
      ⟨_, (X.basicOpen_res f h.op).trans (inf_eq_right.mpr hfU)⟩, 𝟙 _,
      ⟨⟨f, rfl⟩, rfl⟩, rfl⟩, hxf⟩

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

Goal state before:
pp: case H.H.refine_3
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
y✝ a' : R[X] × ↥R[X]⁰
h : φ y✝.1 / φ ↑y✝.2 = φ a'.1 / φ ↑a'.2
this : φ (y✝.1 * ↑a'.2) = φ (a'.1 * ↑y✝.2)
⊢ ↑(a'.1, a'.2).2 * (y✝.1, y✝.2).1 = ↑(y✝.1, y✝.2).2 * (a'.1, a'.2).1

Tactic:
hφ.eq_iff,

Goal state after:
case H.H.refine_3
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
y✝ a' : R[X] × ↥R[X]⁰
h : φ y✝.1 / φ ↑y✝.2 = φ a'.1 / φ ↑a'.2
this : y✝.1 * ↑a'.2 = a'.1 * ↑y✝.2
⊢ ↑(a'.1, a'.2).2 * (y✝.1, y✝.2).1 = ↑(y✝.1, y✝.2).2 * (a'.1, a'.2).1
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
f g : P.Ring →ₐ[R] S
H✝ : f P.X = g P.X
H :
  (f.comp (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1}))).comp CAlgHom =
    (g.comp (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1}))).comp CAlgHom
H' : aeval P.X = (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1})).comp CAlgHom
⊢ f = g

Tactic:
refine Ideal.Quotient.algHom_ext _ (Polynomial.algHom_ext' H ?_)

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
f g : P.Ring →ₐ[R] S
H✝ : f P.X = g P.X
H :
  (f.comp (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1}))).comp CAlgHom =
    (g.comp (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1}))).comp CAlgHom
H' : aeval P.X = (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1})).comp CAlgHom
⊢ (f.comp (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1}))) Y =
    (g.comp (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1}))) Y
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)
⊢ Function.Bijective ⇑(toIntegralClosure R S B)

Tactic:
have (r : s) : IsLocalizedModule.Away r.1
      (Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r))
        (AlgHom.id R (integralClosure R B))).toLinearMap := by
    let := (Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r))
      (AlgHom.id R (integralClosure R B))).toAlgebra
    refine isLocalizedModule_iff_isLocalization.mpr ?_
    refine IsLocalization.tensorProduct_tensorProduct _ _ (.powers r.1) _ ?_
    ext; simp [RingHom.algebraMap_toAlgebra]

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
⊢ Function.Bijective ⇑(toIntegralClosure R S B)
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P✝ : StandardEtalePair R
P : StandardEtalePresentation R S
algInst✝ : Algebra R (P.map (algebraMap R T)).Ring :=
  ((algebraMap T (P.map (algebraMap R T)).Ring).comp (algebraMap R T)).toAlgebra
scalarTowerInst✝ : IsScalarTower R T (P.map (algebraMap R T)).Ring :=
  IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R (P.map (algebraMap R T)).Ring))
H : P.HasMap (P.map (algebraMap R T)).X
f : T ⊗[R] S →ₐ[T] (P.map (algebraMap R T)).Ring :=
  Algebra.TensorProduct.lift (Algebra.ofId T (P.map (algebraMap R T)).Ring)
    ((P.lift (P.map (algebraMap R T)).X H).comp ↑P.equivRing) ⋯
⊢ ((P.map (algebraMap R T)).lift (1 ⊗ₜ[R] P.x) ⋯).comp f = AlgHom.id T (T ⊗[R] S)

Tactic:
ext1; apply P.hom_ext; simp [f]

Goal state after:
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
p : Ideal S
r : S
hr : r ∈ integralClosure R S
hrp : r ∉ p
⊢ Function.Bijective ⇑(Localization.awayMap (integralClosure R S).val.toRingHom ⟨r, ⋯⟩) ↔
    ∀ (x : S), ∃ m, IsIntegral R (r ^ m * x)

Tactic:
Function.Bijective,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal S
r : S
hr : r ∈ integralClosure R S
hrp : r ∉ p
⊢ Function.Injective ⇑(Localization.awayMap (integralClosure R S).val.toRingHom ⟨r, ⋯⟩) ∧
      Function.Surjective ⇑(Localization.awayMap (integralClosure R S).val.toRingHom ⟨r, ⋯⟩) ↔
    ∀ (x : S), ∃ m, IsIntegral R (r ^ m * x)
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
⊢ (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⟩

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

Tactic:
refine ⟨toIntegralClosure_injective_of_flat, ?_⟩
  intro ⟨x, hx⟩
  simp only [toIntegralClosure, Subtype.ext_iff, AlgHom.coe_codRestrict, ← AlgHom.mem_range]
  refine Algebra.adjoin_le ?_ (mem_adjoin_map_integralClosure_of_isStandardEtale x hx)
  rintro _ ⟨y, hy : IsIntegral _ _, rfl⟩
  refine ⟨1 ⊗ₜ ⟨y, hy⟩, by simp⟩

Goal state after: