mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor

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

Tactic:
simpa using

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
S : StrictPseudofunctorCore B C
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
x✝¹ x✝ : b✝ ⟶ c✝
η : x✝¹ ⟶ x✝
⊢ S.map₂ (f ◁ η) = eqToHom ⋯ ≫ S.map f ◁ S.map₂ η ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor

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

Tactic:
simpa using

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
S : StrictPseudofunctorCore B C
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
f : b✝ ⟶ c✝
⊢ S.map₂ (η ▷ f) = eqToHom ⋯ ≫ S.map₂ η ▷ S.map f ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor

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

Tactic:
simpa using

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
S : StrictPseudofunctorCore B C
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ S.map₂ (α_ f g h).hom = eqToHom ⋯ ≫ (α_ (S.map f) (S.map g) (S.map h)).hom ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor

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

Tactic:
simpa using

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
S : StrictPseudofunctorCore B C
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ S.map₂ (λ_ f).hom = eqToHom ⋯ ≫ (λ_ (S.map f)).hom
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor

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

Tactic:
simpa using

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
S : StrictPseudofunctorCore B C
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ S.map₂ (ρ_ f).hom = eqToHom ⋯ ≫ (ρ_ (S.map f)).hom
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
inst✝¹ : Strict B
inst✝ : Strict C
S : StrictPseudofunctorPreCore B C
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
x✝¹ x✝ : b✝ ⟶ c✝
η : x✝¹ ⟶ x✝
⊢ S.map₂ (f ◁ η) = (eqToIso ⋯).hom ≫ S.map f ◁ S.map₂ η ≫ (eqToIso ⋯).inv

Tactic:
simpa using

Goal state after:
B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
inst✝¹ : Strict B
inst✝ : Strict C
S : StrictPseudofunctorPreCore B C
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
x✝¹ x✝ : b✝ ⟶ c✝
η : x✝¹ ⟶ x✝
⊢ S.map₂ (f ◁ η) = eqToHom ⋯ ≫ S.map f ◁ S.map₂ η ≫ eqToHom ⋯
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
inst✝¹ : Strict B
inst✝ : Strict C
S : StrictPseudofunctorPreCore B C
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
f : b✝ ⟶ c✝
⊢ S.map₂ (η ▷ f) = (eqToIso ⋯).hom ≫ S.map₂ η ▷ S.map f ≫ (eqToIso ⋯).inv

Tactic:
simpa using

Goal state after:
B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
inst✝¹ : Strict B
inst✝ : Strict C
S : StrictPseudofunctorPreCore B C
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
f : b✝ ⟶ c✝
⊢ S.map₂ (η ▷ f) = eqToHom ⋯ ≫ S.map₂ η ▷ S.map f ≫ eqToHom ⋯
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R : CommRingCat
X Y : (CommAlgCat ↑R)ᵒᵖ
⊢ (pullbackSpecIso ↑R ↑(unop X) ↑(unop Y)).inv ≫ ((algSpec R).obj X ⊗ (algSpec R).obj Y).hom =
    ((algSpec R).obj (X ⊗ Y)).hom

Tactic:
simpa using

Goal state after:
R : CommRingCat
X Y : (CommAlgCat ↑R)ᵒᵖ
⊢ Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom) ≫
      Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑(unop X))) =
    Spec.map (CommRingCat.ofHom (algebraMap (↑R) (↑(unop X) ⊗[↑R] ↑(unop Y))))
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
S : StrictlyUnitaryPseudofunctorCore B C
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
x✝¹ x✝ : b✝ ⟶ c✝
η : x✝¹ ⟶ x✝
⊢ S.map₂ (f ◁ η) = (S.mapComp f x✝¹).hom ≫ S.map f ◁ S.map₂ η ≫ (S.mapComp f x✝).inv

Tactic:
simpa using

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
S : StrictlyUnitaryPseudofunctorCore B C
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
x✝¹ x✝ : b✝ ⟶ c✝
η : x✝¹ ⟶ x✝
⊢ S.map₂ (f ◁ η) = (S.mapComp f x✝¹).hom ≫ S.map f ◁ S.map₂ η ≫ (S.mapComp f x✝).inv
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
S : StrictlyUnitaryPseudofunctorCore B C
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
f : b✝ ⟶ c✝
⊢ S.map₂ (η ▷ f) = (S.mapComp f✝ f).hom ≫ S.map₂ η ▷ S.map f ≫ (S.mapComp g✝ f).inv

