mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: case refine_2.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 V : (directedCover Y).I₀
i : U ⟶ V
⊢ CommRingCat.ofHom
        ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ ↑V) (f ⁻¹ᵁ toOpens V) ⋯)).codRestrict
          (integralClosure ↑Γ(Y, toOpens V) ↑Γ(X, f ⁻¹ᵁ toOpens V)) ⋯) ≫
      (normalizationDiagram f).map ((toOpensFunctor Y).map i).op =
    T.presheaf.map (homOfLE ⋯).op ≫
      CommRingCat.ofHom
        ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ ↑U) (f ⁻¹ᵁ toOpens U) ⋯)).codRestrict
          (integralClosure ↑Γ(Y, toOpens U) ↑Γ(X, f ⁻¹ᵁ toOpens U)) ⋯)

Tactic:
ext i

Goal state after:
case refine_2.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 V : (directedCover Y).I₀
i✝ : U ⟶ V
i : ↑(CommRingCat.of ↑(T.presheaf.1 (Opposite.op (f₂ ⁻¹ᵁ ↑V))))
⊢ (CommRingCat.Hom.hom
        (CommRingCat.ofHom
            ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ ↑V) (f ⁻¹ᵁ toOpens V) ⋯)).codRestrict
              (integralClosure ↑Γ(Y, toOpens V) ↑Γ(X, f ⁻¹ᵁ toOpens V)) ⋯) ≫
          (normalizationDiagram f).map ((toOpensFunctor Y).map i✝).op))
      i =
    (CommRingCat.Hom.hom
        (T.presheaf.map (homOfLE ⋯).op ≫
          CommRingCat.ofHom
            ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ ↑U) (f ⁻¹ᵁ toOpens U) ⋯)).codRestrict
              (integralClosure ↑Γ(Y, toOpens U) ↑Γ(X, f ⁻¹ᵁ toOpens U)) ⋯)))
      i
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₀
⊢ 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)) ⋯) =
    (normalizationDiagramMap f).app (Opposite.op (toOpens U))

Tactic:
ext i

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₂ (↑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)
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst✝ : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U : (normalizationOpenCover f).I₀
this : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
⊢ (normalizationOpenCover f).f U ≫ f₁ = (normalizationOpenCover f).f U ≫ f₂

Tactic:
have : IsAffineHom f₁ := have : IsAffineHom (f₁ ≫ g) := hf₁ ▸ inferInstance; .of_comp _ g

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst✝ : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U : (normalizationOpenCover f).I₀
this✝ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this : IsAffineHom f₁
⊢ (normalizationOpenCover f).f U ≫ f₁ = (normalizationOpenCover f).f U ≫ f₂
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

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
n m k : ℕ
hn : n = m + k
f : MvPolynomial (Fin n) R →ₐ[R] S
⊢ (fun p ↦ aeval fun x ↦ (↑p).coeff ↑x) ((fun f ↦ (MonicDegreeEq.freeMonic R n).map f.toRingHom) f) = f

Tactic:
ext i

Goal state after:
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
n m k : ℕ
hn : n = m + k
f : MvPolynomial (Fin n) R →ₐ[R] S
i : Fin n
⊢ ((fun p ↦ aeval fun x ↦ (↑p).coeff ↑x) ((fun f ↦ (MonicDegreeEq.freeMonic R n).map f.toRingHom) f)) (X i) = f (X i)
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

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
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq S n
this : ∀ i ≥ n, (if i = n then 1 else 0) = (↑p).coeff i
⊢ (fun f ↦ (MonicDegreeEq.freeMonic R n).map f.toRingHom) ((fun p ↦ aeval fun x ↦ (↑p).coeff ↑x) p) = p

Tactic:
ext i

Goal state after:
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
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq S n
this : ∀ i ≥ n, (if i = n then 1 else 0) = (↑p).coeff i
i : ℕ
⊢ (↑((fun f ↦ (MonicDegreeEq.freeMonic R n).map f.toRingHom) ((fun p ↦ aeval fun x ↦ (↑p).coeff ↑x) p))).coeff i =
    (↑p).coeff i
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
m : ℕ
hm : f.natDegree ≤ m
hg : ∏ i ∈ s, (g i).leadingCoeff ≠ 0
⊢ f.resultant (∏ i ∈ s, g i) m = ∏ i ∈ s, f.resultant (g i) m

