mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Preserves

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a)
Y : Type w
t : F.obj (op I)
h :
  (fun t ↦ FamilyOfElements.IsAmalgamation (fun ⦃Y⦄ f a ↦ ⋯.elim) t) t ∧
    ∀ (y : F.obj (op I)), (fun t ↦ FamilyOfElements.IsAmalgamation (fun ⦃Y⦄ f a ↦ ⋯.elim) t) y → y = t
a : Y ⟶ F.obj (op I)
x✝ : Y
⊢ (ConcreteCategory.hom a).toFun x✝ = (ConcreteCategory.hom default).toFun x✝

Tactic:
exact h.2 _ (by tauto)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Preserves

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a)
⊢ IsTerminal (F.obj (op I))

Tactic:
by
  refine @IsTerminal.ofUnique _ _ _ fun Y ↦ ?_
  choose t h using hF (by tauto) (by tauto)
  exact ⟨⟨↾fun _ ↦ t⟩, fun a ↦ by ext; exact h.2 _ (by tauto)⟩

Goal state after:
Module: Mathlib.Topology.Category.TopCat.ULift

Goal state before:
pp: ⊢ PreservesLimitsOfSize.{w', w, u, max u v, u + 1, max (u + 1) (v + 1)} uliftFunctor

Tactic:
refine ⟨⟨fun {K} ↦ ⟨fun {c} hc ↦ ?_⟩⟩⟩
  rw [nonempty_isLimit_iff_eq_induced]
  · refine le_antisymm ?_ ?_
    · rw [le_iInf_iff]
      rintro j s ⟨t, ht, rfl⟩
      refine ⟨Homeomorph.ulift.symm ⁻¹' ((uliftFunctor.map (c.π.app j)) ⁻¹' t), ?_, rfl⟩
      apply Homeomorph.ulift.continuous_invFun.isOpen_preimage
      apply (uliftFunctor.map (c.π.app j)).hom.continuous_toFun.isOpen_preimage _ ht
    · change _ ≤ TopologicalSpace.induced _ _
      rw [← generateFrom_iUnion_isOpen, induced_of_isLimit _ hc, induced_iInf, le_iInf_iff]
      rintro i s ⟨-, ⟨t, ht, rfl⟩, rfl⟩
      refine .basic _ ?_
      rw [Set.mem_iUnion]
      exact ⟨i, ULift.down ⁻¹' t, Homeomorph.ulift.continuous_toFun.isOpen_preimage _ ht, rfl⟩
  · exact isLimitOfPreserves (forget TopCat ⋙ CategoryTheory.uliftFunctor) hc

Goal state after:
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: case h
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝¹ : FormallyUnramified K L
this✝ : Module.Finite K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
this : IsUnit ((Ideal.Quotient.mk I) ((aeval x) (derivative (minpoly K pb.gen))))
u : B
hu : (Ideal.Quotient.mk I) u = -↑this.unit⁻¹
⊢ (Ideal.Quotient.mk I) ((aeval x) (derivative (minpoly K pb.gen)) * u) + (Ideal.Quotient.mk I) 1 = 0