Tactic:
simpa using

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
S : StrictlyUnitaryPseudofunctorCore B C
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
f : b✝ ⟶ c✝
⊢ S.map₂ (η ▷ f) = (S.mapComp f✝ f).hom ≫ S.map₂ η ▷ S.map f ≫ (S.mapComp g✝ f).inv
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
S : StrictlyUnitaryPseudofunctorCore B C
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ S.map₂ (α_ f g h).hom =
    (S.mapComp (f ≫ g) h).hom ≫
      (S.mapComp f g).hom ▷ S.map h ≫
        (α_ (S.map f) (S.map g) (S.map h)).hom ≫ S.map f ◁ (S.mapComp g h).inv ≫ (S.mapComp f (g ≫ h)).inv

Tactic:
simpa using

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
S : StrictlyUnitaryPseudofunctorCore B C
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ S.map₂ (α_ f g h).hom =
    (S.mapComp (f ≫ g) h).hom ≫
      (S.mapComp f g).hom ▷ S.map h ≫
        (α_ (S.map f) (S.map g) (S.map h)).hom ≫ S.map f ◁ (S.mapComp g h).inv ≫ (S.mapComp f (g ≫ h)).inv
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

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

Tactic:
simpa using

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
S : StrictlyUnitaryPseudofunctorCore B C
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ S.map₂ (λ_ f).hom = (S.mapComp (𝟙 a✝) f).hom ≫ eqToHom ⋯ ≫ (λ_ (S.map f)).hom
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

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

Tactic:
simpa using

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
S : StrictlyUnitaryPseudofunctorCore B C
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ S.map₂ (ρ_ f).hom = (S.mapComp f (𝟙 b✝)).hom ≫ eqToHom ⋯ ≫ (ρ_ (S.map f)).hom
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : Adj B
α : a ⟶ b
⊢ (conjugateEquiv α.adj (𝟙 a ≫ α).adj) (λ_ α.l).hom = (ρ_ α.r).symm.hom

Tactic:
simpa using

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d : Adj B
α : a ⟶ b
⊢ (conjugateEquiv α.adj ((Adjunction.id a.obj).comp α.adj)) (λ_ α.l).hom = (ρ_ α.r).inv
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : Adj B
α : a ⟶ b
⊢ (conjugateEquiv α.adj (𝟙 a ≫ α).adj) (λ_ α.l).hom = (ρ_ α.r).symm.hom

Tactic:
by simpa using conjugateEquiv_id_comp_right_apply α.adj α.adj (𝟙 _)

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : Adj B
α : a ⟶ b
⊢ (conjugateEquiv α.adj (α ≫ 𝟙 b).adj) (ρ_ α.l).hom = (λ_ α.r).symm.hom

Tactic:
simpa using

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d : Adj B
α : a ⟶ b
⊢ (conjugateEquiv α.adj (α.adj.comp (Adjunction.id b.obj))) (ρ_ α.l).hom = (λ_ α.r).inv
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Cat

Goal state before:
pp: C✝ D✝ E : Type u
inst✝² : Category.{v, u} C✝
inst✝¹ : Category.{v, u} D✝
inst✝ : Category.{v, u} E
F✝ : C✝ ⥤ D✝
G✝ : D✝ ⥤ C✝
adj✝ : F✝ ⊣ G✝
F' : D✝ ⥤ E
G' : E ⥤ D✝
adj' : F' ⊣ G'
C D : Cat
F : C ⟶ D
G : D ⟶ C
adj : F ⊣ G
X : ↑C
⊢ F.toFunctor.map (adj.unit.toNatTrans.app X) ≫ adj.counit.toNatTrans.app (F.toFunctor.obj X) = 𝟙 (F.toFunctor.obj X)

Tactic:
simpa using

Goal state after:
C✝ D✝ E : Type u
inst✝² : Category.{v, u} C✝
inst✝¹ : Category.{v, u} D✝
inst✝ : Category.{v, u} E
F✝ : C✝ ⥤ D✝
G✝ : D✝ ⥤ C✝
adj✝ : F✝ ⊣ G✝
F' : D✝ ⥤ E
G' : E ⥤ D✝
adj' : F' ⊣ G'
C D : Cat
F : C ⟶ D
G : D ⟶ C
adj : F ⊣ G
X : ↑C
⊢ F.toFunctor.map (adj.unit.toNatTrans.app X) ≫ adj.counit.toNatTrans.app (F.toFunctor.obj X) = 𝟙 (F.toFunctor.obj X)
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Cat

Goal state before:
pp: C✝ D✝ E : Type u
inst✝² : Category.{v, u} C✝
inst✝¹ : Category.{v, u} D✝
inst✝ : Category.{v, u} E
F✝ : C✝ ⥤ D✝
G✝ : D✝ ⥤ C✝
adj✝ : F✝ ⊣ G✝
F' : D✝ ⥤ E
G' : E ⥤ D✝
adj' : F' ⊣ G'
C D : Cat
F : C ⟶ D
G : D ⟶ C
adj : F ⊣ G
X : ↑D
⊢ adj.unit.toNatTrans.app (G.toFunctor.obj X) ≫ G.toFunctor.map (adj.counit.toNatTrans.app X) = 𝟙 (G.toFunctor.obj X)