Tactic:
simp_rw [resultant_comm f]
  rw [resultant_prod_left _ _ _ _ hg hm, Finset.prod_mul_distrib, Finset.prod_pow_eq_pow_sum,
    ← Finset.mul_sum, natDegree_prod' _ _ hg]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
this✝¹ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
this✝ : IsDomain (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ)
this : Algebra (MvPolynomial (Fin n) ℤ) (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) :=
  (universalFactorizationMap ℤ n m k hn).toAlgebra
F : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ →ₐ[ℤ] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId ℤ R)))
    ((AlgHom.restrictScalars ℤ Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId ℤ R))) ⋯
H₁ : ∀ (i : Fin m), (universalFactorizationMap R n m k hn).IsIntegralElem (X i ⊗ₜ[R] 1)
H₂ : ∀ (i : Fin k), (universalFactorizationMap R n m k hn).IsIntegralElem (1 ⊗ₜ[R] X i)
x : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R
⊢ (universalFactorizationMap R n m k hn).IsIntegralElem x

Tactic:
induction x with

Goal state after:
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
this✝ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
this : Algebra (MvPolynomial (Fin n) R) R := ((MvPolynomial.mapEquivMonic R R n).symm p).toAlgebra
⊢ (fromTensor m k hn p).comp (MvPolynomial.universalFactorizationMap R n m k hn) =
    (Algebra.ofId R 𝓡).comp ((MvPolynomial.mapEquivMonic R R n).symm p)

Tactic:
exact AlgHom.ext fun x ↦ (Algebra.TensorProduct.tmul_one_eq_one_tmul x).symm

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

Goal state before:
pp: case inr
K : Type u_2
inst✝ : Field K
f g : K[X]
hf : f ≠ 0
H : (C f.leadingCoeff⁻¹ * f).Monic
this :
  IsUnit (f.leadingCoeff⁻¹ ^ g.natDegree) ∧ IsUnit (f.resultant g (C f.leadingCoeff⁻¹ * f).natDegree) ↔
    IsCoprime (C f.leadingCoeff⁻¹ * f) g
⊢ f.resultant g = 0 ↔ (f ≠ 0 ∨ g ≠ 0) ∧ ¬IsCoprime f g

Tactic:
natDegree_C_mul (by simp [hf]),

Goal state after:
case inr
K : Type u_2
inst✝ : Field K
f g : K[X]
hf : f ≠ 0
H : (C f.leadingCoeff⁻¹ * f).Monic
this : IsUnit (f.leadingCoeff⁻¹ ^ g.natDegree) ∧ IsUnit (f.resultant g) ↔ IsCoprime (C f.leadingCoeff⁻¹ * f) g
⊢ f.resultant g = 0 ↔ (f ≠ 0 ∨ g ≠ 0) ∧ ¬IsCoprime f g
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝¹⁰ : Nonempty ↥G.left
this✝⁹ : IsProper (G ⊗ G).hom
this✝⁸ : JacobsonSpace ↥(G ⊗ G).left
this✝⁷ : Surjective G.hom
this✝⁶ : IsProper (Over.Hom.left (fst G G))
this✝⁵ : Surjective (Over.Hom.left (fst G G))
this✝⁴ : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this✝³ : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝² : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝¹ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this✝ : IsProper (Over.Hom.left γ)
H :
  (⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} \
      ⇑(Over.Hom.left γ) ⁻¹' {(Over.Hom.left (lift η η)) point}).Nonempty
c : Spec (CommRingCat.of K) ⟶ (G ⊗ G).left
hc : c ≫ (G ⊗ G).hom = 𝟙 (Spec (CommRingCat.of K))
hc₃ : c point ∈ closedPoints ↥(G ⊗ G).left
hc₁ : c point ∈ ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point}
hc₂ : c point ∉ ⇑(Over.Hom.left γ) ⁻¹' {(Over.Hom.left (lift η η)) point}
e : (pointEquivClosedPoint (G ⊗ G).hom) ⟨c, hc⟩ = ⟨c point, hc₃⟩
fc : 𝟙_ (Over S) ⟶ 𝟙_ (Over S) ⊗ G := lift (𝟙 (𝟙_ (Over S))) (Over.homMk c hc ≫ snd G G)
this : c ≫ pullback.fst G.hom G.hom = Over.Hom.left η
H₁ : c = Over.Hom.left fc ≫ Over.Hom.left (η ▷ G)
⊢ fc ≫ η ▷ G ≫ γ = lift η η

