mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝ : Module.Flat R T
a : S →+* T ⊗[R] S := ⋯
f : (map a I).Cotangent →ₗ[T] T ⊗[R] S ⧸ map a I ^ 2 := ⋯
g : T ⊗[R] I.Cotangent →ₗ[T] T ⊗[R] (S ⧸ I ^ 2) := ⋯
hₐ : T ⊗[R] (S ⧸ I ^ 2) ≃ₐ[T] T ⊗[R] S ⧸ map a I ^ 2 := ⋯
this : f ∘ₗ tensorCotangentHom R T I = hₐ.toLinearMap ∘ₗ g
⊢ Function.Injective ⇑g

Tactic:
apply Module.Flat.lTensor_preserves_injective_linearMap (M := T)
      (I.cotangentToQuotientSquare.restrictScalars R)
    apply cotangentToQuotientSquare_injective

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

Goal state before:
pp: case hi₂
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Bijective ⇑0

pp: case hi₄
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Bijective ⇑↑(LinearEquiv.restrictScalars R (P.tensorCotangentOfFlat T))

pp: case hi₅
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Injective ⇑↑(LinearEquiv.restrictScalars R (P.tensorCotangentSpace T))

Tactic:
· simp

Goal state after:
case hi₄
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Bijective ⇑↑(LinearEquiv.restrictScalars R (P.tensorCotangentOfFlat T))

case hi₅
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Injective ⇑↑(LinearEquiv.restrictScalars R (P.tensorCotangentSpace T))
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
obj : B → C
map : {X Y : B} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id : ∀ (X : B), map (𝟙 X) = 𝟙 (obj X)
map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (map f ⟶ map g)
map₂_id : ∀ {a b : B} (f : a ⟶ b), map₂ (𝟙 f) = 𝟙 (map f)
map₂_comp : ∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h), map₂ (η ≫ θ) = map₂ η ≫ map₂ θ
mapComp : {a b c : B} → (f : a ⟶ b) → (g : b ⟶ c) → map f ≫ map g ⟶ map (f ≫ g)
mapComp_naturality_left :
  ∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c), mapComp f g ≫ map₂ (η ▷ g) = map₂ η ▷ map g ≫ mapComp f' g
mapComp_naturality_right :
  ∀ {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g'), mapComp f g ≫ map₂ (f ◁ η) = map f ◁ map₂ η ≫ mapComp f g'
map₂_leftUnitor : ∀ {a b : B} (f : a ⟶ b), map₂ (λ_ f).inv = (λ_ (map f)).inv ≫ eqToHom ⋯ ≫ mapComp (𝟙 a) f
a b : B
f : a ⟶ b
⊢ map f ≫ 𝟙 (obj b) = map f ≫ map (𝟙 b)

Tactic:
by rw [map_id b]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: case obj
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
x✝ : B
⊢ (F.comp (id C)).obj x✝ = F.obj x✝

pp: case map
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @Prefunctor.map B inst✝¹.toQuiver C inst✝.toQuiver (F.comp (id C)).toPrefunctor ≍
    @Prefunctor.map B inst✝¹.toQuiver C inst✝.toQuiver F.toPrefunctor

pp: case map₂
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @PrelaxFunctorStruct.map₂ B inst✝¹.toQuiver (fun a b ↦ (homCategory a b).toQuiver) C inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) (F.comp (id C)).toPrelaxFunctorStruct ≍
    @PrelaxFunctorStruct.map₂ B inst✝¹.toQuiver (fun a b ↦ (homCategory a b).toQuiver) C inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) F.toPrelaxFunctorStruct

pp: case mapId
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ (F.comp (id C)).mapId ≍ F.mapId

pp: case mapComp
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @LaxFunctor.mapComp B inst✝¹ C inst✝ (F.comp (id C)).toLaxFunctor ≍
    @LaxFunctor.mapComp B inst✝¹ C inst✝ F.toLaxFunctor

Tactic:
· simp

