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

Goal state before:
pp: case refine_1
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
hVW' : ↑W = (↑V)ᶜ
this✝ : IsClosedImmersion V.ι
this : IsClosedImmersion W.ι
H : IsColimit (BinaryCofan.mk V.ι W.ι)
e : normalization (pullback.snd f fT) ≅ ↑V ⨿ normalization (W.ι ≫ pullback.snd f fT) :=
  (normalizationCoprodIso (pullback.snd f fT) H).symm ≪≫
    coprod.mapIso (asIso (toNormalization (V.ι ≫ pullback.snd f fT))).symm
      (Iso.refl (normalization (W.ι ≫ pullback.snd f fT)))
ι : ↑V ⟶ ↑V ⨿ normalization (W.ι ≫ pullback.snd f fT) := coprod.inl
⊢ ι ≫ e.inv = V.ι ≫ toNormalization (pullback.snd f fT)

Tactic:
simp [ι, e, Scheme.Hom.normalizationCoprodIso]

Goal state after:
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 γ) '' ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} ⊆ {(Over.Hom.left (lift η η)) point}
U : G.left.Opens
hηU : (Over.Hom.left η) point ∈ U
H : IsFinite ((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U)
x : ↥U
this : ⇑U.ι ⁻¹' {↑x} = {x}
⊢ ⇑(pullback.fst G.hom G.hom) ⁻¹' {↑x} ∩ Set.range ⇑(Over.Hom.left γ) ⊆
    ⇑(Over.Hom.left (fst G G)) ⁻¹' {↑x} ∩
      ⇑(Scheme.Hom.imageι (Over.Hom.left γ)) ''
        ↑((TopologicalSpace.Opens.map ((Scheme.Hom.imageι (Over.Hom.left γ)).base ≫ (Over.Hom.left (fst G G)).base)).obj
            U)

Tactic:
dsimp

Goal state after:
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 γ) '' ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} ⊆ {(Over.Hom.left (lift η η)) point}
U : G.left.Opens
hηU : (Over.Hom.left η) point ∈ U
H : IsFinite ((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U)
x : ↥U
this : ⇑U.ι ⁻¹' {↑x} = {x}
⊢ ⇑(pullback.fst G.hom G.hom) ⁻¹' {↑x} ∩ Set.range ⇑(Over.Hom.left γ) ⊆
    ⇑(pullback.fst G.hom G.hom) ⁻¹' {↑x} ∩
      ⇑(Scheme.Hom.imageι (Over.Hom.left γ)) ''
        ⇑(Scheme.Hom.imageι (Over.Hom.left γ)) ⁻¹' ⇑(pullback.fst G.hom G.hom) ⁻¹' ↑U
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
x✝ : ↥X
⊢ x✝ ∈ ↑(quasiFiniteLocus (f ≫ g)) ↔ x✝ ∈ ↑(f ⁻¹ᵁ quasiFiniteLocus g)

Tactic:
simp [quasiFiniteAt_comp_iff_of_isOpenImmersion]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.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✝ : FinitePresentation T (T ⊗[R] S)
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
this✝ : Module.FaithfullyFlat (MvPolynomial (Fin n) R) (T ⊗[R] MvPolynomial (Fin n) R)
fT : T ⊗[R] MvPolynomial (Fin n) R →ₐ[T] T ⊗[R] S := ⋯
this :
  Ideal.map (algebraMap (MvPolynomial (Fin n) R) (T ⊗[R] MvPolynomial (Fin n) R)) (RingHom.ker f.toRingHom) =
    RingHom.ker fT
⊢ Function.Surjective ⇑fT

Tactic:
exact FiniteType.baseChangeAux_surj T hf

Goal state after:
Module: Mathlib.RingTheory.Ideal.CotangentBaseChange

Goal state before:
pp: case h
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
a : S →+* T ⊗[R] S := ⋯
t : T
x : ↥(Submodule.restrictScalars R I)
⊢ (map Algebra.TensorProduct.includeRight.toRingHom I).cotangentToQuotientSquare
      ((tensorCotangentHom R T I) (t ⊗ₜ[R] I.toCotangent x)) =
    (map Algebra.TensorProduct.includeRight.toRingHom I).cotangentToQuotientSquare
      ((map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent
        ⟨(LinearMap.lTensor T (Submodule.restrictScalars R I).subtype) (t ⊗ₜ[R] x), ⋯⟩)

Tactic:
simp [-AlgHom.toRingHom_eq_coe, tensorCotangentHom_tmul, Algebra.smul_def,
      ← Ideal.Quotient.mk_algebraMap, ← map_mul]

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

Goal state before:
pp: case mem
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
s : S
x y : Ω[P.Ring⁄R]
hy : y ∈ Set.range ⇑(KaehlerDifferential.D R P.Ring)
⊢ t ⊗ₜ[R] s ⊗ₜ[P.baseChange.Ring]
      (KaehlerDifferential.tensorKaehlerEquiv R T P.Ring P.baseChange.Ring) (1 ⊗ₜ[P.Ring] y) =
    t ⊗ₜ[R] s ⊗ₜ[P.baseChange.Ring] (KaehlerDifferential.map R T P.Ring P.baseChange.Ring) y

Tactic:
| mem y hy =>

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

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ⟶ f ≫ g
ε : g ≫ f ⟶ 𝟙 b
h : leftZigzag η ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ g ◁ η ⊗≫ (ε ▷ g ▷ 𝟙 a ≫ (𝟙 b ≫ g) ◁ η) ⊗≫ ε ▷ g =
    𝟙 (g ≫ 𝟙 a) ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 (𝟙 b ≫ g)

Tactic:
← whisker_exchange

Goal state after:
B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ⟶ f ≫ g
ε : g ≫ f ⟶ 𝟙 b
h : leftZigzag η ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ g ◁ η ⊗≫ (((g ≫ f) ≫ g) ◁ η ≫ ε ▷ g ▷ (f ≫ g)) ⊗≫ ε ▷ g =
    𝟙 (g ≫ 𝟙 a) ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 (𝟙 b ≫ g)
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ 𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      adj₁.unit ▷ (f₁ ≫ f₂) ⊗≫
        f₁ ◁ (adj₂.unit ▷ (g₁ ≫ f₁) ≫ (f₂ ≫ g₂) ◁ adj₁.counit) ▷ f₂ ⊗≫ (f₁ ≫ f₂) ◁ adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c) =
    𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      leftZigzag adj₁.unit adj₁.counit ▷ f₂ ⊗≫ f₁ ◁ leftZigzag adj₂.unit adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c)