Tactic:
ext1 <;> simp [fc, γ, S]

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

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
inst✝ : Module.FaithfullyFlat R S
I : Ideal R
hI : (Ideal.map (algebraMap R S) I).FG
f : S ⊗[R] ↥I →ₗ[S] S := ↑(AlgebraTensorModule.rid R S S) ∘ₗ (AlgebraTensorModule.lTensor S S) (Submodule.subtype I)
hf : Function.Injective ⇑f
x : S ⊗[R] ↥I
⊢ f x ∈ Ideal.map (algebraMap R S) I

Tactic:
induction x with

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

Goal state before:
pp: case left
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Module.FaithfullyFlat R T
inst✝ : Smooth T (T ⊗[R] S)
this : FinitePresentation R S
x✝ : Algebra T (S ⊗[R] T) := TensorProduct.rightAlgebra
⊢ Module.Projective S Ω[S⁄R]

Tactic:
let e : S ⊗[R] T ≃ₐ[T] T ⊗[R] S :=
      .ofRingEquiv (f := TensorProduct.comm R S T) <| by simp [RingHom.algebraMap_toAlgebra]

Goal state after:
case left
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Module.FaithfullyFlat R T
inst✝ : Smooth T (T ⊗[R] S)
this : FinitePresentation R S
x✝ : Algebra T (S ⊗[R] T) := TensorProduct.rightAlgebra
e : S ⊗[R] T ≃ₐ[T] T ⊗[R] S := AlgEquiv.ofRingEquiv ⋯
⊢ Module.Projective S Ω[S⁄R]
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: 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
t : T
x : S ⊗[P.Ring] Ω[P.Ring⁄R]
⊢ (P.tensorCotangentSpace T) (t ⊗ₜ[R] x) = t • (CotangentSpace.map (toBaseChange T)) x

Tactic:
induction x with

Goal state after:
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'
a b : B
f : a ⟶ b
⊢ 𝟙 (obj a) ≫ map f = map (𝟙 a) ≫ map f

Tactic:
rw [map_id a]

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

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
S : StrictPseudofunctorCore B C
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ S.map₂ (λ_ f).hom = (eqToIso ⋯).hom ≫ (eqToIso ⋯).hom ▷ S.map f ≫ (λ_ (S.map f)).hom

Tactic:
simpa using S.map₂_left_unitor f

Goal state after:
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
a b : B
f : a ⟶ b
⊢ map (𝟙 a) ≫ map f = 𝟙 (obj a) ≫ map f

Tactic:
rw [map_id a]

Goal state after:
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
S : StrictlyUnitaryPseudofunctorCore B C
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ S.map₂ (λ_ f).hom = (S.mapComp (𝟙 a✝) f).hom ≫ (eqToIso ⋯).hom ▷ S.map f ≫ (λ_ (S.map f)).hom

Tactic:
simpa using S.map₂_left_unitor f

Goal state after:
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
F : StrictlyUnitaryPseudofunctor B C
x : B
⊢ F.toLax.mapId x = eqToHom ⋯

Tactic:
by simp [F.mapId_eq_eqToIso]

Goal state after:
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : Function.Bijective ⇑g
h1 : f.Finite
h2 : f.Flat
x : PrimeSpectrum R
⊢ (g.comp f).finrank x = f.finrank x

Tactic:
algebraize [f, g, (g.comp f)]

Goal state after:
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : Function.Bijective ⇑g
h1 : f.Finite
h2 : f.Flat
x : PrimeSpectrum R
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Module.Finite R S
algebraizeInst✝ : Module.Flat R S
⊢ (g.comp f).finrank x = f.finrank x
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Bijective ⇑f
h1 : g.Finite
h2 : g.Flat
x : PrimeSpectrum S
⊢ (g.comp f).finrank (PrimeSpectrum.comap f x) = g.finrank x

Tactic:
algebraize [f, g, (g.comp f)]

Goal state after:
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Bijective ⇑f
h1 : g.Finite
h2 : g.Flat
x : PrimeSpectrum S
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Module.Finite S T
algebraizeInst✝ : Module.Flat S T
⊢ (g.comp f).finrank (PrimeSpectrum.comap f x) = g.finrank x
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

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

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @Surjective) Y.affineCover]

Goal state after:
case refine_1.inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
h : 1 ≤ finrank f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f], 1 ≤ finrank f → (∃ R, Y = Spec R) → Surjective f
hY : ¬∃ R, Y = Spec R
⊢ ∀ (i : Y.affineCover.toPreZeroHypercover.1), Surjective (Cover.pullbackHom Y.affineCover f i)
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:

Tactic:
_ = 𝟙 _ ⊗≫ r₁ ◁ g₁ ◁ adj₂.unit ▷ g₂ ⊗≫ r₁ ◁ α ▷ r₂ ▷ g₂ ⊗≫
          ((adj₁.counit ▷ (h₁ ≫ r₂ ≫ g₂ ≫ 𝟙 e)) ≫ 𝟙 b ◁ (h₁ ◁ r₂ ◁ g₂ ◁ adj₃.unit)) ⊗≫
            h₁ ◁ r₂ ◁ β ▷ r₃ ⊗≫ h₁ ◁ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 _ ⊗≫ r₁ ◁ g₁ ◁ adj₂.unit ▷ g₂ ⊗≫
          (r₁ ◁ (α ▷ (r₂ ≫ g₂ ≫ 𝟙 e) ≫ (l₁ ≫ h₁) ◁ r₂ ◁ g₂ ◁ adj₃.unit)) ⊗≫
            ((adj₁.counit ▷ (h₁ ≫ r₂) ▷ (g₂ ≫ l₃) ≫ (𝟙 b ≫ h₁ ≫ r₂) ◁ β) ▷ r₃) ⊗≫
              h₁ ◁ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 _ := by
      rw [← whisker_exchange]
      bicategory
    _ = 𝟙 _ ⊗≫ r₁ ◁ g₁ ◁ (adj₂.unit ▷ (g₂ ≫ 𝟙 e) ≫ (l₂ ≫ r₂) ◁ g₂ ◁ adj₃.unit) ⊗≫
          (r₁ ◁ (α ▷ (r₂ ≫ g₂ ≫ l₃) ≫ (l₁ ≫ h₁) ◁ r₂ ◁ β) ▷ r₃) ⊗≫
            (adj₁.counit ▷ h₁ ▷ (r₂ ≫ l₂) ≫ (𝟙 b ≫ h₁) ◁ adj₂.counit) ▷ h₂ ▷ r₃ ⊗≫ 𝟙 _ := by
      rw [← whisker_exchange, ← whisker_exchange]
      bicategory
    _ = 𝟙 _ ⊗≫ r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫
          r₁ ◁ g₁ ◁ (adj₂.unit ▷ (g₂ ≫ l₃) ≫ (l₂ ≫ r₂) ◁ β) ▷ r₃ ⊗≫
            r₁ ◁ (α ▷ (r₂ ≫ l₂) ≫ (l₁ ≫ h₁) ◁ adj₂.counit) ▷ h₂ ▷ r₃ ⊗≫
              adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 _ := by
      rw [← whisker_exchange, ← whisker_exchange, ← whisker_exchange]
      bicategory
    _ = 𝟙 _ ⊗≫ r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫ r₁ ◁ g₁ ◁ β ▷ r₃ ⊗≫
          ((r₁ ≫ g₁) ◁ leftZigzag adj₂.unit adj₂.counit ▷ (h₂ ≫ r₃)) ⊗≫
            r₁ ◁ α ▷ h₂ ▷ r₃ ⊗≫ adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 _ := by
      rw [← whisker_exchange, ← whisker_exchange]
      bicategory
    _ = _ := by
      rw [adj₂.left_triangle]
      bicategory

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x y : K
h1 : x + y ≠ 0
⊢ min ((ordFrac R) x) ((ordFrac R) y) ≤ (ordFrac R) (x + y)

Tactic:
simp only [ordFrac_eq_valuation_inv]

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x y : K
h1 : x + y ≠ 0
⊢ min ((valuation K (IsDiscreteValuationRing.maximalIdeal R)) x)⁻¹
      ((valuation K (IsDiscreteValuationRing.maximalIdeal R)) y)⁻¹ ≤
    ((valuation K (IsDiscreteValuationRing.maximalIdeal R)) (x + y))⁻¹
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: case pos
X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
z : ↥X
h : coheight z = 1
⊢ ord 0 z = 0 z