Tactic:
simpa using

Goal state after:
C✝ D✝ E : Type u
inst✝² : Category.{v, u} C✝
inst✝¹ : Category.{v, u} D✝
inst✝ : Category.{v, u} E
F✝ : C✝ ⥤ D✝
G✝ : D✝ ⥤ C✝
adj✝ : F✝ ⊣ G✝
F' : D✝ ⥤ E
G' : E ⥤ D✝
adj' : F' ⊣ G'
C D : Cat
F : C ⟶ D
G : D ⟶ C
adj : F ⊣ G
X : ↑D
⊢ adj.unit.toNatTrans.app (G.toFunctor.obj X) ≫ G.toFunctor.map (adj.counit.toNatTrans.app X) = 𝟙 (G.toFunctor.obj 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✝¹ : 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
⊢ (⇑e₁.symm ∘ e) (Fin.last n) ∈ P''

Tactic:
simpa using

Goal state after:
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
⊢ e₁.symm (e (Fin.last n)) ∈ P''
Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation

Goal state before:
pp: case insert
R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
a : S
s : Finset S
has : a ∉ s
S' : Type u
w✝⁴ : CommRing S'
w✝³ : Algebra R S'
w✝² : Module.Finite R S'
w✝¹ : Free R S'
w✝ : Algebra.FinitePresentation R S'
f : S' →ₐ[R] S
hsf : ↑s ⊆ ↑f.range
ha : IsIntegral R a
this✝ : Module.Finite S' (AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a)))
this : Free S' (AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a)))
⊢ ∃ S' x x_1,
    ∃ (_ : Module.Finite R S') (_ : Free R S') (_ : Algebra.FinitePresentation R S'), ∃ f, ↑(insert a s) ⊆ ↑f.range

Tactic:
algebraize [f.toRingHom]

Goal state after:
case insert
R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
a : S
s : Finset S
has : a ∉ s
S' : Type u
w✝⁴ : CommRing S'
w✝³ : Algebra R S'
w✝² : Module.Finite R S'
w✝¹ : Free R S'
w✝ : Algebra.FinitePresentation R S'
f : S' →ₐ[R] S
hsf : ↑s ⊆ ↑f.range
ha : IsIntegral R a
this✝ : Module.Finite S' (AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a)))
this : Free S' (AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a)))
algInst✝ : Algebra S' S := f.toAlgebra
⊢ ∃ S' x x_1,
    ∃ (_ : Module.Finite R S') (_ : Free R S') (_ : Algebra.FinitePresentation R S'), ∃ f, ↑(insert a s) ⊆ ↑f.range
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case hy
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
⊢ x✝ = PrimeSpectrum.comap (CommRingCat.Hom.hom (ΓSpecIso R).inv) ((Spec R).isoSpec.hom x✝)

Tactic:
· simp [isoSpec_Spec_hom, SpecMap_ΓSpecIso_hom, ← AlgebraicGeometry.Spec.map_apply,
      ← Scheme.Hom.comp_apply, toSpecΓ_SpecMap_ΓSpecIso_inv]

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
hr : r ∈ R⁰
hr' : ¬Ideal.span {r} = ⊤
this✝¹ : Nonempty ↑(PrimeSpectrum.zeroLocus ↑(Ideal.span {r}))
this✝ : Nontrivial (R ⧸ Ideal.span {r})
this : Nontrivial R
l : LTSeries ↑(PrimeSpectrum.zeroLocus ↑(Ideal.span {r}))
p : Ideal R
hp : p ∈ ⊥.minimalPrimes
hp' : p ≤ (↑(RelSeries.head l)).asIdeal
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
h : p' = ↑(RelSeries.head l)
⊢ r ∈ p

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommRing R
r : R
hr : r ∈ R⁰
hr' : ¬Ideal.span {r} = ⊤
this✝¹ : Nonempty ↑(PrimeSpectrum.zeroLocus ↑(Ideal.span {r}))
this✝ : Nontrivial (R ⧸ Ideal.span {r})
this : Nontrivial R
l : LTSeries ↑(PrimeSpectrum.zeroLocus ↑(Ideal.span {r}))
p : Ideal R
hp : p ∈ ⊥.minimalPrimes
hp' : p ≤ (↑(RelSeries.head l)).asIdeal
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
h : p' = ↑(RelSeries.head l)
⊢ r ∈ p
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
σ : Type u_3
inst✝ : Finite σ
⊢ ringKrullDim R + ↑(Nat.card σ) ≤ ringKrullDim (MvPolynomial σ R)

Tactic:
induction σ using Finite.induction_empty_option with

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : R
hx : IsUnit x
⊢ ord R x = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommRing R
x : R
hx : IsUnit x
⊢ ord R x = 0
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: case neg
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
U : X.Opens
inst✝ : Nonempty ↥↑U
hxU : x ∈ U
a : ↑Γ(X, U)
ha : a ≠ 0
f : ↑X.functionField
hx : coheight x = 1
hf : ¬f = 0
this✝ : a • f ≠ 0
algInst✝ : Algebra ↑(X.presheaf.obj (Opposite.op U)) ↑(X.presheaf.stalk x) :=
  (CommRingCat.Hom.hom (X.presheaf.germ U x hxU)).toAlgebra
this : Ring.KrullDimLE 1 ↑(X.presheaf.stalk x)
⊢ (ordHom x hx) f ≤ (ordHom x hx) (a • f)

Tactic:
have : IsScalarTower ↑Γ(X, U) ↑(X.presheaf.stalk x) ↑X.functionField :=
    functionField_isScalarTower X U ⟨x, hxU⟩

Goal state after:
case neg
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
U : X.Opens
inst✝ : Nonempty ↥↑U
hxU : x ∈ U
a : ↑Γ(X, U)
ha : a ≠ 0
f : ↑X.functionField
hx : coheight x = 1
hf : ¬f = 0
this✝¹ : a • f ≠ 0
algInst✝ : Algebra ↑(X.presheaf.obj (Opposite.op U)) ↑(X.presheaf.stalk x) :=
  (CommRingCat.Hom.hom (X.presheaf.germ U x hxU)).toAlgebra
this✝ : Ring.KrullDimLE 1 ↑(X.presheaf.stalk x)
this : IsScalarTower ↑Γ(X, U) ↑(X.presheaf.stalk x) ↑X.functionField
⊢ (ordHom x hx) f ≤ (ordHom x hx) (a • f)
Module: Mathlib.AlgebraicGeometry.PointsPi

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

Tactic:
simpa using

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

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → ↑(R i))))
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
t : Finset ↑s
ht : V ⊆ ⋃ i ∈ t, (basicOpen ↑i).carrier
⊢ V ⊆ ⋃ i ∈ ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) t), (basicOpen i).carrier