Goal state after:
case map
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @Prefunctor.map B inst✝¹.toQuiver C inst✝.toQuiver (F.comp (id C)).toPrefunctor ≍
    @Prefunctor.map B inst✝¹.toQuiver C inst✝.toQuiver F.toPrefunctor

case map₂
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @PrelaxFunctorStruct.map₂ B inst✝¹.toQuiver (fun a b ↦ (homCategory a b).toQuiver) C inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) (F.comp (id C)).toPrelaxFunctorStruct ≍
    @PrelaxFunctorStruct.map₂ B inst✝¹.toQuiver (fun a b ↦ (homCategory a b).toQuiver) C inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) F.toPrelaxFunctorStruct

case mapId
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ (F.comp (id C)).mapId ≍ F.mapId

case mapComp
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @LaxFunctor.mapComp B inst✝¹ C inst✝ (F.comp (id C)).toLaxFunctor ≍
    @LaxFunctor.mapComp B inst✝¹ C inst✝ F.toLaxFunctor
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: case obj
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
x✝ : B
⊢ ((id B).comp F).obj x✝ = F.obj x✝

pp: case map
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @Prefunctor.map B inst✝¹.toQuiver C inst✝.toQuiver ((id B).comp F).toPrefunctor ≍
    @Prefunctor.map B inst✝¹.toQuiver C inst✝.toQuiver F.toPrefunctor

pp: case map₂
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @PrelaxFunctorStruct.map₂ B inst✝¹.toQuiver (fun a b ↦ (homCategory a b).toQuiver) C inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) ((id B).comp F).toPrelaxFunctorStruct ≍
    @PrelaxFunctorStruct.map₂ B inst✝¹.toQuiver (fun a b ↦ (homCategory a b).toQuiver) C inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) F.toPrelaxFunctorStruct

pp: case mapId
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ ((id B).comp F).mapId ≍ F.mapId

pp: case mapComp
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @LaxFunctor.mapComp B inst✝¹ C inst✝ ((id B).comp F).toLaxFunctor ≍
    @LaxFunctor.mapComp B inst✝¹ C inst✝ F.toLaxFunctor

Tactic:
· simp

Goal state after:
case map
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @Prefunctor.map B inst✝¹.toQuiver C inst✝.toQuiver ((id B).comp F).toPrefunctor ≍
    @Prefunctor.map B inst✝¹.toQuiver C inst✝.toQuiver F.toPrefunctor

case map₂
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @PrelaxFunctorStruct.map₂ B inst✝¹.toQuiver (fun a b ↦ (homCategory a b).toQuiver) C inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) ((id B).comp F).toPrelaxFunctorStruct ≍
    @PrelaxFunctorStruct.map₂ B inst✝¹.toQuiver (fun a b ↦ (homCategory a b).toQuiver) C inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) F.toPrelaxFunctorStruct

case mapId
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ ((id B).comp F).mapId ≍ F.mapId

case mapComp
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @LaxFunctor.mapComp B inst✝¹ C inst✝ ((id B).comp F).toLaxFunctor ≍
    @LaxFunctor.mapComp B inst✝¹ C inst✝ F.toLaxFunctor
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
obj : B → C
map : {X Y : B} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id : ∀ (X : B), map (𝟙 X) = 𝟙 (obj X)
map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (map f ⟶ map g)
map₂_id : ∀ {a b : B} (f : a ⟶ b), map₂ (𝟙 f) = 𝟙 (map f)
map₂_comp : ∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h), map₂ (η ≫ θ) = map₂ η ≫ map₂ θ
mapComp : {a b c : B} → (f : a ⟶ b) → (g : b ⟶ c) → map (f ≫ g) ≅ map f ≫ map g
map₂_whisker_left :
  ∀ {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h),
    map₂ (f ◁ η) = (mapComp f g).hom ≫ map f ◁ map₂ η ≫ (mapComp f h).inv
