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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
x : ↥X
hx : QuasiFiniteAt f x
T : Scheme
fT : T ⟶ Y
left✝¹ : Etale fT
u : ↥T
hu : fT u = f x
V W : (pullback f fT).Opens
v : ↥V
hVW : IsCompl V W
left✝ : IsFinite (V.ι ≫ pullback.snd f fT)
hv₂ : (pullback.fst f fT) ↑v = x
⊢ ∃ U, (toNormalization (pullback.snd f fT)) ↑v ∈ U ∧ IsIso (toNormalization (pullback.snd f fT) ∣_ U)

Tactic:
have hVW' : (W : Set ↑(pullback f fT)) = (↑V)ᶜ :=
      eq_compl_iff_isCompl.mpr (hVW.map TopologicalSpace.Opens.frameHom).symm
    have : IsClosedImmersion V.ι := .of_isPreimmersion _ (by simp [eq_compl_comm.mp hVW', W.isOpen])
    have : IsClosedImmersion W.ι := .of_isPreimmersion _ (by simpa [hVW'] using V.2)
    obtain ⟨H⟩ := nonempty_isColimit_binaryCofanMk_of_isCompl V.ι W.ι (by simpa)
    let e : (pullback.snd f fT).normalization ≅ V ⨿ (W.ι ≫ pullback.snd f fT).normalization :=
      (Scheme.Hom.normalizationCoprodIso (pullback.snd f fT) H).symm ≪≫
        coprod.mapIso (asIso (V.ι ≫ pullback.snd f fT).toNormalization).symm (.refl _)
    let ι : V.toScheme ⟶ V ⨿ (W.ι ≫ pullback.snd f fT).normalization := coprod.inl
    refine ⟨e.hom ⁻¹ᵁ ι.opensRange, ⟨v, ?_⟩, ?_⟩
    · rw [← V.ι_apply, ← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply]
      congr 5
      rw [← Category.assoc, ← Iso.comp_inv_eq]
      simp [ι, e, Scheme.Hom.normalizationCoprodIso]
    rw [← isIso_comp_right_iff _ (e.hom ∣_ ι.opensRange),
      ← morphismRestrict_comp, ← isIso_comp_right_iff _ ι.isoOpensRange.inv]
    have Heq : (pullback.snd f fT).toNormalization ⁻¹ᵁ e.hom ⁻¹ᵁ Scheme.Hom.opensRange ι = V := by
      apply le_antisymm
      · rintro a ⟨b, hab⟩
        by_contra h
        lift a to W using hVW'.ge h
        replace hab : ι b = ((W.ι ≫ pullback.snd f fT).toNormalization ≫ coprod.inr) a := by
          have : W.ι ≫ (H.coconePointUniqueUpToIso (colimit.isColimit _)).hom = coprod.inr :=
            H.comp_coconePointUniqueUpToIso_hom _ ⟨.right⟩
          simp only [← W.ι_apply, ← Scheme.Hom.comp_apply, Category.assoc, e] at hab
          simpa [-Scheme.Hom.comp_base, Scheme.Hom.normalizationCoprodIso,
            reassoc_of% this] using hab
        exact Set.disjoint_iff_forall_ne.mp
          (isCompl_range_inl_inr V (W.ι ≫ pullback.snd f fT).normalization).1 ⟨_, rfl⟩ ⟨_, rfl⟩ hab
      · rw [← Scheme.Hom.inv_image, ← SetLike.coe_subset_coe]
        simpa [← Scheme.Hom.opensRange_comp, ι, e, Scheme.Hom.normalizationCoprodIso,
          Set.range_comp] using Set.subset_preimage_image _ _
    convert! (inferInstance : IsIso (Scheme.isoOfEq _ Heq).hom)
    rw [Iso.comp_inv_eq, ← Iso.inv_comp_eq, ← cancel_mono (Scheme.Opens.ι _)]
    have : V.ι ≫ (H.coconePointUniqueUpToIso (colimit.isColimit _)).hom = coprod.inl :=
      H.comp_coconePointUniqueUpToIso_hom _ ⟨.left⟩
    simp [e, Scheme.Hom.isoOpensRange, Scheme.Hom.normalizationCoprodIso, reassoc_of% this, ι]

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
⊢ Function.Surjective ⇑(tensorCotangentHom R T I)

Tactic:
let a : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom
  intro x
  obtain ⟨⟨x, hx⟩, rfl⟩ := Ideal.toCotangent_surjective _ x
  obtain ⟨y, rfl⟩ := I.map_includeRight_eq.le hx
  obtain rfl : hx = I.map_includeRight_eq.ge ⟨y, rfl⟩ := rfl
  induction y with
  | zero => exact ⟨0, by simp only [map_zero]; exact (map_zero _).symm⟩
  | add x y hx hy =>
    obtain ⟨a, ha⟩ := hx
    obtain ⟨b, hb⟩ := hy
    exact ⟨a + b, by simp only [map_add, ha, hb]; rfl⟩
  | tmul t x =>
    use t ⊗ₜ I.toCotangent x
    apply Ideal.cotangentToQuotientSquare_injective
    simp [-AlgHom.toRingHom_eq_coe, tensorCotangentHom_tmul, Algebra.smul_def,
      ← Ideal.Quotient.mk_algebraMap, ← map_mul]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y S : Scheme
f : X ⟶ Y
g : Y ⟶ S
s : ↥S
H : (⇑f '' ⇑(f ≫ g) ⁻¹' {s}).Finite
inst✝² : IsProper (f ≫ g)
inst✝¹ : IsSeparated g
inst✝ : LocallyOfFiniteType g
this : IsProper f
⊢ ∃ U, s ∈ U ∧ IsFinite ((Scheme.Hom.imageι f ≫ g) ∣_ U)

Tactic:
have : IsProper (f.imageι ≫ g) := by
    suffices UniversallyClosed (f.imageι ≫ g) from ⟨⟩
    have : UniversallyClosed (f.toImage ≫ f.imageι ≫ g) := by
      rw [Scheme.Hom.toImage_imageι_assoc]; infer_instance
    refine .of_comp_surjective f.toImage _

Goal state after:
X Y S : Scheme
f : X ⟶ Y
g : Y ⟶ S
s : ↥S
H : (⇑f '' ⇑(f ≫ g) ⁻¹' {s}).Finite
inst✝² : IsProper (f ≫ g)
inst✝¹ : IsSeparated g
inst✝ : LocallyOfFiniteType g
this✝ : IsProper f
this : IsProper (Scheme.Hom.imageι f ≫ g)
⊢ ∃ U, s ∈ U ∧ IsFinite ((Scheme.Hom.imageι f ≫ g) ∣_ U)
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

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

Tactic:
tmul_add,

Goal state after:
case add
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 y : S ⊗[P.Ring] Ω[P.Ring⁄R]
hx : (P.tensorCotangentSpace T) (t ⊗ₜ[R] x) = t • (CotangentSpace.map (toBaseChange T)) x
hy : (P.tensorCotangentSpace T) (t ⊗ₜ[R] y) = t • (CotangentSpace.map (toBaseChange T)) y
⊢ (P.tensorCotangentSpace T) (t ⊗ₜ[R] x + t ⊗ₜ[R] y) = t • (CotangentSpace.map (toBaseChange T)) (x + y)
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
⊢ False

Tactic:
obtain ⟨x, hx, hxc⟩ :=
    nonempty_inter_closedPoints H f.smoothLocus.2.isClosed_compl.isLocallyClosed

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
⊢ False
Module: Mathlib.Topology.Sheaves.Over

Goal state before:
pp: case mpr
X : Type u
inst✝¹ : TopologicalSpace X
U : Opens X
A : Type u_1
inst✝ : Category.{v_1, u_1} A
V : Over U
S : Sieve V
H : S ∈ ((Opens.grothendieckTopology X).over U) V
x : ↥U
hxV : x ∈ U.overEquivalence.functor.obj V
⊢ ∃ V_1 f, S.arrows (U.overEquivalence.inverse.map f ≫ U.overEquivalence.unitInv.app V) ∧ x ∈ V_1

Tactic:
obtain ⟨W, f, ⟨W', hW'V, hWW', hSW'V, rfl⟩, hxW⟩ := H x hxV

Goal state after:
case mpr
X : Type u
inst✝¹ : TopologicalSpace X
U : Opens X
A : Type u_1
inst✝ : Category.{v_1, u_1} A
V : Over U
S : Sieve V
H : S ∈ ((Opens.grothendieckTopology X).over U) V
x : ↥U
hxV : x ∈ U.overEquivalence.functor.obj V
W : Opens X
hxW : ↑x ∈ W
W' : Over U
hW'V : W' ⟶ V
hWW' : W ⟶ (Over.forget U).obj W'
hSW'V : S.arrows hW'V
⊢ ∃ V_1 f, S.arrows (U.overEquivalence.inverse.map f ≫ U.overEquivalence.unitInv.app V) ∧ x ∈ V_1
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
l₁ : a ⟶ b
r₁ : b ⟶ a
adj₁ : l₁ ⊣ r₁
l₂ : c ⟶ d
r₂ : d ⟶ c
adj₂ : l₂ ⊣ r₂
f : a ⟶ c
g : b ⟶ d
φ : f ≫ 𝟙 c ≫ l₂ ⟶ l₁ ≫ g
⊢ (mateEquiv adj₁ ((Adjunction.id c).comp adj₂)) φ =
    (mateEquiv adj₁ adj₂) (f ◁ (λ_ l₂).inv ≫ φ) ≫ (ρ_ (g ≫ r₂)).inv ≫ (α_ g r₂ (𝟙 c)).hom

Tactic:
simp only [mateEquiv_apply, Adjunction.homEquiv₁_apply, Adjunction.homEquiv₂_apply,
    Adjunction.id]

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d : B
l₁ : a ⟶ b
r₁ : b ⟶ a
adj₁ : l₁ ⊣ r₁
l₂ : c ⟶ d
r₂ : d ⟶ c
adj₂ : l₂ ⊣ r₂
f : a ⟶ c
g : b ⟶ d
φ : f ≫ 𝟙 c ≫ l₂ ⟶ l₁ ≫ g
⊢ r₁ ◁
        (((ρ_ f).inv ≫
            f ◁
                ({ unit := (ρ_ (𝟙 c)).inv, counit := (ρ_ (𝟙 c)).hom, left_triangle := ⋯, right_triangle := ⋯ }.comp
                    adj₂).unit ≫
              (α_ f (𝟙 c ≫ l₂) (r₂ ≫ 𝟙 c)).inv ≫ φ ▷ (r₂ ≫ 𝟙 c)) ≫
          (α_ l₁ g (r₂ ≫ 𝟙 c)).hom) ≫
      (α_ r₁ l₁ (g ≫ r₂ ≫ 𝟙 c)).inv ≫ adj₁.counit ▷ (g ≫ r₂ ≫ 𝟙 c) ≫ (λ_ (g ≫ r₂ ≫ 𝟙 c)).hom =
    (r₁ ◁ (((ρ_ f).inv ≫ f ◁ adj₂.unit ≫ (α_ f l₂ r₂).inv ≫ (f ◁ (λ_ l₂).inv ≫ φ) ▷ r₂) ≫ (α_ l₁ g r₂).hom) ≫
        (α_ r₁ l₁ (g ≫ r₂)).inv ≫ adj₁.counit ▷ (g ≫ r₂) ≫ (λ_ (g ≫ r₂)).hom) ≫
      (ρ_ (g ≫ r₂)).inv ≫ (α_ g r₂ (𝟙 c)).hom
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
l₁ : a ⟶ b
r₁ : b ⟶ a
adj₁ : l₁ ⊣ r₁
l₂ : c ⟶ d
r₂ : d ⟶ c
adj₂ : l₂ ⊣ r₂
f : a ⟶ c
g : b ⟶ d
φ : f ≫ l₂ ≫ 𝟙 d ⟶ l₁ ≫ g
⊢ (mateEquiv adj₁ (adj₂.comp (Adjunction.id d))) φ =
    (mateEquiv adj₁ adj₂) ((ρ_ (f ≫ l₂)).inv ≫ (α_ f l₂ (𝟙 d)).hom ≫ φ) ≫ g ◁ (λ_ r₂).inv

Tactic:
simp only [mateEquiv_apply, Adjunction.homEquiv₁_apply, Adjunction.homEquiv₂_apply,
    Adjunction.id]

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d : B
l₁ : a ⟶ b
r₁ : b ⟶ a
adj₁ : l₁ ⊣ r₁
l₂ : c ⟶ d
r₂ : d ⟶ c
adj₂ : l₂ ⊣ r₂
f : a ⟶ c
g : b ⟶ d
φ : f ≫ l₂ ≫ 𝟙 d ⟶ l₁ ≫ g
⊢ r₁ ◁
        (((ρ_ f).inv ≫
            f ◁
                (adj₂.comp
                    { unit := (ρ_ (𝟙 d)).inv, counit := (ρ_ (𝟙 d)).hom, left_triangle := ⋯,
                      right_triangle := ⋯ }).unit ≫
              (α_ f (l₂ ≫ 𝟙 d) (𝟙 d ≫ r₂)).inv ≫ φ ▷ (𝟙 d ≫ r₂)) ≫
          (α_ l₁ g (𝟙 d ≫ r₂)).hom) ≫
      (α_ r₁ l₁ (g ≫ 𝟙 d ≫ r₂)).inv ≫ adj₁.counit ▷ (g ≫ 𝟙 d ≫ r₂) ≫ (λ_ (g ≫ 𝟙 d ≫ r₂)).hom =
    (r₁ ◁
          (((ρ_ f).inv ≫ f ◁ adj₂.unit ≫ (α_ f l₂ r₂).inv ≫ ((ρ_ (f ≫ l₂)).inv ≫ (α_ f l₂ (𝟙 d)).hom ≫ φ) ▷ r₂) ≫
            (α_ l₁ g r₂).hom) ≫
        (α_ r₁ l₁ (g ≫ r₂)).inv ≫ adj₁.counit ▷ (g ≫ r₂) ≫ (λ_ (g ≫ r₂)).hom) ≫
      g ◁ (λ_ r₂).inv
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✝¹ : Module.Finite R S
p : Ideal R
inst✝ : p.IsPrime
R' : Type u
w✝⁶ : CommRing R'
w✝⁵ : Algebra R R'
w✝⁴ : Etale R R'
P : Ideal R'
w✝³ : P.IsPrime
w✝² : P.LiesOver p
n : ℕ
e : Fin (n + 1) → R' ⊗[R] ULift.{u, v} S
he : CompleteOrthogonalIdempotents e
P' : Fin n → Ideal (R' ⊗[R] ULift.{u, v} S)
w✝¹ : ∀ (i : Fin n), (P' i).IsPrime
w✝ : ∀ (i : Fin n), (P' i).LiesOver P
hP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
hP' : ∀ (i : Fin n), e i.castSucc ∉ P' i
H :
  ∀ (P'' : Ideal (R' ⊗[R] ULift.{u, v} S)),
    P''.IsPrime → P''.LiesOver P → e (Fin.last n) ∈ P'' ∧ ∀ (i : Fin n), e i.castSucc ∉ P'' → P'' = P' i
e₁ : R' ⊗[R] S ≃ₐ[R'] R' ⊗[R] ULift.{u, v} S := TensorProduct.congr AlgEquiv.refl ULift.algEquiv.{u, v, u}.symm
P'' : Ideal (R' ⊗[R] S)
x✝¹ : P''.IsPrime
x✝ : P''.LiesOver P
this :
  e (Fin.last n) ∈ Ideal.comap (↑e₁.symm) P'' ∧
    ∀ (i : Fin n), e i.castSucc ∉ Ideal.comap (↑e₁.symm) P'' → Ideal.comap (↑e₁.symm) P'' = P' i
i : Fin n
hi : (⇑e₁.symm ∘ e) i.castSucc ∉ P''
⊢ P'' = (fun i ↦ Ideal.comap (↑e₁) (P' i)) i

Tactic:
simp [← this.2 i (by simpa), Ideal.comap_comapₐ]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Flat R S
inst✝ : Module.Finite R S
⊢ Function.Surjective (comap (algebraMap R S)) ↔ Function.Injective ⇑(algebraMap R S)

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦
    have : FaithfulSMul R S := (faithfulSMul_iff_algebraMap_injective R S).mpr h
    Algebra.IsIntegral.comap_surjective _ _⟩
  apply injective_of_isLocalization_isMaximal (fun P _ ↦ Localization.AtPrime P)
    (fun P _ ↦ Localization.AtPrime P ⊗[R] S)
  intro p _
  rw [← faithfulSMul_iff_algebraMap_injective]
  obtain ⟨⟨Q, _⟩, hQ⟩ := h ⟨p, inferInstance⟩
  have : Q.LiesOver p := ⟨congr($(hQ).asIdeal).symm⟩
  let := Localization.AtPrime.algebraOfLiesOver p Q
  have : Nontrivial (Localization.AtPrime p ⊗[R] S) := by
    let f : Localization.AtPrime p ⊗[R] S →ₐ[R] Localization.AtPrime Q :=
      Algebra.TensorProduct.lift (IsScalarTower.toAlgHom R _ _)
        (IsScalarTower.toAlgHom R S _) (fun _ _ ↦ Commute.all _ _)
    exact f.domain_nontrivial
  infer_instance

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : Module.Finite R S
⊢ [Function.Surjective ⇑(algebraMap R S), Function.Bijective ⇑(LinearMap.mul' R S),
      ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1].TFAE

Tactic:
tfae_have 1 → 2 := LinearMap.mul'_bijective_of_surjective _ _

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : Module.Finite R S
tfae_1_to_2 : Function.Surjective ⇑(algebraMap R S) → Function.Bijective ⇑(LinearMap.mul' R S)
⊢ [Function.Surjective ⇑(algebraMap R S), Function.Bijective ⇑(LinearMap.mul' R S),
      ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1].TFAE
Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber

Goal state before:
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:
obtain ⟨R, rfl⟩ := h

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
r : R
hr : r ∈ R⁰
hr' : Ideal.span {r} = ⊤
⊢ ringKrullDim (R ⧸ Ideal.span {r}) + 1 ≤ ringKrullDim R

Tactic:
rw [hr', ringKrullDim_eq_bot_of_subsingleton]
    simp

Goal state after:
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
l₁ : a ⟶ b
l₂ : b ⟶ c
l₃ : d ⟶ e
l₄ : e ⟶ f
l₅ : x ⟶ y
l₆ : y ⟶ z
α : g₁ ≫ l₃ ⟶ l₁ ≫ h₁
β : h₁ ≫ l₄ ⟶ l₂ ≫ k₁
γ : g₂ ≫ l₅ ⟶ l₃ ≫ h₂
δ : h₂ ≫ l₆ ⟶ l₄ ≫ k₂
⊢ (α_ g₁ g₂ (l₅ ≫ l₆)).hom ≫
      g₁ ◁ ((α_ g₂ l₅ l₆).inv ≫ γ ▷ l₆ ≫ (α_ l₃ h₂ l₆).hom ≫ l₃ ◁ δ ≫ (α_ l₃ l₄ k₂).inv) ≫
        (α_ g₁ (l₃ ≫ l₄) k₂).inv ≫
          ((α_ g₁ l₃ l₄).inv ≫ α ▷ l₄ ≫ (α_ l₁ h₁ l₄).hom ≫ l₁ ◁ β ≫ (α_ l₁ l₂ k₁).inv) ▷ k₂ ≫
            (α_ (l₁ ≫ l₂) k₁ k₂).hom =
    (α_ (g₁ ≫ g₂) l₅ l₆).inv ≫
      ((α_ g₁ g₂ l₅).hom ≫ g₁ ◁ γ ≫ (α_ g₁ l₃ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ l₆ ≫
        (α_ l₁ (h₁ ≫ h₂) l₆).hom ≫
          l₁ ◁ ((α_ h₁ h₂ l₆).hom ≫ h₁ ◁ δ ≫ (α_ h₁ l₄ k₂).inv ≫ β ▷ k₂ ≫ (α_ l₂ k₁ k₂).hom) ≫ (α_ l₁ l₂ (k₁ ≫ k₂)).inv

Tactic:
calc
    _ = 𝟙 _ ⊗≫ g₁ ◁ γ ▷ l₆ ⊗≫ ((g₁ ≫ l₃) ◁ δ ≫ α ▷ (l₄ ≫ k₂)) ⊗≫ l₁ ◁ β ▷ k₂ ⊗≫ 𝟙 _ := by
      bicategory
    _ = _ := by
      rw [whisker_exchange]
      bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : l₂ ≅ l₁
⊢ (conjugateEquiv adj₁ adj₂) α.hom ≫ (conjugateEquiv adj₂ adj₁) α.inv = 𝟙 r₁

Tactic:
rw [conjugateEquiv_comp, Iso.inv_hom_id, conjugateEquiv_id]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : ↥(unop U)) → at ↑x
ha : (isLocallyFraction 𝒜).pred a
hb : (isLocallyFraction 𝒜).pred b
x : ↥(unop U)
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ unop U
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
hwa : ∀ (x : ↥Va), ↑⟨sa, sa_mem⟩ ∉ (↑x).asHomogeneousIdeal
wa :
  ∀ (x : ↥Va),
    (fun x ↦ a (ia x)) x =
      HomogeneousLocalization.mk { deg := ja, num := ⟨ra, ra_mem⟩, den := ⟨sa, sa_mem⟩, den_mem := ⋯ }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ unop U
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
hwb : ∀ (x : ↥Vb), ↑⟨sb, sb_mem⟩ ∉ (↑x).asHomogeneousIdeal
wb :
  ∀ (x : ↥Vb),
    (fun x ↦ b (ib x)) x =
      HomogeneousLocalization.mk { deg := jb, num := ⟨rb, rb_mem⟩, den := ⟨sb, sb_mem⟩, den_mem := ⋯ }
⊢ ∀ (x : ↥(Va ⊓ Vb)),
    (fun x ↦ (a + b) ((Va.infLELeft Vb ≫ ia) x)) x =
      HomogeneousLocalization.mk { deg := ja + jb, num := ⟨sb * ra + sa * rb, ⋯⟩, den := ⟨sa * sb, ⋯⟩, den_mem := ⋯ }

Tactic:
rintro ⟨y, hy⟩

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : ↥(unop U)) → at ↑x
ha : (isLocallyFraction 𝒜).pred a
hb : (isLocallyFraction 𝒜).pred b
x : ↥(unop U)
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ unop U
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
hwa : ∀ (x : ↥Va), ↑⟨sa, sa_mem⟩ ∉ (↑x).asHomogeneousIdeal
wa :
  ∀ (x : ↥Va),
    (fun x ↦ a (ia x)) x =
      HomogeneousLocalization.mk { deg := ja, num := ⟨ra, ra_mem⟩, den := ⟨sa, sa_mem⟩, den_mem := ⋯ }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ unop U
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
hwb : ∀ (x : ↥Vb), ↑⟨sb, sb_mem⟩ ∉ (↑x).asHomogeneousIdeal
wb :
  ∀ (x : ↥Vb),
    (fun x ↦ b (ib x)) x =
      HomogeneousLocalization.mk { deg := jb, num := ⟨rb, rb_mem⟩, den := ⟨sb, sb_mem⟩, den_mem := ⋯ }
y : ↑(ProjectiveSpectrum.top 𝒜)
hy : y ∈ Va ⊓ Vb
⊢ (fun x ↦ (a + b) ((Va.infLELeft Vb ≫ ia) x)) ⟨y, hy⟩ =
    HomogeneousLocalization.mk { deg := ja + jb, num := ⟨sb * ra + sa * rb, ⋯⟩, den := ⟨sa * sb, ⋯⟩, den_mem := ⋯ }
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : ↥(unop U)) → at ↑x
ha : (isLocallyFraction 𝒜).pred a
hb : (isLocallyFraction 𝒜).pred b
x : ↥(unop U)
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ unop U
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
hwa : ∀ (x : ↥Va), ↑⟨sa, sa_mem⟩ ∉ (↑x).asHomogeneousIdeal
wa :
  ∀ (x : ↥Va),
    (fun x ↦ a (ia x)) x =
      HomogeneousLocalization.mk { deg := ja, num := ⟨ra, ra_mem⟩, den := ⟨sa, sa_mem⟩, den_mem := ⋯ }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ unop U
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
hwb : ∀ (x : ↥Vb), ↑⟨sb, sb_mem⟩ ∉ (↑x).asHomogeneousIdeal
wb :
  ∀ (x : ↥Vb),
    (fun x ↦ b (ib x)) x =
      HomogeneousLocalization.mk { deg := jb, num := ⟨rb, rb_mem⟩, den := ⟨sb, sb_mem⟩, den_mem := ⋯ }
⊢ ∀ (x : ↥(Va ⊓ Vb)),
    (fun x ↦ (a * b) ((Va.infLELeft Vb ≫ ia) x)) x =
      HomogeneousLocalization.mk { deg := ja + jb, num := ⟨ra * rb, ⋯⟩, den := ⟨sa * sb, ⋯⟩, den_mem := ⋯ }

Tactic:
rintro ⟨y, hy⟩

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : ↥(unop U)) → at ↑x
ha : (isLocallyFraction 𝒜).pred a
hb : (isLocallyFraction 𝒜).pred b
x : ↥(unop U)
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ unop U
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
hwa : ∀ (x : ↥Va), ↑⟨sa, sa_mem⟩ ∉ (↑x).asHomogeneousIdeal
wa :
  ∀ (x : ↥Va),
    (fun x ↦ a (ia x)) x =
      HomogeneousLocalization.mk { deg := ja, num := ⟨ra, ra_mem⟩, den := ⟨sa, sa_mem⟩, den_mem := ⋯ }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ unop U
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
hwb : ∀ (x : ↥Vb), ↑⟨sb, sb_mem⟩ ∉ (↑x).asHomogeneousIdeal
wb :
  ∀ (x : ↥Vb),
    (fun x ↦ b (ib x)) x =
      HomogeneousLocalization.mk { deg := jb, num := ⟨rb, rb_mem⟩, den := ⟨sb, sb_mem⟩, den_mem := ⋯ }
y : ↑(ProjectiveSpectrum.top 𝒜)
hy : y ∈ Va ⊓ Vb
⊢ (fun x ↦ (a * b) ((Va.infLELeft Vb ≫ ia) x)) ⟨y, hy⟩ =
    HomogeneousLocalization.mk { deg := ja + jb, num := ⟨ra * rb, ⋯⟩, den := ⟨sa * sb, ⋯⟩, den_mem := ⋯ }
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: X✝ Y Z T : Scheme
M N K : X✝.Modules
φ : M ⟶ N
U✝ V✝ : X✝.Opens
X : Scheme
U V : X.Opens
f : V ⟶ U
⊢ overMap X.ringCatSheaf f ⋙ (overEquiv V).functor ≅ (overEquiv U).functor ⋙ restrictFunctor (X.homOfLE ⋯)

Tactic:
by
  haveI : (Hom.opensFunctor (X.homOfLE <| leOfHom f)).IsContinuous
      (Opens.grothendieckTopology V.toScheme) (Opens.grothendieckTopology U.carrier) :=
    inferInstanceAs <|
      (Hom.opensFunctor (X.homOfLE <| leOfHom f)).IsContinuous _
      (Opens.grothendieckTopology U.toScheme)
  haveI := U.instIsDenseSubsiteSubtypeMemOverGrothendieckTopologyOverInverseOverEquivalence
  haveI : (Hom.opensFunctor (X.homOfLE <| leOfHom f)).IsContinuous
      (Opens.grothendieckTopology ↥V) (Opens.grothendieckTopology U.toScheme) :=
    inferInstanceAs <| (X.homOfLE <| leOfHom f).opensFunctor.IsContinuous
      (Opens.grothendieckTopology V.toScheme) (Opens.grothendieckTopology U.toScheme)
  haveI : ((Opens.overEquivalence V).symm.functor ⋙ Over.map f).IsContinuous
      (Opens.grothendieckTopology ↥V) ((Opens.grothendieckTopology X).over U) :=
    Functor.isContinuous_comp _ _ _ (.over (Opens.grothendieckTopology _) _) _
  haveI : (Opens.overEquivalence U).symm.functor.IsContinuous (Opens.grothendieckTopology U)
      ((Opens.grothendieckTopology X).over U) :=
    inferInstanceAs <| U.overEquivalence.inverse.IsContinuous (Opens.grothendieckTopology U.carrier)
      ((Opens.grothendieckTopology X).over U)
  haveI : ((X.homOfLE (leOfHom f)).opensFunctor ⋙
        (Opens.overEquivalence U).symm.functor).IsContinuous (Opens.grothendieckTopology ↥V)
      ((Opens.grothendieckTopology ↥X).over U) :=
    Functor.isContinuous_comp _ _ _ (Opens.grothendieckTopology _) _
  refine (SheafOfModules.pushforwardComp _ _) ≪≫ ?_ ≪≫ (SheafOfModules.pushforwardComp _ _).symm
  refine SheafOfModules.pushforwardCongr₂ _ ?_ ?_
  · refine NatIso.ofComponents (fun W ↦ Over.isoMk (eqToIso ?_) ?_) ?_
    · suffices U.ι ''ᵁ ((X.homOfLE (leOfHom f)) ''ᵁ W) = V.ι ''ᵁ W by simpa
      simp [← Scheme.Hom.comp_image]
    · cat_disch
    · cat_disch
  · ext W x
    suffices X.presheaf.map _ x = ((X.homOfLE <| leOfHom f).appIso _).inv x by simpa
    rw [Scheme.Hom.appIso_homOfLE_inv]
    rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
a : ↑(CommRingCat.of (Away 𝒜 f))
⊢ ↑((CommRingCat.Hom.hom (CommRingCat.ofHom (awayMap 𝒜 g_deg hx) ≫ awayToSection 𝒜 x)) a) =
    ↑((CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (homOfLE ⋯).op)) a)

Tactic:
ext ⟨i, hi⟩

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
a : ↑(CommRingCat.of (Away 𝒜 f))
i : ↑(ProjectiveSpectrum.top 𝒜)
hi : i ∈ Opposite.unop (Opposite.op (basicOpen 𝒜 x))
⊢ val (↑((CommRingCat.Hom.hom (CommRingCat.ofHom (awayMap 𝒜 g_deg hx) ≫ awayToSection 𝒜 x)) a) ⟨i, hi⟩) =
    val (↑((CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (homOfLE ⋯).op)) a) ⟨i, hi⟩)