Tactic:
simpa using

Goal state after:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → ↑(R i))))
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
t : Finset ↑s
ht : V ⊆ ⋃ i ∈ t, (basicOpen ↑i).carrier
⊢ V ⊆ ⋃ i, ⋃ (i_1 : i ∈ s), ⋃ (_ : ⟨i, ⋯⟩ ∈ t), (zeroLocus {i})ᶜ
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → ↑(R i))))
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
t : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ ⋃ i ∈ t, (basicOpen i).carrier
⊢ V ⊆ (zeroLocus t)ᶜ

Tactic:
simpa using

Goal state after:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → ↑(R i))))
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
t : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ ⋃ i ∈ t, (basicOpen i).carrier
⊢ V ⊆ (zeroLocus t)ᶜ
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → ↑(R i))))
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
t : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
this✝ : ∀ (i : ι), Ideal.span (⇑(Pi.evalRingHom (fun x ↦ ↑(R x)) i) '' t) = ⊤
this : Ideal.span s = ⊤
⊢ U = ⊤

Tactic:
simpa using

Goal state after:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → ↑(R i))))
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
t : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
this✝ : ∀ (i : ι), Ideal.span (⇑(Pi.evalRingHom (fun x ↦ ↑(R x)) i) '' t) = ⊤
this : Ideal.span s = ⊤
⊢ U = ⊤
Module: Mathlib.AlgebraicGeometry.PointsPi

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

Tactic:
simpa using

Goal state after:
ι : Type u
R : ι → CommRingCat
I : Ideal ((i : ι) → ↑(R i))
f : (∐ fun i ↦ Spec (R i)) ⟶ Spec (CommRingCat.of (((i : ι) → ↑(R i)) ⧸ I))
hf : f ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R
x : (i : ι) → ↑(R i)
hx : x ∈ I
i : ι
⊢ x i = 0
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₁
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂) α)
this : IsIso ((conjugateEquiv adj₁ adj₂).symm ((conjugateEquiv adj₁ adj₂) α))
⊢ IsIso α

Tactic:
simpa using

Goal state after:
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₁
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂) α)
this : IsIso ((conjugateEquiv adj₁ adj₂).symm ((conjugateEquiv adj₁ adj₂) α))
⊢ IsIso α
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₂
α : r₁ ⟶ r₂
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂).symm α)
this : IsIso ((conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α))
⊢ IsIso α

Tactic:
simpa using

Goal state after:
B : Type u
inst✝¹ : Bicategory B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : r₁ ⟶ r₂
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂).symm α)
this : IsIso ((conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α))
⊢ IsIso α