map₂_whisker_right :
  ∀ {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
    map₂ (η ▷ h) = (mapComp f h).hom ≫ map₂ η ▷ map h ≫ (mapComp g h).inv
map₂_left_unitor : ∀ {a b : B} (f : a ⟶ b), map₂ (λ_ f).hom = (mapComp (𝟙 a) f).hom ≫ eqToHom ⋯ ≫ (λ_ (map f)).hom
a b : B
f : a ⟶ b
⊢ map f ≫ map (𝟙 b) = map f ≫ 𝟙 (obj b)

Tactic:
by rw [map_id b]

Goal state after:
Module: Mathlib.Topology.Sheaves.Over

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
U : Opens X
A : Type u_1
inst✝ : Category.{v_1, u_1} A
V : Over U
⊢ ((𝟭 (Over U)).obj V).left =
    (({ obj := fun V ↦ { carrier := Subtype.val ⁻¹' ↑V.left, is_open' := ⋯ }, map := fun {X_1 Y} f ↦ homOfLE ⋯,
              map_id := ⋯, map_comp := ⋯ } ⋙
            { obj := fun W ↦ Over.mk (homOfLE ⋯), map := fun {X_1 Y} f ↦ Over.homMk (homOfLE ⋯) ⋯, map_id := ⋯,
              map_comp := ⋯ }).obj
        V).left

Tactic:
ext x
    dsimp
    simp only [SetLike.mem_coe, Set.mem_image, Set.mem_preimage,
      Subtype.exists, exists_and_left, exists_prop, exists_eq_right_right, iff_self_and]
    apply leOfHom V.hom

Goal state after:
Module: Mathlib.Topology.Sheaves.Module

Goal state before:
pp: X : TopCat
U : Opens ↑X
R : TopCat.Sheaf RingCat X
⊢ SheafOfModules (Sheaf.over R U) ≌ SheafOfModules (U.sheafRestrict.obj R)

Tactic:
by
  refine SheafOfModules.pushforwardPushforwardEquivalence (eqv := U.overEquivalence.symm)
    (U.overPullbackSheafEquivOver.app _).inv (U.sheafRestrictSheafEquivOver.app _).inv rfl ?_
  ext : 2
  simp [overPullbackSheafEquivOver, sheafRestrictSheafEquivOver, eqToHom_map, overEquivalence,
    IsOpenMap.functor]

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

Goal state before:
pp: case h.succ
R : Type u
S : Type (max u v)
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
p : Ideal R
inst✝ : p.IsPrime
this : IsArtinianRing (p.ResidueField ⊗[R] S)
hpSfin : (p.primesOver S).Finite
n : ℕ
IH :
  ∀ m < n + 1,
    ∀ {R : Type u} {S : Type (max u v)} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
      [Module.Finite R S] (p : Ideal R) [inst_4 : p.IsPrime],
      (p.primesOver S).ncard = m →
        ∃ R' x x_1,
          ∃ (_ : Etale R R'),
            ∃ P,
              ∃ (x_3 : P.IsPrime) (x_4 : P.LiesOver p),
                ∃ n e,
                  ∃ (_ : CompleteOrthogonalIdempotents e),
                    ∃ P',
                      ∃ (_ : ∀ (i : Fin n), (P' i).IsPrime) (_ : ∀ (i : Fin n), (P' i).LiesOver P),
                        Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) ∧
                          (∀ (i : Fin n), e i.castSucc ∉ P' i) ∧
                            ∀ (P'' : Ideal (R' ⊗[R] S)),
                              P''.IsPrime →
                                P''.LiesOver P → e (Fin.last n) ∈ P'' ∧ ∀ (i : Fin n), e i.castSucc ∉ P'' → P'' = P' i
h : (p.primesOver S).ncard = n + 1
⊢ ∃ R' x x_1,
    ∃ (_ : Etale R R'),
      ∃ P,
        ∃ (x_3 : P.IsPrime) (x_4 : P.LiesOver p),
          ∃ n e,
            ∃ (_ : CompleteOrthogonalIdempotents e),
              ∃ P',
                ∃ (_ : ∀ (i : Fin n), (P' i).IsPrime) (_ : ∀ (i : Fin n), (P' i).LiesOver P),
                  Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) ∧
                    (∀ (i : Fin n), e i.castSucc ∉ P' i) ∧
                      ∀ (P'' : Ideal (R' ⊗[R] S)),
                        P''.IsPrime →
                          P''.LiesOver P → e (Fin.last n) ∈ P'' ∧ ∀ (i : Fin n), e i.castSucc ∉ P'' → P'' = P' i

Tactic:
| succ n =>

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

Goal state before:
pp: R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
a : S
s : Finset S
has : a ∉ s
S' : Type u
w✝⁴ : CommRing S'
w✝³ : Algebra R S'
w✝² : Module.Finite R S'
w✝¹ : Free R S'
w✝ : Algebra.FinitePresentation R S'
f : S' →ₐ[R] S
hsf : ↑s ⊆ ↑f.range
ha : IsIntegral R a
this✝ : Module.Finite S' (AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a)))
this : Free S' (AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a)))
algInst✝ : Algebra S' S := f.toAlgebra
⊢ Polynomial.eval₂ (↑(Algebra.ofId S' S)) a (Polynomial.map (algebraMap R S') (minpoly R a)) = 0

Tactic:
by simp [← Polynomial.aeval_def]

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

Goal state before:
pp: R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : Module.Flat R S
x : PrimeSpectrum R
⊢ (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap R S))).finrank x = Module.rankAtStalk S x

pp: case hf₁
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : Module.Flat R S
x : PrimeSpectrum R
⊢ (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap R S))).Finite

pp: case hf₂
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : Module.Flat R S
x : PrimeSpectrum R
⊢ (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap R S))).Flat

Tactic:
· simp

Goal state after:
case hf₁
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : Module.Flat R S
x : PrimeSpectrum R
⊢ (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap R S))).Finite