Tactic:
← whisker_exchange

Goal state after:
B : Type u₁
inst✝ : Bicategory B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ 𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      adj₁.unit ▷ (f₁ ≫ f₂) ⊗≫
        f₁ ◁ (𝟙 b ◁ adj₁.counit ≫ adj₂.unit ▷ 𝟙 b) ▷ f₂ ⊗≫ (f₁ ≫ f₂) ◁ adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c) =
    𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      leftZigzag adj₁.unit adj₁.counit ▷ f₂ ⊗≫ f₁ ◁ leftZigzag adj₂.unit adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c)
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
x : X
⊢ x ∈ ↑((𝟭 (Over U)).obj V).left ↔
    x ∈
      ↑(({ 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:
dsimp

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
U : Opens X
A : Type u_1
inst✝ : Category.{v_1, u_1} A
V : Over U
x : X
⊢ x ∈ ↑V.left ↔ x ∈ Subtype.val '' Subtype.val ⁻¹' ↑V.left
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
γ : g ⟶ l ≫ h
⊢ 𝟙 g ⊗≫ (adj.unit ▷ g ≫ (l ≫ r) ◁ γ) ⊗≫ l ◁ adj.counit ▷ h ⊗≫ 𝟙 (l ≫ h) =
    γ ⊗≫ leftZigzag adj.unit adj.counit ▷ h ⊗≫ 𝟙 (l ≫ h)

Tactic:
← whisker_exchange

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
γ : g ⟶ l ≫ h
⊢ 𝟙 g ⊗≫ (𝟙 b ◁ γ ≫ adj.unit ▷ (l ≫ h)) ⊗≫ l ◁ adj.counit ▷ h ⊗≫ 𝟙 (l ≫ h) =
    γ ⊗≫ leftZigzag adj.unit adj.counit ▷ h ⊗≫ 𝟙 (l ≫ h)
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ 𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
        g₂ ◁ ((g₁ ≫ f₁) ◁ adj₂.unit ≫ adj₁.counit ▷ (f₂ ≫ g₂)) ▷ g₁ ⊗≫ adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁) =
    𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      g₂ ◁ rightZigzag adj₁.unit adj₁.counit ⊗≫ rightZigzag adj₂.unit adj₂.counit ▷ g₁ ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁)

Tactic:
rw [whisker_exchange]; bicategory

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : a ⟶ b
h : a ⟶ c
α : g ≫ l ⟶ h
⊢ 𝟙 (g ≫ l) ⊗≫ g ◁ adj.unit ▷ l ⊗≫ (α ▷ (r ≫ l) ≫ h ◁ adj.counit) ⊗≫ 𝟙 h =
    𝟙 (g ≫ l) ⊗≫ g ◁ leftZigzag adj.unit adj.counit ⊗≫ α

Tactic:
← whisker_exchange

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : a ⟶ b
h : a ⟶ c
α : g ≫ l ⟶ h
⊢ 𝟙 (g ≫ l) ⊗≫ g ◁ adj.unit ▷ l ⊗≫ ((g ≫ l) ◁ adj.counit ≫ α ▷ 𝟙 c) ⊗≫ 𝟙 h =
    𝟙 (g ≫ l) ⊗≫ g ◁ leftZigzag adj.unit adj.counit ⊗≫ α
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
⊢ 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

Tactic:
dsimp

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 ◁ ((ρ_ (𝟙 c)).inv ⊗≫ 𝟙 c ◁ adj₂.unit ▷ 𝟙 c ⊗≫ 𝟙 ((𝟙 c ≫ l₂) ≫ r₂ ≫ 𝟙 c)) ≫
              (α_ 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
⊢ 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

Tactic:
dsimp

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₂.unit ⊗≫ l₂ ◁ (ρ_ (𝟙 d)).inv ▷ r₂ ⊗≫ 𝟙 ((l₂ ≫ 𝟙 d) ≫ 𝟙 d ≫ r₂)) ≫
              (α_ 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.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e f : B
g₁ : a ⟶ c
g₂ : c ⟶ e
h₁ : b ⟶ d
h₂ : d ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : e ⟶ f
r₃ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁
β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂
⊢ 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      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₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      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₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)

Tactic:
← whisker_exchange

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d e f : B
g₁ : a ⟶ c
g₂ : c ⟶ e
h₁ : b ⟶ d
h₂ : d ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : e ⟶ f
r₃ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁
β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂
⊢ 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ adj₂.unit ▷ g₂ ⊗≫
        r₁ ◁ α ▷ r₂ ▷ g₂ ⊗≫
          ((r₁ ≫ l₁) ◁ h₁ ◁ r₂ ◁ g₂ ◁ adj₃.unit ≫ adj₁.counit ▷ (h₁ ≫ r₂ ≫ g₂ ≫ l₃ ≫ r₃)) ⊗≫
            h₁ ◁ r₂ ◁ β ▷ r₃ ⊗≫ h₁ ◁ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      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₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e f : B
g₁ : a ⟶ c
g₂ : c ⟶ e
h₁ : b ⟶ d
h₂ : d ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : e ⟶ f
r₃ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁
β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂
⊢ 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ adj₂.unit ▷ g₂ ⊗≫
        r₁ ◁ ((g₁ ≫ l₂) ◁ r₂ ◁ g₂ ◁ adj₃.unit ≫ α ▷ (r₂ ≫ g₂ ≫ l₃ ≫ r₃)) ⊗≫
          (adj₁.counit ▷ (h₁ ≫ r₂) ▷ (g₂ ≫ l₃) ≫ (𝟙 b ≫ h₁ ≫ r₂) ◁ β) ▷ r₃ ⊗≫
            h₁ ◁ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      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₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)