pp: case neg
X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
z : ↥X
h : ¬coheight z = 1
⊢ ord 0 z = 0 z

Tactic:
· simp [ord_eq_ordHom_of_coheight_eq_one h, unzeroD]

Goal state after:
case neg
X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
z : ↥X
h : ¬coheight z = 1
⊢ ord 0 z = 0 z
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u_2
R : ι → Type u_1
inst✝ : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
hs' : ∀ (i : ι), Ideal.span (⇑(Pi.evalRingHom (fun x ↦ R x) i) '' s) = ⊤
⊢ Ideal.span s = ⊤

Tactic:
simp only [Ideal.eq_top_iff_one, ← Subtype.range_val (s := s), ← Set.range_comp,
    Finsupp.mem_ideal_span_range_iff_exists_finsupp] at hs' ⊢

Goal state after:
ι : Type u_2
R : ι → Type u_1
inst✝ : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
hs' : ∀ (i : ι), ∃ c, (c.sum fun i_1 a ↦ a * (⇑(Pi.evalRingHom (fun x ↦ R x) i) ∘ Subtype.val) i_1) = 1
⊢ ∃ c, (c.sum fun i a ↦ a * ↑i) = 1
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u_2
R : ι → Type u_1
inst✝ : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
f : (i : ι) → { x // x ∈ s } →₀ R i
hf : ∀ (i : ι), ((f i).sum fun i_1 a ↦ a * (⇑(Pi.evalRingHom (fun x ↦ R x) i) ∘ Subtype.val) i_1) = 1
this : Fintype ↑s
⊢ ((Finsupp.equivFunOnFinite.symm fun i x ↦ (f x) i).sum fun i a ↦ a * ↑i) = 1

Tactic:
ext i

Goal state after:
ι : Type u_2
R : ι → Type u_1
inst✝ : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
f : (i : ι) → { x // x ∈ s } →₀ R i
hf : ∀ (i : ι), ((f i).sum fun i_1 a ↦ a * (⇑(Pi.evalRingHom (fun x ↦ R x) i) ∘ Subtype.val) i_1) = 1
this : Fintype ↑s
i : ι
⊢ (Finsupp.equivFunOnFinite.symm fun i x ↦ (f x) i).sum (fun i a ↦ a * ↑i) i = 1 i
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e f x y z : B
g₁ : a ⟶ d
h₁ : b ⟶ e
k₁ : c ⟶ f
g₂ : d ⟶ x
h₂ : e ⟶ y
k₂ : f ⟶ z
r₁ : b ⟶ a
r₂ : c ⟶ b
r₃ : e ⟶ d
r₄ : f ⟶ e
r₅ : y ⟶ x
r₆ : z ⟶ y
α : r₁ ≫ g₁ ⟶ h₁ ≫ r₃
β : r₂ ≫ h₁ ⟶ k₁ ≫ r₄
γ : r₃ ≫ g₂ ⟶ h₂ ≫ r₅
δ : r₄ ≫ h₂ ⟶ k₂ ≫ r₆
⊢ comp α β γ δ = hcomp (vcomp α γ) (vcomp β δ)

Tactic:
by
  dsimp only [comp, vcomp, hcomp]
  calc
    _ = 𝟙 _ ⊗≫ r₂ ◁ α ▷ g₂ ⊗≫ (β ▷ (r₃ ≫ g₂) ≫ (k₁ ≫ r₄) ◁ γ) ⊗≫ k₁ ◁ δ ▷ r₅ ⊗≫ 𝟙 _ := by
      bicategory
    _ = _ := by
      rw [← whisker_exchange]
      bicategory

Goal state after:
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
I : Ideal ((i : ι) → ↑(R i))
f : (∐ fun i ↦ Spec (R i)) ⟶ Spec (CommRingCat.of (((i : ι) → ↑(R i)) ⧸ I))
hf : f ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R
x : (i : ι) → ↑(R i)
hx : x ∈ I
⊢ x ∈ ⊥

Tactic:
ext i

Goal state after:
ι : Type u
R : ι → CommRingCat
I : Ideal ((i : ι) → ↑(R i))
f : (∐ fun i ↦ Spec (R i)) ⟶ Spec (CommRingCat.of (((i : ι) → ↑(R i)) ⧸ I))
hf : f ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R
x : (i : ι) → ↑(R i)
hx : x ∈ I
i : ι
⊢ x i = 0 i