case hf₂
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : Module.Flat R S
x : PrimeSpectrum R
⊢ (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap R S))).Flat
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
R : CommRingCat
g : Spec R ⟶ Y
w✝ : IsOpenImmersion g
y : ↥(Spec R)
this : Nontrivial ↑R
⊢ Module.rankAtStalk (↑R) y = 1

pp: case hf₁
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
R : CommRingCat
g : Spec R ⟶ Y
w✝ : IsOpenImmersion g
y : ↥(Spec R)
this : Nontrivial ↑R
⊢ (CommRingCat.Hom.hom (𝟙 R)).Finite

pp: case hf₂
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
R : CommRingCat
g : Spec R ⟶ Y
w✝ : IsOpenImmersion g
y : ↥(Spec R)
this : Nontrivial ↑R
⊢ (CommRingCat.Hom.hom (𝟙 R)).Flat

Tactic:
· simp

Goal state after:
case hf₁
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
R : CommRingCat
g : Spec R ⟶ Y
w✝ : IsOpenImmersion g
y : ↥(Spec R)
this : Nontrivial ↑R
⊢ (CommRingCat.Hom.hom (𝟙 R)).Finite

case hf₂
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
R : CommRingCat
g : Spec R ⟶ Y
w✝ : IsOpenImmersion g
y : ↥(Spec R)
this : Nontrivial ↑R
⊢ (CommRingCat.Hom.hom (𝟙 R)).Flat
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
h : finrank f = 1
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f], finrank f = 1 → (∃ R, Y = Spec R) → IsIso f
hY : ¬∃ R, Y = Spec R
⊢ IsIso f

pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
h : finrank f = 1
hY : ∃ R, Y = Spec R
⊢ IsIso f