Tactic:
← whisker_exchange

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d e f : B
g₁ : a ⟶ c
g₂ : c ⟶ e
h₁ : b ⟶ d
h₂ : d ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : e ⟶ f
r₃ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁
β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂
⊢ 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ adj₂.unit ▷ g₂ ⊗≫
        r₁ ◁ ((g₁ ≫ l₂) ◁ r₂ ◁ g₂ ◁ adj₃.unit ≫ α ▷ (r₂ ≫ g₂ ≫ l₃ ≫ r₃)) ⊗≫
          (((r₁ ≫ l₁) ≫ h₁ ≫ r₂) ◁ β ≫ adj₁.counit ▷ (h₁ ≫ r₂) ▷ (l₂ ≫ h₂)) ▷ r₃ ⊗≫
            h₁ ◁ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      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₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)
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.FinitePresentation R S
⊢ FinitePresentation R S

Tactic:
by
  obtain ⟨S', _, _, _, _, _, f, hf⟩ := Module.Finite.exists_free_surjective R S
  refine .of_surjective hf ?_
  apply Submodule.FG.of_restrictScalars R
  exact Module.FinitePresentation.fg_ker f.toLinearMap hf

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 : B
g₁ : a ⟶ c
g₂ : c ⟶ e
h₁ : b ⟶ d
h₂ : d ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : e ⟶ f
r₃ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁
β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂
⊢ 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ (𝟙 c ◁ g₂ ◁ adj₃.unit ≫ adj₂.unit ▷ (g₂ ≫ l₃ ≫ r₃)) ⊗≫
        r₁ ◁ ((g₁ ≫ l₂) ◁ r₂ ◁ β ≫ α ▷ (r₂ ≫ l₂ ≫ h₂)) ▷ r₃ ⊗≫
          (adj₁.counit ▷ h₁ ▷ (r₂ ≫ l₂) ≫ (𝟙 b ≫ h₁) ◁ adj₂.counit) ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      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₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)

Tactic:
← whisker_exchange

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d e f : B
g₁ : a ⟶ c
g₂ : c ⟶ e
h₁ : b ⟶ d
h₂ : d ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : e ⟶ f
r₃ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁
β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂
⊢ 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ (𝟙 c ◁ g₂ ◁ adj₃.unit ≫ adj₂.unit ▷ (g₂ ≫ l₃ ≫ r₃)) ⊗≫
        r₁ ◁ ((g₁ ≫ l₂) ◁ r₂ ◁ β ≫ α ▷ (r₂ ≫ l₂ ≫ h₂)) ▷ r₃ ⊗≫
          (((r₁ ≫ l₁) ≫ h₁) ◁ adj₂.counit ≫ adj₁.counit ▷ h₁ ▷ 𝟙 d) ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      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₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
hf₁✝ : IsFinite (Spec.map f)
hf₂✝ : Flat (Spec.map f)
hf₁ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Finite
hf₂ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Flat
x✝ : ↥(Spec R)
this : f = (ΓSpecIso R).inv ≫ appTop (Spec.map f) ≫ (ΓSpecIso S).hom
⊢ (CommRingCat.Hom.hom (appTop (Spec.map f))).finrank ((Spec R).isoSpec.hom x✝) =
    (CommRingCat.Hom.hom ((ΓSpecIso R).inv ≫ appTop (Spec.map f) ≫ (ΓSpecIso S).hom)).finrank x✝

Tactic:
dsimp

Goal state after:
R S : CommRingCat
f : R ⟶ S
hf₁✝ : IsFinite (Spec.map f)
hf₂✝ : Flat (Spec.map f)
hf₁ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Finite
hf₂ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Flat
x✝ : ↥(Spec R)
this : f = (ΓSpecIso R).inv ≫ appTop (Spec.map f) ≫ (ΓSpecIso S).hom
⊢ (CommRingCat.Hom.hom (appTop (Spec.map f))).finrank ((Spec R).isoSpec.hom x✝) =
    (((CommRingCat.Hom.hom (ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (appTop (Spec.map f)))).comp
          (CommRingCat.Hom.hom (ΓSpecIso R).inv)).finrank
      x✝
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e f : B
g₁ : a ⟶ c
g₂ : c ⟶ e
h₁ : b ⟶ d
h₂ : d ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : e ⟶ f
r₃ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁
β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂
⊢ 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫
        r₁ ◁ g₁ ◁ (𝟙 c ◁ β ≫ adj₂.unit ▷ (l₂ ≫ h₂)) ▷ r₃ ⊗≫
          r₁ ◁ (α ▷ (r₂ ≫ l₂) ≫ (l₁ ≫ h₁) ◁ adj₂.counit) ▷ h₂ ▷ r₃ ⊗≫ adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      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₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)

Tactic:
← whisker_exchange

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d e f : B
g₁ : a ⟶ c
g₂ : c ⟶ e
h₁ : b ⟶ d
h₂ : d ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : e ⟶ f
r₃ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁
β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂
⊢ 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫
        r₁ ◁ g₁ ◁ (𝟙 c ◁ β ≫ adj₂.unit ▷ (l₂ ≫ h₂)) ▷ r₃ ⊗≫
          r₁ ◁ ((g₁ ≫ l₂) ◁ adj₂.counit ≫ α ▷ 𝟙 d) ▷ h₂ ▷ r₃ ⊗≫ adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      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₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: R S : CommRingCat
φ : R ⟶ S
h : finrank (Spec.map φ) = 1
inst✝¹ : (CommRingCat.Hom.hom φ).Flat
inst✝ : (CommRingCat.Hom.hom φ).Finite
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝¹ : Module.Flat ↑R ↑S
algebraizeInst✝ : Module.Finite ↑R ↑S
⊢ IsIso (Spec.map φ)

Tactic:
have : IsIso φ := by
    rw [ConcreteCategory.isIso_iff_bijective]
    apply Module.algebraMap_bijective_of_rankAtStalk
    rwa [finrank_SpecMap_eq_finrank ‹_› ‹_›] at h

Goal state after:
R S : CommRingCat
φ : R ⟶ S
h : finrank (Spec.map φ) = 1
inst✝¹ : (CommRingCat.Hom.hom φ).Flat
inst✝ : (CommRingCat.Hom.hom φ).Finite
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝¹ : Module.Flat ↑R ↑S
algebraizeInst✝ : Module.Finite ↑R ↑S
this : IsIso φ
⊢ IsIso (Spec.map φ)
Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale

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

Tactic:
weaklyEtale_eq_flat_inf_diagonal_flat

Goal state after:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@Flat ⊓ MorphismProperty.diagonal @Flat).RespectsIso
Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale

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

Tactic:
weaklyEtale_eq_flat_inf_diagonal_flat

Goal state after:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@Flat ⊓ MorphismProperty.diagonal @Flat).IsMultiplicative
Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale

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

Tactic:
weaklyEtale_eq_flat_inf_diagonal_flat

Goal state after:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@Flat ⊓ MorphismProperty.diagonal @Flat).IsStableUnderBaseChange
Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtSource @WeaklyEtale

Tactic:
weaklyEtale_eq_flat_inf_diagonal_flat

Goal state after:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtSource (@Flat ⊓ MorphismProperty.diagonal @Flat)