mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : FiniteType R S
inst✝⁷ : CommRing R'
inst✝⁶ : Algebra R R'
inst✝⁵ : CommRing R''
inst✝⁴ : Algebra R R''
inst✝³ : Algebra R'' S
inst✝² : Algebra.IsIntegral R R''
inst✝¹ : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst✝ : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e : (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)) e₀ = e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' → P'' = Ideal.comap (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom P'
g : R''
hgq : (algebraMap R'' S) g ∉ q
hg : Function.Surjective ⇑(Localization.awayMap (algebraMap R'' S) g)
this✝ : Algebra.IsIntegral R' (Localization.Away e₀)
f : R'
hfP : f ∉ P
hf : (Localization.awayMapₐ (ofId R' (Localization.Away e)) f).Finite
φ : R' ⊗[R] S →ₐ[R'] Localization.Away f ⊗[R] S := TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)
algInst✝ : Algebra (R' ⊗[R] S) (Localization.Away f ⊗[R] S) := φ.toAlgebra
this : Submonoid.powers (f ⊗ₜ[R] 1) = algebraMapSubmonoid (R' ⊗[R] S) (Submonoid.powers f)
⊢ (algebraMap (R' ⊗[R] S) (Localization.Away f ⊗[R] S)).comp TensorProduct.includeRight.toRingHom =
    TensorProduct.includeRight.toRingHom

Tactic:
ext

Goal state after:
R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : FiniteType R S
inst✝⁷ : CommRing R'
inst✝⁶ : Algebra R R'
inst✝⁵ : CommRing R''
inst✝⁴ : Algebra R R''
inst✝³ : Algebra R'' S
inst✝² : Algebra.IsIntegral R R''
inst✝¹ : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst✝ : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e : (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)) e₀ = e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' → P'' = Ideal.comap (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom P'
g : R''
hgq : (algebraMap R'' S) g ∉ q
hg : Function.Surjective ⇑(Localization.awayMap (algebraMap R'' S) g)
this✝ : Algebra.IsIntegral R' (Localization.Away e₀)
f : R'
hfP : f ∉ P
hf : (Localization.awayMapₐ (ofId R' (Localization.Away e)) f).Finite
φ : R' ⊗[R] S →ₐ[R'] Localization.Away f ⊗[R] S := TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)
algInst✝ : Algebra (R' ⊗[R] S) (Localization.Away f ⊗[R] S) := φ.toAlgebra
this : Submonoid.powers (f ⊗ₜ[R] 1) = algebraMapSubmonoid (R' ⊗[R] S) (Submonoid.powers f)
x✝ : S
⊢ ((algebraMap (R' ⊗[R] S) (Localization.Away f ⊗[R] S)).comp TensorProduct.includeRight.toRingHom) x✝ =
    TensorProduct.includeRight.toRingHom x✝
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
Z : Scheme
inst✝¹ : IsOpenImmersion f
g : Y ⟶ Z
inst✝ : LocallyOfFiniteType g
⊢ quasiFiniteLocus (f ≫ g) = f ⁻¹ᵁ quasiFiniteLocus g

Tactic:
ext

Goal state after:
X Y : Scheme
f : X ⟶ Y
Z : Scheme
inst✝¹ : IsOpenImmersion f
g : Y ⟶ Z
inst✝ : LocallyOfFiniteType g
x✝ : ↥X
⊢ x✝ ∈ ↑(quasiFiniteLocus (f ≫ g)) ↔ x✝ ∈ ↑(f ⁻¹ᵁ quasiFiniteLocus g)
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: ⊢ @IsFinite = @IsProper ⊓ @LocallyQuasiFinite

Tactic:
ext

Goal state after:
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsFinite x✝ ↔ (@IsProper ⊓ @LocallyQuasiFinite) x✝
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: ⊢ @IsClosedImmersion = @IsProper ⊓ MorphismProperty.monomorphisms Scheme

Tactic:
ext

Goal state after:
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsClosedImmersion x✝ ↔ (@IsProper ⊓ MorphismProperty.monomorphisms Scheme) x✝
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FiniteType R S
p : Ideal R
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
inst✝¹ : q.LiesOver p
inst✝ : QuasiFiniteAt R q
R' : Type u
w✝⁶ : CommRing R'
w✝⁵ : Algebra R R'
w✝⁴ : Etale R R'
P : Ideal R'
w✝³ : P.IsPrime
w✝² : P.LiesOver p
e : R' ⊗[R] S
he : IsIdempotentElem e
e₀ : R' ⊗[R] ↥(integralClosure R S)
he₀ : IsIdempotentElem e₀
he₀e : (TensorProduct.map (AlgHom.id R' R') (integralClosure R S).val) e₀ = e
P' : Ideal (R' ⊗[R] S)
w✝¹ : P'.IsPrime
w✝ : P'.LiesOver P
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
heP' : e ∉ P'
hpP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
H' :
  ∀ (P'' : Ideal (R' ⊗[R] ↥(integralClosure R S))),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' → P'' = Ideal.comap (TensorProduct.map (AlgHom.id R' R') (integralClosure R S).val).toRingHom P'
H : ∀ (P'' : Ideal (R' ⊗[R] S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'
g : ↥(integralClosure R S)
hgq : ↑g ∉ q
hg : Function.Bijective ⇑(Localization.awayMap (integralClosure R S).val.toRingHom g)
f : R'
hfP : f ∉ P
hf :
  Module.Finite (Localization.Away f)
    (Localization.Away ((TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)) e))
Pf : Ideal (Localization.Away f) := Ideal.map (algebraMap R' (Localization.Away f)) P
this✝⁸ : Pf.IsPrime
this✝⁷ : Pf.LiesOver P
φ : R' ⊗[R] S →ₐ[R'] Localization.Away f ⊗[R] S := TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)
this✝⁶ : Algebra (R' ⊗[R] S) (Localization.Away f ⊗[R] S) := φ.toAlgebra
this✝⁵ : IsScalarTower R' (R' ⊗[R] S) (Localization.Away f ⊗[R] S) :=
  IsScalarTower.of_algebraMap_eq' (Eq.symm (AlgHom.comp_algebraMap φ))
this✝⁴ : IsLocalization.Away (f ⊗ₜ[R] 1) (Localization.Away f ⊗[R] S)
P'f : Ideal (Localization.Away f ⊗[R] S) := Ideal.map (algebraMap (R' ⊗[R] S) (Localization.Away f ⊗[R] S)) P'
hP'f : Disjoint ↑(Submonoid.powers (f ⊗ₜ[R] 1)) ↑P'
this✝³ : P'f.IsPrime
this✝² : P'f.LiesOver P'
this✝¹ : P'f.LiesOver P
this✝ : P'f.LiesOver Pf
this : Function.Bijective ⇑(Ideal.ResidueField.mapₐ P Pf (IsScalarTower.toAlgHom R R' (Localization.Away f)) ⋯)
⊢ Ideal.ResidueField.mapₐ p Pf (ofId R (Localization.Away f)) ⋯ =
    (Ideal.ResidueField.mapₐ P Pf (IsScalarTower.toAlgHom R R' (Localization.Away f)) ⋯).comp
      (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)

Tactic:
ext

Goal state after:
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 ⇑(↑R I.cotangentToQuotientSquare)

Tactic:
apply cotangentToQuotientSquare_injective

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

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
inst✝¹ : Module.FaithfullyFlat R T
inst✝ : FormallyUnramified T (T ⊗[R] S)
⊢ FormallyUnramified R S

Tactic:
constructor

Goal state after:
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✝ : FormallyUnramified T (T ⊗[R] S)
⊢ Subsingleton Ω[S⁄R]
Module: Mathlib.RingTheory.Etale.Descent

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
inst✝¹ : Module.FaithfullyFlat R T
inst✝ : Smooth T (T ⊗[R] S)
this : FinitePresentation R S
⊢ Module.Projective S Ω[S⁄R] ∧ Subsingleton (H1Cotangent R S)

Tactic:
constructor

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
⊢ Module.Projective S Ω[S⁄R]

case right
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
⊢ Subsingleton (H1Cotangent R S)
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
⊢ Module.Projective S Ω[S⁄R]

pp: case right
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
⊢ Subsingleton (H1Cotangent R S)

Tactic:
· let _ : Algebra T (S ⊗[R] T) := TensorProduct.rightAlgebra
    let e : S ⊗[R] T ≃ₐ[T] T ⊗[R] S :=
      .ofRingEquiv (f := TensorProduct.comm R S T) <| by simp [RingHom.algebraMap_toAlgebra]
    have : FormallySmooth T (S ⊗[R] T) := .of_equiv e.symm
    let e' : (S ⊗[R] T) ⊗[S] Ω[S⁄R] ≃ₗ[S ⊗[R] T] Ω[S ⊗[R] T⁄T] :=
      KaehlerDifferential.tensorKaehlerEquiv R T S (S ⊗[R] T)
    have : Module.Flat (S ⊗[R] T) ((S ⊗[R] T) ⊗[S] Ω[S⁄R]) := .of_linearEquiv e'
    have : Module.Flat S Ω[S⁄R] := Module.Flat.of_flat_tensorProduct _ _ (S ⊗[R] T)
    exact Module.Flat.projective_of_finitePresentation

Goal state after:
case right
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
⊢ Subsingleton (H1Cotangent R S)
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: case hc₃
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
⊢ ↑R h1Cotangentι ∘ₗ ↑R (P.tensorToH1Cotangent T) =
    ↑(LinearEquiv.restrictScalars R (P.tensorCotangentOfFlat T)) ∘ₗ LinearMap.lTensor T (↑R h1Cotangentι)

Tactic:
ext

Goal state after:
case hc₃
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
x✝¹ : T
x✝ : P.H1Cotangent
⊢ (((AlgebraTensorModule.curry (↑R h1Cotangentι ∘ₗ ↑R (P.tensorToH1Cotangent T))) x✝¹) x✝).val =
    (((AlgebraTensorModule.curry
            (↑(LinearEquiv.restrictScalars R (P.tensorCotangentOfFlat T)) ∘ₗ LinearMap.lTensor T (↑R h1Cotangentι)))
          x✝¹)
        x✝).val
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: case hc₄
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
⊢ ↑R P.baseChange.cotangentComplex ∘ₗ ↑(LinearEquiv.restrictScalars R (P.tensorCotangentOfFlat T)) =
    ↑(LinearEquiv.restrictScalars R (P.tensorCotangentSpace T)) ∘ₗ LinearMap.lTensor T (↑R P.cotangentComplex)

Tactic:
ext

Goal state after:
case hc₄
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
x✝¹ : T
x✝ : P.Cotangent
⊢ ((AlgebraTensorModule.curry
          (↑R P.baseChange.cotangentComplex ∘ₗ ↑(LinearEquiv.restrictScalars R (P.tensorCotangentOfFlat T))))
        x✝¹)
      x✝ =
    ((AlgebraTensorModule.curry
          (↑(LinearEquiv.restrictScalars R (P.tensorCotangentSpace T)) ∘ₗ LinearMap.lTensor T (↑R P.cotangentComplex)))
        x✝¹)
      x✝
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u
S : Type (max u v)
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra R S
p : Ideal R
inst✝¹⁶ : p.IsPrime
q : Ideal S
R' : Type u
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : Algebra R R'
inst✝¹³ : Etale R R'
P : Ideal R'
inst✝¹² : P.IsPrime
inst✝¹¹ : P.LiesOver p
e : R' ⊗[R] S
P' : Ideal (R' ⊗[R] S)
inst✝¹⁰ : P'.IsPrime
inst✝⁹ : P'.LiesOver P
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
heP' : e ∉ P'
hpP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
H : ∀ (P'' : Ideal (R' ⊗[R] S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'
R'' : Type u
inst✝⁸ : CommRing R''
inst✝⁷ : Algebra R' R''
inst✝⁶ : Algebra R R''
inst✝⁵ : IsScalarTower R R' R''
inst✝⁴ : Etale R' R''
Q : Ideal R''
inst✝³ : Q.IsPrime
inst✝² : Q.LiesOver P
n : ℕ
e' : Fin (n + 1 + 1) → R'' ⊗[R] S
he' : CompleteOrthogonalIdempotents e'
he'0 : e' 0 = (TensorProduct.map (ofId R' R'') (AlgHom.id R S)) e
Q' : Fin n → Ideal (R'' ⊗[R] S)
inst✝¹ : ∀ (i : Fin n), (Q' i).IsPrime
inst✝ : ∀ (i : Fin n), (Q' i).LiesOver Q
hPQ : Function.Bijective ⇑(Ideal.ResidueField.mapₐ P Q (ofId R' R'') ⋯)
hQ' : ∀ (i : Fin n), e' i.succ.castSucc ∉ Q' i
H' :
  ∀ (P'' : Ideal (R'' ⊗[R] S)),
    e' 0 ∈ P'' →
      P''.IsPrime → P''.LiesOver Q → e' (Fin.last (n + 1)) ∈ P'' ∧ ∀ (i : Fin n), e' i.succ.castSucc ∉ P'' → P'' = Q' i
φ : R' ⊗[R] S →ₐ[R'] R'' ⊗[R] S := TensorProduct.map (ofId R' R'') (AlgHom.id R S)
this : Q.LiesOver p
⊢ Ideal.ResidueField.mapₐ p Q (ofId R R'') ⋯ =
    (AlgHom.restrictScalars R (Ideal.ResidueField.mapₐ P Q (ofId R' R'') ⋯)).comp
      (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)

Tactic:
ext

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

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst✝³ : LocallyOfFiniteType f
inst✝² : GrpObj (Over.mk f)
inst✝¹ : IsReduced G
inst✝ : IsAlgClosed K
this✝ : JacobsonSpace ↥G
this : Nonempty ↥G
H : (↑(Scheme.Hom.smoothLocus f))ᶜ.Nonempty
x : ↥G
hx : x ∈ (↑(Scheme.Hom.smoothLocus f))ᶜ
hxc : x ∈ closedPoints ↥G
y : ↥G
hy : y ∈ Scheme.Hom.smoothLocus f
hyc : y ∈ closedPoints ↥G
x' : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ Over.mk f := Over.homMk ↑((pointEquivClosedPoint f).symm ⟨x, hxc⟩) ⋯
y' : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ Over.mk f := Over.homMk ↑((pointEquivClosedPoint f).symm ⟨y, hyc⟩) ⋯
⊢ False

Tactic:
let α := (GrpObj.mulRight (A := Over.mk f) x').symm ≪≫
    (GrpObj.mulRight (A := Over.mk f) y')

Goal state after:
K : Type u
inst✝⁴ : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst✝³ : LocallyOfFiniteType f
inst✝² : GrpObj (Over.mk f)
inst✝¹ : IsReduced G
inst✝ : IsAlgClosed K
this✝ : JacobsonSpace ↥G
this : Nonempty ↥G
H : (↑(Scheme.Hom.smoothLocus f))ᶜ.Nonempty
x : ↥G
hx : x ∈ (↑(Scheme.Hom.smoothLocus f))ᶜ
hxc : x ∈ closedPoints ↥G
y : ↥G
hy : y ∈ Scheme.Hom.smoothLocus f
hyc : y ∈ closedPoints ↥G
x' : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ Over.mk f := Over.homMk ↑((pointEquivClosedPoint f).symm ⟨x, hxc⟩) ⋯
y' : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ Over.mk f := Over.homMk ↑((pointEquivClosedPoint f).symm ⟨y, hyc⟩) ⋯
α : Over.mk f ≅ Over.mk f := (GrpObj.mulRight x').symm ≪≫ GrpObj.mulRight y'
⊢ False
Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent

Goal state before:
pp: X : Scheme
Z : Set ↥X
hZ : Z ∈ irreducibleComponents ↥X
inst✝ : IsNoetherian X
⊢ X.irreducibleComponentIdeal Z hZ = Hom.ker (X.irreducibleComponentOpen Z).ι

Tactic:
ext

Goal state after:
X : Scheme
Z : Set ↥X
hZ : Z ∈ irreducibleComponents ↥X
inst✝ : IsNoetherian X
x✝¹ : ↑X.affineOpens
x✝ : ↑Γ(X, ↑x✝¹)
⊢ x✝ ∈ (X.irreducibleComponentIdeal Z hZ).ideal x✝¹ ↔ x✝ ∈ (Hom.ker (X.irreducibleComponentOpen Z).ι).ideal x✝¹
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

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

Tactic:
ext

Goal state after:
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✝

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 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

Tactic:
ext

Goal state after:
case map
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
x✝² x✝¹ : B
x✝ : x✝² ⟶ x✝¹
⊢ (F.comp (id C)).map x✝ = F.map x✝
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
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

Tactic:
ext

Goal state after:
case map₂
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
x✝⁴ x✝³ : B
x✝² x✝¹ : x✝⁴ ⟶ x✝³
x✝ : x✝² ⟶ x✝¹
⊢ (F.comp (id C)).map₂ x✝ = F.map₂ x✝
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
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

Tactic:
ext

Goal state after:
case mapId
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
x✝ : B
⊢ (F.comp (id C)).mapId x✝ = F.mapId x✝
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
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:
ext

Goal state after:
case mapComp
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
x✝⁴ x✝³ x✝² : B
x✝¹ : x✝⁴ ⟶ x✝³
x✝ : x✝³ ⟶ x✝²
⊢ (F.comp (id C)).mapComp x✝¹ x✝ = F.mapComp x✝¹ x✝
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

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

Tactic:
ext

Goal state after:
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✝

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: 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

Tactic:
ext

Goal state after:
case map
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
x✝² x✝¹ : B
x✝ : x✝² ⟶ x✝¹
⊢ ((id B).comp F).map x✝ = F.map x✝
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
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

Tactic:
ext

Goal state after:
case map₂
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
x✝⁴ x✝³ : B
x✝² x✝¹ : x✝⁴ ⟶ x✝³
x✝ : x✝² ⟶ x✝¹
⊢ ((id B).comp F).map₂ x✝ = F.map₂ x✝
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
F✝ F : StrictPseudofunctor B C
G : StrictPseudofunctor C D
a✝ b✝ c✝ : B
x✝¹ : a✝ ⟶ b✝
x✝ : b✝ ⟶ c✝
⊢ (F.comp G.toStrictlyUnitaryPseudofunctor).mapComp x✝¹ x✝ = eqToIso ⋯

Tactic:
ext

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : StrictPseudofunctor B C
G : StrictPseudofunctor C D
a✝ b✝ c✝ : B
x✝¹ : a✝ ⟶ b✝
x✝ : b✝ ⟶ c✝
⊢ ((F.comp G.toStrictlyUnitaryPseudofunctor).mapComp x✝¹ x✝).hom = (eqToIso ⋯).hom
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
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

Tactic:
ext

Goal state after:
case mapId
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
x✝ : B
⊢ ((id B).comp F).mapId x✝ = F.mapId x✝
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
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:
ext

Goal state after:
case mapComp
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
x✝⁴ x✝³ x✝² : B
x✝¹ : x✝⁴ ⟶ x✝³
x✝ : x✝³ ⟶ x✝²
⊢ ((id B).comp F).mapComp x✝¹ x✝ = F.mapComp x✝¹ x✝