Tactic:
· rw [← MorphismProperty.isomorphisms.iff,
      IsZariskiLocalAtTarget.iff_of_openCover (P := .isomorphisms Scheme) Y.affineCover]
    intro i
    dsimp [Scheme.Cover.pullbackHom]
    refine this _ ?_ ⟨_, rfl⟩
    ext y
    rw [finrank_pullback_snd, h, Pi.one_apply, Pi.one_apply]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
h : finrank f = 1
hY : ∃ R, Y = Spec R
⊢ IsIso f
Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f],
    (∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) → (∃ R, Y = Spec R) → Smooth f
h : ¬∃ R, Y = Spec R
⊢ Smooth f

pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
h : ∃ R, Y = Spec R
⊢ Smooth f

Tactic:
· rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @Smooth) Y.affineCover]
    intro i
    dsimp [Scheme.Cover.pullbackHom]
    refine this _ (fun y ↦ ?_) ⟨_, rfl⟩
    apply MorphismProperty.of_isPullback
    · exact isPullback_fiberToSpecResidueField_of_isPullback (IsPullback.of_hasPullback _ _) _
    · infer_instance

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
h : ∃ R, Y = Spec R
⊢ Smooth f
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : KrullDimLE 1 R
x : R
hx : x ∈ nonZeroDivisors R
⊢ Order.krullDim (PrimeSpectrum (R ⧸ span {x})) ≤ ↑0

Tactic:
← ENat.WithBot.add_le_add_one_right_iff,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : KrullDimLE 1 R
x : R
hx : x ∈ nonZeroDivisors R
⊢ Order.krullDim (PrimeSpectrum (R ⧸ span {x})) + 1 ≤ ↑0 + 1
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: R : Type u_2
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : KrullDimLE 1 R
inst✝ : Nontrivial R
x : ↥R⁰
⊢ ↑(Multiplicative.ofAdd ↑(↑((ord R ↑x).lift ⋯)).toNat) = ↑(Multiplicative.ofAdd ↑((ord R ↑x).lift ⋯))

Tactic:
ENat.natCast_lift,

Goal state after:
R : Type u_2
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : KrullDimLE 1 R
inst✝ : Nontrivial R
x : ↥R⁰
⊢ ↑(Multiplicative.ofAdd ↑(ord R ↑x).toNat) = ↑(Multiplicative.ofAdd ↑((ord R ↑x).lift ⋯))
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
l' : a ⟶ b
r' : b ⟶ a
adj' : l' ⊣ r'
φ : l' ⟶ l
⊢ (conjugateEquiv adj (adj'.comp (Adjunction.id b))) ((ρ_ l').hom ≫ φ) = (conjugateEquiv adj adj') φ ≫ (λ_ r').inv

Tactic:
simp only [conjugateEquiv_apply, Category.assoc, mateEquiv_comp_id_right, id_whiskerLeft,
    Iso.inv_hom_id, Category.comp_id, Iso.hom_inv_id, Iso.cancel_iso_inv_left,
    EmbeddingLike.apply_eq_iff_eq]

Goal state after:
B : Type u
inst✝ : Bicategory B
a b : B
l : a ⟶ b
r : b ⟶ a
adj : l ⊣ r
l' : a ⟶ b
r' : b ⟶ a
adj' : l' ⊣ r'
φ : l' ⟶ l
⊢ (ρ_ (𝟙 a ≫ l')).inv ≫ (α_ (𝟙 a) l' (𝟙 b)).hom ≫ (λ_ (l' ≫ 𝟙 b)).hom ≫ (ρ_ l').hom ≫ φ ≫ (ρ_ l).inv =
    (λ_ l').hom ≫ φ ≫ (ρ_ l).inv
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
𝒜 : ι → σ
x : Submonoid A
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝒜
𝔭 : Ideal A
inst✝ : 𝔭.IsPrime
r : 0 = 1
⊢ False

Tactic:
by simp [ext_iff_val, val_zero, val_one, zero_ne_one] at r

Goal state after:
Module: Mathlib.RingTheory.Valuation.Integral

Goal state before:
pp: case neg.refine_2
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : R
a✝ : Nontrivial R
this : Nontrivial O
f : O[X]
hm : f.Monic
hn : ¬f.natDegree = 0
hf : 1 < v x
⊢ ∀ i ∈ Finset.range f.natDegree, v ((algebraMap O R) (f.coeff i) * x ^ i) < v x ^ f.natDegree

Tactic:
simp only [Finset.mem_range, map_mul, map_pow]

Goal state after:
case neg.refine_2
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : R
a✝ : Nontrivial R
this : Nontrivial O
f : O[X]
hm : f.Monic
hn : ¬f.natDegree = 0
hf : 1 < v x
⊢ ∀ i < f.natDegree, v ((algebraMap O R) (f.coeff i)) * v x ^ i < v x ^ f.natDegree
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case h
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
g : ↑R
hg : basicOpen g ≤ V
hV : Aux M V
f : ↑R
hfg : basicOpen f ≤ basicOpen g
s : ↑Γ(M, basicOpen f)
n : ℕ
t : ↑Γ(M, V)
ht : (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) t = f ^ n • s
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE hfg).op)) ((ConcreteCategory.hom (M.presheaf.map (homOfLE hg).op)) t) =
    f ^ n • s

Tactic:
simp [← M.presheaf.map_comp_apply, ← op_comp, homOfLE_comp, ht]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : (topologically @SpecializingMap).universally f
R : Type u
commRing✝ : CommRing R
domain✝ : IsDomain R
valuationRing✝ : ValuationRing R
K : Type u
field✝ : Field K
algebra✝ : Algebra R K
isFractionRing✝ : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this✝ : IsDomain ↑(CommRingCat.of R)
this : ValuationRing ↑(CommRingCat.of R)
⊢ ⋯.HasLift

Tactic:
let : Field (CommRingCat.of K) := ‹_›

Goal state after:
X Y : Scheme
f : X ⟶ Y
H : (topologically @SpecializingMap).universally f
R : Type u
commRing✝ : CommRing R
domain✝ : IsDomain R
valuationRing✝ : ValuationRing R
K : Type u
field✝ : Field K
algebra✝ : Algebra R K
isFractionRing✝ : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this✝¹ : IsDomain ↑(CommRingCat.of R)
this✝ : ValuationRing ↑(CommRingCat.of R)
this : Field ↑(CommRingCat.of K) := field✝
⊢ ⋯.HasLift
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
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e :
  (algebraMap A (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) (↑z.den * ↑y.num) =
    (algebraMap A (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) (↑y.den * ↑z.num)
c : A
hcx : c ∈ (↑x).asHomogeneousIdeal.toIdeal.primeCompl
hc : ↑⟨c, hcx⟩ * (↑z.den * ↑y.num) = ↑⟨c, hcx⟩ * (↑y.den * ↑z.num)
⊢ ∃ i, ∃ c ∈ 𝒜 i, c ∉ (↑x).asHomogeneousIdeal ∧ c * (↑z.den * ↑y.num) = c * (↑y.den * ↑z.num)

Tactic:
obtain ⟨i, hi⟩ := not_forall.mp ((x.1.1.isHomogeneous.mem_iff _).not.mp hcx)

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e :
  (algebraMap A (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) (↑z.den * ↑y.num) =
    (algebraMap A (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) (↑y.den * ↑z.num)
c : A
hcx : c ∈ (↑x).asHomogeneousIdeal.toIdeal.primeCompl
hc : ↑⟨c, hcx⟩ * (↑z.den * ↑y.num) = ↑⟨c, hcx⟩ * (↑y.den * ↑z.num)
i : ℕ
hi : ↑(((decompose 𝒜) c) i) ∉ (↑x).asHomogeneousIdeal.toIdeal
⊢ ∃ i, ∃ c ∈ 𝒜 i, c ∉ (↑x).asHomogeneousIdeal ∧ c * (↑z.den * ↑y.num) = c * (↑y.den * ↑z.num)