Tactic:
map_mul,

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝¹ : FormallyUnramified K L
this✝ : Module.Finite K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
this : IsUnit ((Ideal.Quotient.mk I) ((aeval x) (derivative (minpoly K pb.gen))))
u : B
hu : (Ideal.Quotient.mk I) u = -↑this.unit⁻¹
⊢ (Ideal.Quotient.mk I) ((aeval x) (derivative (minpoly K pb.gen))) * (Ideal.Quotient.mk I) u +
      (Ideal.Quotient.mk I) 1 =
    0
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: case w.hy
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
u : B
hu : (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I
⊢ (Ideal.Quotient.mk I) (u * (aeval x) (minpoly K pb.gen)) = 0

Tactic:
map_mul,

Goal state after:
case w.hy
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
u : B
hu : (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I
⊢ (Ideal.Quotient.mk I) u * (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
r : R
x✝ : S
y✝ : Ω[A⁄R]
⊢ x✝ ⊗ₜ[R] (r • y✝) = r • x✝ ⊗ₜ[R] y✝

Tactic:
tmul_smul

Goal state after:
case tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
r : R
x✝ : S
y✝ : Ω[A⁄R]
⊢ r • x✝ ⊗ₜ[R] y✝ = r • x✝ ⊗ₜ[R] y✝
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
m n : ℕ
hmn : m ≤ n
⊢ transitionMap I N hmn ∘ₗ ↑R (reduceModIdeal (I ^ n) f) = ↑R (reduceModIdeal (I ^ m) f) ∘ₗ transitionMap I M hmn

Tactic:
ext x
  simp

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Exactness

Goal state before:
pp: case convert_6.refine_1
R : Type u
inst✝⁸ : CommRing R
I : Ideal R
M : Type u
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
k : ℕ
hkn : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)
x : AdicCauchySequence I N
hker : ∀ (n : ℕ), g (↑x n) ∈ I ^ n • ⊤
n : ℕ
d : N
hdmem : d ∈ I ^ (k + n + 1) • ⊤
y yₙ : M
hd : f y = ↑x (k + n + 1) - d
hyₙ : f yₙ - ↑x (k + n) ∈ I ^ (k + n) • ⊤
⊢ Submodule.Quotient.mk (↑x (k + n + 1)) = Submodule.Quotient.mk (↑x (k + n))

Tactic:
exact AdicCauchySequence.mk_eq_mk (by lia) _

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r s : AdicCompletion I R
x : AdicCompletion I M
⊢ (r * s) • x = r • s • x

Tactic:
ext n
    simp only [smul_eval, val_mul, mul_smul]

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
f : P.Ring
h : (algebraMap P.Ring S) f = g
⊢ (localizationAway T g).ker =
    Ideal.span
      {((localizationAway T g).ofComp P).toAlgHom ((rename Sum.inr) f * X (Sum.inl ())) -
          ((localizationAway T g).ofComp P).toAlgHom 1}

Tactic:
map_mul,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
f : P.Ring
h : (algebraMap P.Ring S) f = g
⊢ (localizationAway T g).ker =
    Ideal.span
      {((localizationAway T g).ofComp P).toAlgHom ((rename Sum.inr) f) *
            ((localizationAway T g).ofComp P).toAlgHom (X (Sum.inl ())) -
          ((localizationAway T g).ofComp P).toAlgHom 1}
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
⊢ (compLocalizationAwayAlgHom T g P) ((rename Sum.inr) (P.σ g) * X (Sum.inl ())) - 1 = 0

Tactic:
map_mul,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
⊢ (compLocalizationAwayAlgHom T g P) ((rename Sum.inr) (P.σ g)) * (compLocalizationAwayAlgHom T g P) (X (Sum.inl ())) -
      1 =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
⊢ ![u ^ 4 * W'.dblX P, u ^ 4 * W'.dblY P, u ^ 4 * W'.dblZ P] =
    ![u ^ 4 * W'.dblX P, u ^ 4 * W'.dblY P, u ^ 4 * W'.dblXYZ P z]

Tactic:
dblXYZ_Z

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
⊢ ![u ^ 4 * W'.dblX P, u ^ 4 * W'.dblY P, u ^ 4 * W'.dblZ P] =
    ![u ^ 4 * W'.dblX P, u ^ 4 * W'.dblY P, u ^ 4 * W'.dblZ P]
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
⊢ (compLocalizationAwayAlgHom T g P) (((localizationAway T g).toComp P).toAlgHom (P.σ g)) *
        (compLocalizationAwayAlgHom T g P) (X (Sum.inl ())) -
      1 =
    0

Tactic:
rw [compLocalizationAwayAlgHom_toAlgHom_toComp, compLocalizationAwayAlgHom_X_inl,
    IsScalarTower.algebraMap_apply P.Ring (P.Ring ⧸ P.ker ^ 2) (Localization.Away _)]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
⊢ (algebraMap (P.Ring ⧸ P.ker ^ 2) (Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g))))
          ((algebraMap P.Ring (P.Ring ⧸ P.ker ^ 2)) (P.σ g)) *
        IsLocalization.Away.invSelf ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) -
      1 =
    0
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
a : ((localizationAway T g).comp P).Ring
hx : ((rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1) * a ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1}
⊢ (compLocalizationAwayAlgHom T g P) (((rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1) * a) = 0

Tactic:
map_mul,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
a : ((localizationAway T g).comp P).Ring
hx : ((rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1) * a ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1}
⊢ (compLocalizationAwayAlgHom T g P) ((rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1) *
      (compLocalizationAwayAlgHom T g P) a =
    0
Module: Mathlib.RingTheory.Extension.Cotangent.Free

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_3
σ : Type u_4
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
b : Module.Basis κ S Ω[S⁄R]
hb : ∀ (k : κ), b k = (D R S) (P.val (v k))
inst✝ : Subsingleton (H1Cotangent R S)
⊢ Function.Bijective ⇑(P.cotangentRestrict hu)

Tactic:
refine P.cotangentRestrict_bijective_of_isCompl _ huv ?_ ?_

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_3
σ : Type u_4
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
b : Module.Basis κ S Ω[S⁄R]
hb : ∀ (k : κ), b k = (D R S) (P.val (v k))
inst✝ : Subsingleton (H1Cotangent R S)
⊢ Submodule.span S (Set.range fun i ↦ (D R S) (P.val (v i))) = ⊤

case refine_2
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_3
σ : Type u_4
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
b : Module.Basis κ S Ω[S⁄R]
hb : ∀ (k : κ), b k = (D R S) (P.val (v k))
inst✝ : Subsingleton (H1Cotangent R S)
⊢ Disjoint P.toExtension.toKaehler.ker (Submodule.span S (Set.range fun x ↦ P.cotangentSpaceBasis (v x)))
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: case a.a
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
hsple :
  ∀ {x : ((localizationAway T g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
⊢ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} *
      Ideal.map ((localizationAway T g).toComp P).toAlgHom P.ker ≤
    RingHom.ker (compLocalizationAwayAlgHom T g P)

Tactic:
rw [Ideal.mul_le]
      intro x hx y hy
      simp [hsple hx]

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
hsple :
  ∀ {x : ((localizationAway T g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
⊢ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} *
      Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} ≤
    RingHom.ker (compLocalizationAwayAlgHom T g P)

Tactic:
rw [Ideal.mul_le]
      intro x hx y hy
      simp [hsple hx]

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

Goal state before:
pp: n m : ℕ
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ Smooth f ↔ affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ RingHom.Smooth) f

Tactic:
rw [smooth_iff, affineLocally_iff_forall_isAffineOpen]

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

Goal state before:
pp: X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.RespectsIso @IsProper

Tactic:
rw [isProper_eq]
  infer_instance

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

Goal state before:
pp: X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.IsStableUnderComposition @IsProper

Tactic:
rw [isProper_eq]
  infer_instance

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

Goal state before:
pp: X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.IsMultiplicative @IsProper

Tactic:
rw [isProper_eq]
  infer_instance

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

Goal state before:
pp: X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.IsStableUnderBaseChange @IsProper

Tactic:
rw [isProper_eq]
  infer_instance

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

Goal state before:
pp: X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtTarget @IsProper

Tactic:
rw [isProper_eq]
  infer_instance

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
hf : f.QuasiFinite
hg : g.QuasiFinite
⊢ (f.comp g).QuasiFinite

Tactic:
by
  algebraize [f, g, (f.comp g)]
  exact .trans R S T

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral

Goal state before:
pp: case h.inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
H : IsIntegral R s
h : ∃ t ∈ R⁰, t • s ∈ (algebraMap R S).range
b : R
hb' : b ∈ R⁰
hb : ∀ i < (minpoly R s).natDegree, b • s ^ i ∈ (algebraMap R S).range
n : ℕ
IH : ∀ m < n, b • s ^ m ∈ (algebraMap R S).range
hn : (minpoly R s).natDegree ≤ n
this : s ^ (minpoly R s).natDegree = -∑ x ∈ Finset.range (minpoly R s).natDegree, (minpoly R s).coeff x • s ^ x
⊢ b • -(s ^ (n - (minpoly R s).natDegree) * ∑ x ∈ Finset.range (minpoly R s).natDegree, (minpoly R s).coeff x • s ^ x) ∈
    (algebraMap R S).range

Tactic:
smul_neg,

Goal state after:
case h.inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
H : IsIntegral R s
h : ∃ t ∈ R⁰, t • s ∈ (algebraMap R S).range
b : R
hb' : b ∈ R⁰
hb : ∀ i < (minpoly R s).natDegree, b • s ^ i ∈ (algebraMap R S).range
n : ℕ
IH : ∀ m < n, b • s ^ m ∈ (algebraMap R S).range
hn : (minpoly R s).natDegree ≤ n
this : s ^ (minpoly R s).natDegree = -∑ x ∈ Finset.range (minpoly R s).natDegree, (minpoly R s).coeff x • s ^ x
⊢ -(b •
        (s ^ (n - (minpoly R s).natDegree) *
          ∑ x ∈ Finset.range (minpoly R s).natDegree, (minpoly R s).coeff x • s ^ x)) ∈
    (algebraMap R S).range
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

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
I : Ideal R
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp (mapRingHom (algebraMap R I.ResidueField))) ⋯ ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
⊢ (↑({ toRingHom := f, commutes' := ⋯ }.comp
            { toRingHom := RatFunc.liftRingHom ↑(aeval ((algebraMap R[X] J.ResidueField) X)) ⋯, commutes' := ⋯ })).comp
      (algebraMap I.ResidueField[X] (RatFunc I.ResidueField)) =
    (RingHom.id (RatFunc I.ResidueField)).comp (algebraMap I.ResidueField[X] (RatFunc I.ResidueField))

Tactic:
simp only [AlgHom.comp_toRingHom, AlgHom.coe_ringHom_mk, RingHom.comp_assoc,
      RatFunc.liftRingHom_comp_algebraMap, RingHomCompTriple.comp_eq, f]

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
I : Ideal R
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp (mapRingHom (algebraMap R I.ResidueField))) ⋯ ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
⊢ (Ideal.ResidueField.lift J
          ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp (mapRingHom (algebraMap R I.ResidueField))) ⋯
          ⋯).comp
      ↑(aeval ((algebraMap R[X] J.ResidueField) X)) =
    algebraMap I.ResidueField[X] (RatFunc I.ResidueField)
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

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
I : Ideal R
inst✝⁵ : I.IsPrime
J : Ideal R[X]
inst✝⁴ : J.IsPrime
inst✝³ : J.LiesOver I
inst✝² : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra I J
f : R[X] →ₐ[R] S
hf : Function.Surjective ⇑f
p : Ideal R
inst✝ : p.IsPrime
⊢ RingHom.ker ↑f ≤ Ideal.comap (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker (aeval (1 ⊗ₜ[R] f X)).toRingHom)

Tactic:
RingHom.comap_ker

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
I : Ideal R
inst✝⁵ : I.IsPrime
J : Ideal R[X]
inst✝⁴ : J.IsPrime
inst✝³ : J.LiesOver I
inst✝² : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra I J
f : R[X] →ₐ[R] S
hf : Function.Surjective ⇑f
p : Ideal R
inst✝ : p.IsPrime
⊢ RingHom.ker ↑f ≤ RingHom.ker ((aeval (1 ⊗ₜ[R] f X)).comp (mapRingHom (algebraMap R p.ResidueField)))
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case H.H
K : Type u
inst✝⁶ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : CommGroupWithZero G₀
inst✝⁴ : Field L
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
hq : φ ↑q ∈ S[X]⁰
hq' : φ ↑q' ∈ S[X]⁰
hqq' : φ ↑(q * q') ∈ S[X]⁰
⊢ { toFractionRing := Localization.mk (φ (p * p')) ⟨φ (↑q * ↑q'), ⋯⟩ } =
    { toFractionRing := Localization.mk (φ p) ⟨φ ↑q, hq⟩ * Localization.mk (φ p') ⟨φ ↑q', hq'⟩ }

Tactic:
map_mul,

Goal state after:
case H.H
K : Type u
inst✝⁶ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : CommGroupWithZero G₀
inst✝⁴ : Field L
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
hq : φ ↑q ∈ S[X]⁰
hq' : φ ↑q' ∈ S[X]⁰
hqq' : φ ↑(q * q') ∈ S[X]⁰
⊢ { toFractionRing := Localization.mk (φ p * φ p') ⟨φ ↑q * φ ↑q', ⋯⟩ } =
    { toFractionRing := Localization.mk (φ p) ⟨φ ↑q, hq⟩ * Localization.mk (φ p') ⟨φ ↑q', hq'⟩ }
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: case mpr
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
x : ↥X
hx : x ∈ U.toOpens
⊢ (∃ i ∈ s, x ∈ X.basicOpen i) → ∃ V, (∃ f ∈ s, ∃ g, X.basicOpen (f * g) = V.toOpens) ∧ ∃ x_1, x ∈ V.toOpens

Tactic:
· rintro ⟨f, hfs, hxf⟩
    refine ⟨U.basicOpen _, ⟨f, hfs, 1, rfl⟩, ⟨_, rfl⟩, by simpa using hxf⟩

Goal state after: