mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
g : R[X]
n : ℕ
r : R
hg✝ : g.natDegree ≤ n
a✝ : Nontrivial R
hg : g.natDegree > 0
⊢ (X - C r).resultant (g %ₘ (X - C r) + (X - C r) * (g /ₘ (X - C r))) 1 n = eval r g

Tactic:
resultant_add_mul_right _ _ _ _ _ _ (natDegree_X_sub_C_le _),

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
g : R[X]
n : ℕ
r : R
hg✝ : g.natDegree ≤ n
a✝ : Nontrivial R
hg : g.natDegree > 0
⊢ (X - C r).resultant (g %ₘ (X - C r)) 1 n = eval r g

R : Type u_1
inst✝ : CommRing R
g : R[X]
n : ℕ
r : R
hg✝ : g.natDegree ≤ n
a✝ : Nontrivial R
hg : g.natDegree > 0
⊢ (g /ₘ (X - C r)).natDegree + 1 ≤ n
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
q : PrimeSpectrum S
⊢ QuasiFiniteAt R q.asIdeal ↔ IsOpen {⟨q, ⋯⟩}

Tactic:
by
  refine ⟨fun H ↦ ?_, .of_isOpen_singleton_fiber q⟩
  let p := q.comap (algebraMap R S)
  let e := PrimeSpectrum.preimageHomeomorphFiber R S p
  rw [← e.isOpen_image, Set.image_singleton]
  suffices Algebra.QuasiFiniteAt p.asIdeal.ResidueField (e ⟨q, rfl⟩).asIdeal from
    (QuasiFiniteAt.isClopen_singleton (R := p.asIdeal.ResidueField) _).isOpen
  exact .baseChange q.asIdeal _ congr($(e.symm_apply_apply ⟨q, rfl⟩).1.asIdeal).symm

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

Goal state before:
pp: case inr.inr.inr.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.resultant (f * a + b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
⊢ ∃ n, f.resultant g ∣ f.leadingCoeff ^ n

pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
⊢ a.natDegree + f.natDegree ≤ b.natDegree + g.natDegree

Tactic:
mul_comm f,

Goal state after:
case inr.inr.inr.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.resultant (a * f + b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
⊢ ∃ n, f.resultant g ∣ f.leadingCoeff ^ n

R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
⊢ a.natDegree + f.natDegree ≤ b.natDegree + g.natDegree
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u
S : Type v
T : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra.FiniteType R T
inst✝¹ : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg : Function.Surjective ⇑(awayMapₐ f g)
p : Ideal R
inst✝ : p.IsPrime
hgp : IsUnit (1 ⊗ₜ[R] g)
this : IsClosed (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})
r : R
hpr : { asIdeal := p, isPrime := inst✝ } ∈ ↑(PrimeSpectrum.basicOpen r)
hrg : ↑(PrimeSpectrum.basicOpen r) ⊆ (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})ᶜ
⊢ IsLocalization.Away (f.toRingHom ((algebraMap R S) r)) (Away ((algebraMap R T) r))

Tactic:
simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, AlgHom.commutes]

Goal state after:
R : Type u
S : Type v
T : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra.FiniteType R T
inst✝¹ : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg : Function.Surjective ⇑(awayMapₐ f g)
p : Ideal R
inst✝ : p.IsPrime
hgp : IsUnit (1 ⊗ₜ[R] g)
this : IsClosed (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})
r : R
hpr : { asIdeal := p, isPrime := inst✝ } ∈ ↑(PrimeSpectrum.basicOpen r)
hrg : ↑(PrimeSpectrum.basicOpen r) ⊆ (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})ᶜ
⊢ IsLocalization.Away ((algebraMap R T) r) (Away ((algebraMap R T) r))
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsSeparated f
x : ↥X
s : ↥S
h : f x = s
hx : Scheme.Hom.QuasiFiniteAt f x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hUV : V ≤ f ⁻¹ᵁ U
this✝² : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).FiniteType
algInst✝ : Algebra ↑Γ(S, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).toAlgebra
algebraizeInst✝ : Algebra.FiniteType ↑Γ(S, U) ↑Γ(X, V)
this✝¹ : (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal.LiesOver (IsAffineOpen.primeIdealOf hU ⟨f x, hxU⟩).asIdeal
this✝ : Algebra.QuasiFiniteAt (↑Γ(S, U)) (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
R : Type u
w✝⁷ : CommRing R
w✝⁶ : Algebra (↑Γ(S, U)) R
w✝⁵ : Algebra.Etale (↑Γ(S, U)) R
P : Ideal R
w✝⁴ : P.IsPrime
w✝³ : P.LiesOver (IsAffineOpen.primeIdealOf hU ⟨f x, hxU⟩).asIdeal
e : R ⊗[↑Γ(S, U)] ↑Γ(X, V)
w✝² : IsIdempotentElem e
P' : Ideal (R ⊗[↑Γ(S, U)] ↑Γ(X, V))
w✝¹ : P'.IsPrime
w✝ : P'.LiesOver P
hP' : Ideal.comap Algebra.TensorProduct.includeRight.toRingHom P' = (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
heP' : e ∉ P'
left✝ : Module.Finite R (Localization.Away e)
this : (algebraMap R (Localization.Away e)).Finite
⊢ ∃ U g,
    Etale g ∧ s ∈ Set.range ⇑g ∧ ∃ V W v, IsCompl V W ∧ IsFinite (V.ι ≫ pullback.snd f g) ∧ (pullback.fst f g) ↑v = x

Tactic:
let φ : Γ(S, U) ⟶ .of R := CommRingCat.ofHom <| algebraMap Γ(S, U) R

Goal state after:
X S : Scheme
f : X ⟶ S
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsSeparated f
x : ↥X
s : ↥S
h : f x = s
hx : Scheme.Hom.QuasiFiniteAt f x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hUV : V ≤ f ⁻¹ᵁ U
this✝² : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).FiniteType
algInst✝ : Algebra ↑Γ(S, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).toAlgebra
algebraizeInst✝ : Algebra.FiniteType ↑Γ(S, U) ↑Γ(X, V)
this✝¹ : (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal.LiesOver (IsAffineOpen.primeIdealOf hU ⟨f x, hxU⟩).asIdeal
this✝ : Algebra.QuasiFiniteAt (↑Γ(S, U)) (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
R : Type u
w✝⁷ : CommRing R
w✝⁶ : Algebra (↑Γ(S, U)) R
w✝⁵ : Algebra.Etale (↑Γ(S, U)) R
P : Ideal R
w✝⁴ : P.IsPrime
w✝³ : P.LiesOver (IsAffineOpen.primeIdealOf hU ⟨f x, hxU⟩).asIdeal
e : R ⊗[↑Γ(S, U)] ↑Γ(X, V)
w✝² : IsIdempotentElem e
P' : Ideal (R ⊗[↑Γ(S, U)] ↑Γ(X, V))
w✝¹ : P'.IsPrime
w✝ : P'.LiesOver P
hP' : Ideal.comap Algebra.TensorProduct.includeRight.toRingHom P' = (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
heP' : e ∉ P'
left✝ : Module.Finite R (Localization.Away e)
this : (algebraMap R (Localization.Away e)).Finite
φ : Γ(S, U) ⟶ CommRingCat.of R := CommRingCat.ofHom (algebraMap (↑Γ(S, U)) R)
⊢ ∃ U g,
    Etale g ∧ s ∈ Set.range ⇑g ∧ ∃ V W v, IsCompl V W ∧ IsFinite (V.ι ≫ pullback.snd f g) ∧ (pullback.fst f g) ↑v = x
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
F : Cᵒᵖ ⥤ GrpCat
X : C
e : (F ⋙ forget GrpCat).RepresentableBy X
⊢ yonedaGrp.essImage F

Tactic:
let := GrpObj.ofRepresentableBy X F e

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
F : Cᵒᵖ ⥤ GrpCat
X : C
e : (F ⋙ forget GrpCat).RepresentableBy X
this : GrpObj X := GrpObj.ofRepresentableBy X F e
⊢ yonedaGrp.essImage F
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 γ) ⊆
    ⇑(((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ⁻¹ᵁ U).ι ≫
          Scheme.Hom.imageι (Over.Hom.left γ)) ''
      ⇑((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U ≫ U.ι) ⁻¹' {↑x}

Tactic:
morphismRestrict_ι,

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 γ) ⊆
    ⇑(((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ⁻¹ᵁ U).ι ≫
          Scheme.Hom.imageι (Over.Hom.left γ)) ''
      ⇑(((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ⁻¹ᵁ U).ι ≫
            Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ⁻¹'
        {↑x}
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsProper f
inst✝ : LocallyQuasiFinite f
this : IsIso (Scheme.Hom.toNormalization f)
⊢ IsIntegralHom f

Tactic:
rw [← f.toNormalization_fromNormalization]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsProper f
inst✝ : LocallyQuasiFinite f
this : IsIso (Scheme.Hom.toNormalization f)
⊢ IsIntegralHom (Scheme.Hom.toNormalization f ≫ Scheme.Hom.fromNormalization f)
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✝ : FiniteType T (T ⊗[R] S)
s : Finset (T ⊗[R] S)
hs : adjoin T ↑s = ⊤
k : ↥s → ℕ
t : (x : ↥s) → Fin (k x) → T
m : (x : ↥s) → Fin (k x) → S
h : ∀ (x : ↥s), ↑x = ∑ j, t x j ⊗ₜ[R] m x j
f : MvPolynomial ((x : ↥s) × Fin (k x)) R →ₐ[R] S :=
  MvPolynomial.aeval fun x ↦
    match x with
    | ⟨x, i⟩ => m x i
hf : Function.Surjective ⇑(TensorProduct.map (AlgHom.id T T) f)
⊢ Function.Surjective ⇑f

Tactic:
exact (Module.FaithfullyFlat.lTensor_surjective_iff_surjective _ T _).mp hf

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

Goal state before:
pp: R S T : Type u_4
x✝⁴ : CommRing R
x✝³ : CommRing S
x✝² : CommRing T
x✝¹ : Algebra R S
x✝ : Algebra R T
h : Module.FaithfullyFlat R S
h' : Module.Finite S (S ⊗[R] T)
⊢ Module.Finite R T

Tactic:
exact .of_finite_tensorProduct_of_faithfullyFlat S

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent

Goal state before:
pp: X : Scheme
Z : Set ↥X
hZ : Z ∈ irreducibleComponents ↥X
inst✝¹ : IsNoetherian X
inst✝ : IrreducibleSpace ↥X
⊢ X.irreducibleComponentOpen Z = ⊤

Tactic:
by
  rw [irreducibleComponents_eq_singleton, Set.mem_singleton_iff] at hZ
  simp [irreducibleComponentOpen, irreducibleComponents_eq_singleton, hZ]

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'
map₂_leftUnitor : ∀ {a b : B} (f : a ⟶ b), map₂ (λ_ f).inv = (λ_ (map f)).inv ≫ eqToHom ⋯ ≫ mapComp (𝟙 a) f
a b : B
f : a ⟶ b
⊢ map f ≫ 𝟙 (obj b) = map f ≫ map (𝟙 b)

Tactic:
map_id b

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
obj : B → C
map : {X Y : B} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id : ∀ (X : B), map (𝟙 X) = 𝟙 (obj X)
map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (map f ⟶ map g)
map₂_id : ∀ {a b : B} (f : a ⟶ b), map₂ (𝟙 f) = 𝟙 (map f)
map₂_comp : ∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h), map₂ (η ≫ θ) = map₂ η ≫ map₂ θ
mapComp : {a b c : B} → (f : a ⟶ b) → (g : b ⟶ c) → map f ≫ map g ⟶ map (f ≫ g)
mapComp_naturality_left :
  ∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c), mapComp f g ≫ map₂ (η ▷ g) = map₂ η ▷ map g ≫ mapComp f' g
mapComp_naturality_right :
  ∀ {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g'), mapComp f g ≫ map₂ (f ◁ η) = map f ◁ map₂ η ≫ mapComp f g'
map₂_leftUnitor : ∀ {a b : B} (f : a ⟶ b), map₂ (λ_ f).inv = (λ_ (map f)).inv ≫ eqToHom ⋯ ≫ mapComp (𝟙 a) f
a b : B
f : a ⟶ b
⊢ map f ≫ 𝟙 (obj b) = map f ≫ 𝟙 (obj b)
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
obj : B → C
map : {X Y : B} → (X ⟶ Y) → (obj X ⟶ obj Y)
toPrefunctor : B ⥤q C := { obj := obj, map := map }
map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (map f ⟶ map g)
toPrelaxFunctorStruct : PrelaxFunctorStruct B C := { toPrefunctor := toPrefunctor, map₂ := map₂ }
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₂ θ
toPrelaxFunctor : PrelaxFunctor B C :=
  { toPrelaxFunctorStruct := toPrelaxFunctorStruct, map₂_id := map₂_id, map₂_comp := map₂_comp }
map_id : ∀ (X : B), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {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 g' : b ⟶ c} (η : g ⟶ g'), map₂ (f ◁ η) = eqToHom ⋯ ≫ map f ◁ map₂ η ≫ eqToHom ⋯
map₂_whisker_right :
  ∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c), map₂ (η ▷ g) = eqToHom ⋯ ≫ map₂ η ▷ map g ≫ eqToHom ⋯
toStrictPseudofunctorPreCore : StrictPseudofunctorPreCore B C :=
  { toPrelaxFunctor := toPrelaxFunctor, map_id := map_id, map_comp := map_comp, map₂_whisker_left := map₂_whisker_left,
    map₂_whisker_right := map₂_whisker_right }
map₂_left_unitor : ∀ {a b : B} (f : a ⟶ b), map₂ (λ_ f).hom = eqToHom ⋯ ≫ (λ_ (map f)).hom
a b : B
f : a ⟶ b
⊢ map f ≫ map (𝟙 b) = map f ≫ 𝟙 (obj b)

Tactic:
map_id b

Goal state after:
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)
toPrefunctor : B ⥤q C := { obj := obj, map := map }
map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (map f ⟶ map g)
toPrelaxFunctorStruct : PrelaxFunctorStruct B C := { toPrefunctor := toPrefunctor, map₂ := map₂ }
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₂ θ
toPrelaxFunctor : PrelaxFunctor B C :=
  { toPrelaxFunctorStruct := toPrelaxFunctorStruct, map₂_id := map₂_id, map₂_comp := map₂_comp }
map_id : ∀ (X : B), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {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 g' : b ⟶ c} (η : g ⟶ g'), map₂ (f ◁ η) = eqToHom ⋯ ≫ map f ◁ map₂ η ≫ eqToHom ⋯
map₂_whisker_right :
  ∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c), map₂ (η ▷ g) = eqToHom ⋯ ≫ map₂ η ▷ map g ≫ eqToHom ⋯
toStrictPseudofunctorPreCore : StrictPseudofunctorPreCore B C :=
  { toPrelaxFunctor := toPrelaxFunctor, map_id := map_id, map_comp := map_comp, map₂_whisker_left := map₂_whisker_left,
    map₂_whisker_right := map₂_whisker_right }
map₂_left_unitor : ∀ {a b : B} (f : a ⟶ b), map₂ (λ_ f).hom = eqToHom ⋯ ≫ (λ_ (map f)).hom
a b : B
f : a ⟶ b
⊢ map f ≫ 𝟙 (obj b) = map f ≫ 𝟙 (obj b)
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

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

Tactic:
map_id b

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

Goal state before:
pp: R✝¹ R✝ A R : CommRingCat
⊢ algΓ R ⊣ algSpec R

Tactic:
have overAdjunction := Over.postAdjunctionRight (Y := .op <| R) ΓSpec.adjunction

Goal state after:
R✝¹ R✝ A R : CommRingCat
overAdjunction : Over.post Γ.rightOp ⋙ Over.map (ΓSpec.adjunction.counit.app (op R)) ⊣ Over.post Scheme.Spec
⊢ algΓ R ⊣ algSpec R
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 ≫ 𝟙 a) ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 (𝟙 b ≫ g) =
    g ◁ η ⊗≫ g ◁ leftZigzag η ε ▷ g ⊗≫ ε ▷ g

Tactic:
rw [← whisker_exchange, ← whisker_exchange, leftZigzag]

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 ≫ 𝟙 a) ⊗≫ g ◁ (𝟙 a ◁ η ≫ η ▷ (f ≫ g)) ⊗≫ ((g ≫ f) ◁ ε ≫ ε ▷ 𝟙 b) ▷ g ⊗≫ 𝟙 (𝟙 b ≫ g) =
    g ◁ η ⊗≫ g ◁ (η ▷ f ⊗≫ f ◁ ε) ▷ g ⊗≫ ε ▷ g
Module: Mathlib.Topology.Sheaves.Over

Goal state before:
pp: case mp
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
⊢ (∀ x ∈ U.overEquivalence.functor.obj V,
      ∃ V_1 f, S.arrows (U.overEquivalence.inverse.map f ≫ U.overEquivalence.unitInv.app V) ∧ x ∈ V_1) →
    S ∈ ((Opens.grothendieckTopology X).over U) V

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
⊢ S ∈ ((Opens.grothendieckTopology X).over U) V →
    ∀ 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:
· intro H x hxV
      obtain ⟨W, f, hW, hxW⟩ := H ⟨x, V.hom.le hxV⟩ hxV
      exact ⟨_, ((U.overEquivalence.symm.toAdjunction.homEquiv _ _ ).symm f).left,
        ⟨_, _, 𝟙 _, hW, rfl⟩, _, hxW, rfl⟩

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
⊢ S ∈ ((Opens.grothendieckTopology X).over U) V →
    ∀ x ∈ U.overEquivalence.functor.obj V,
      ∃ V_1 f, S.arrows (U.overEquivalence.inverse.map f ≫ U.overEquivalence.unitInv.app V) ∧ x ∈ V_1
Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation

Goal state before:
pp: R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
⊢ ∃ S' x x_1,
    ∃ (_ : Module.Finite R S') (_ : Free R S') (_ : Algebra.FinitePresentation R S'), ∃ f, Function.Surjective ⇑f

Tactic:
obtain ⟨s, hs⟩ : (⊤ : Submodule R S).FG := Module.finite_def.mp inferInstance
  suffices h : ∃ (S' : Type u) (_ : CommRing S') (_ : Algebra R S') (_ : Module.Finite R S')
      (_ : Module.Free R S') (_ : Algebra.FinitePresentation R S')
      (f : S' →ₐ[R] S), (s : Set S) ⊆ AlgHom.range f by
    obtain ⟨S', _, _, _, _, _, f, hsf⟩ := h
    have hf : Function.Surjective f := by
      have := (Submodule.span_le (p := LinearMap.range f.toLinearMap)).mpr hsf
      rwa [hs, top_le_iff, LinearMap.range_eq_top] at this
    use S', ‹_›, ‹_›, ‹_›, ‹_›, ‹_›, f
  clear hs
  induction s using Finset.induction with
  | empty =>
    exact ⟨R, _, _, inferInstance, inferInstance, inferInstance, Algebra.ofId R S, by simp⟩
  | insert a s has IH =>
    obtain ⟨S', _, _, _, _, _, f, hsf⟩ := IH
    have ha := Algebra.IsIntegral.isIntegral (R := R) a
    have := ((minpoly.monic ha).map (algebraMap R S')).finite_adjoinRoot
    have := ((minpoly.monic ha).map (algebraMap R S')).free_adjoinRoot
    algebraize [f.toRingHom]
    refine ⟨AdjoinRoot ((minpoly R a).map (algebraMap R S')), inferInstance, inferInstance,
      .trans S' _, .trans (S := S'), .trans _ S' _,
      (AdjoinRoot.liftAlgHom _ (Algebra.ofId _ _) a
        (by simp [← Polynomial.aeval_def])).restrictScalars R, ?_⟩
    simp only [Finset.coe_insert, AlgHom.coe_range, AlgHom.coe_restrictScalars',
      Set.insert_subset_iff, Set.mem_range]
    exact ⟨⟨.root _, by simp⟩, hsf.trans fun y ⟨x, hx⟩ ↦ ⟨.of _ x, by simpa⟩⟩

Goal state after: