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

Goal state before:
pp: case map₂
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @PrelaxFunctorStruct.map₂ B inst✝¹.toQuiver (fun a b ↦ (homCategory a b).toQuiver) C inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) ((id B).comp F).toPrelaxFunctorStruct ≍
    @PrelaxFunctorStruct.map₂ B inst✝¹.toQuiver (fun a b ↦ (homCategory a b).toQuiver) C inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) F.toPrelaxFunctorStruct

Tactic:
rw [heq_iff_eq]
    ext
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

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

Tactic:
rw [heq_iff_eq]
    ext
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: case mapComp
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @LaxFunctor.mapComp B inst✝¹ C inst✝ ((id B).comp F).toLaxFunctor ≍
    @LaxFunctor.mapComp B inst✝¹ C inst✝ F.toLaxFunctor

Tactic:
rw [heq_iff_eq]
    ext
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: case map
B : Type u₁
inst✝³ : Bicategory B
C : Type u₂
inst✝² : Bicategory C
D : Type u₃
inst✝¹ : Bicategory D
E : Type u₄
inst✝ : Bicategory E
F : StrictlyUnitaryLaxFunctor B C
G : StrictlyUnitaryLaxFunctor C D
H : StrictlyUnitaryLaxFunctor D E
⊢ @Prefunctor.map B inst✝³.toQuiver E inst✝.toQuiver ((F.comp G).comp H).toPrefunctor ≍
    @Prefunctor.map B inst✝³.toQuiver E inst✝.toQuiver (F.comp (G.comp H)).toPrefunctor

Tactic:
rw [heq_iff_eq]
    ext
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: case map₂
B : Type u₁
inst✝³ : Bicategory B
C : Type u₂
inst✝² : Bicategory C
D : Type u₃
inst✝¹ : Bicategory D
E : Type u₄
inst✝ : Bicategory E
F : StrictlyUnitaryLaxFunctor B C
G : StrictlyUnitaryLaxFunctor C D
H : StrictlyUnitaryLaxFunctor D E
⊢ @PrelaxFunctorStruct.map₂ B inst✝³.toQuiver (fun a b ↦ (homCategory a b).toQuiver) E inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) ((F.comp G).comp H).toPrelaxFunctorStruct ≍
    @PrelaxFunctorStruct.map₂ B inst✝³.toQuiver (fun a b ↦ (homCategory a b).toQuiver) E inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) (F.comp (G.comp H)).toPrelaxFunctorStruct

Tactic:
rw [heq_iff_eq]
    ext
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: case mapId
B : Type u₁
inst✝³ : Bicategory B
C : Type u₂
inst✝² : Bicategory C
D : Type u₃
inst✝¹ : Bicategory D
E : Type u₄
inst✝ : Bicategory E
F : StrictlyUnitaryLaxFunctor B C
G : StrictlyUnitaryLaxFunctor C D
H : StrictlyUnitaryLaxFunctor D E
⊢ ((F.comp G).comp H).mapId ≍ (F.comp (G.comp H)).mapId

Tactic:
rw [heq_iff_eq]
    ext
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: case mapComp
B : Type u₁
inst✝³ : Bicategory B
C : Type u₂
inst✝² : Bicategory C
D : Type u₃
inst✝¹ : Bicategory D
E : Type u₄
inst✝ : Bicategory E
F : StrictlyUnitaryLaxFunctor B C
G : StrictlyUnitaryLaxFunctor C D
H : StrictlyUnitaryLaxFunctor D E
⊢ @LaxFunctor.mapComp B inst✝³ E inst✝ ((F.comp G).comp H).toLaxFunctor ≍
    @LaxFunctor.mapComp B inst✝³ E inst✝ (F.comp (G.comp H)).toLaxFunctor

Tactic:
rw [heq_iff_eq]
    ext
    simp

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g f' : a ⟶ b
η θ : f ≅ g
η_f : 𝟙 a ≫ f ≅ f'
η_g : 𝟙 a ≫ g ≅ f'
h_η : 𝟙 a ◁ η ≪≫ η_g = η_f
h_θ : 𝟙 a ◁ θ ≪≫ η_g = η_f
⊢ η = θ

Tactic:
apply Iso.ext

Goal state after:
B : Type u
inst✝ : Bicategory B
a b : B
f g f' : a ⟶ b
η θ : f ≅ g
η_f : 𝟙 a ≫ f ≅ f'
η_g : 𝟙 a ≫ g ≅ f'
h_η : 𝟙 a ◁ η ≪≫ η_g = η_f
h_θ : 𝟙 a ◁ θ ≪≫ η_g = η_f
⊢ η.hom = θ.hom
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'
⊢ adj.toCat.comp adj'.toCat = (adj.comp adj').toCat

Tactic:
cat_disch

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
⊢ leftZigzagIso η (adjointifyCounit η ε) = λ_ f ≪≫ (ρ_ f).symm

Tactic:
apply Iso.ext

Goal state after:
B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ (leftZigzagIso η (adjointifyCounit η ε)).hom = (λ_ f ≪≫ (ρ_ f).symm).hom
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d e f : B
g : c ⟶ e
h : d ⟶ f
l₁ : c ⟶ d
r₁ : d ⟶ c
l₂ : e ⟶ f
r₂ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : g ≫ l₂ ⟶ l₁ ≫ h
⊢ adj₁.homEquiv₁ (adj₂.homEquiv₂ α ≫ (α_ l₁ h r₂).hom) =
    𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h ▷ r₂ ⊗≫ 𝟙 (h ≫ r₂)

Tactic:
Adjunction.homEquiv₂_apply,

Goal state after:
B : Type u
inst✝ : Bicategory B
c d e f : B
g : c ⟶ e
h : d ⟶ f
l₁ : c ⟶ d
r₁ : d ⟶ c
l₂ : e ⟶ f
r₂ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : g ≫ l₂ ⟶ l₁ ≫ h
⊢ adj₁.homEquiv₁ (((ρ_ g).inv ≫ g ◁ adj₂.unit ≫ (α_ g l₂ r₂).inv ≫ α ▷ r₂) ≫ (α_ l₁ h r₂).hom) =
    𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h ▷ r₂ ⊗≫ 𝟙 (h ≫ r₂)
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' x x_1,
    ∃ (_ : Etale R R'),
      ∃ P,
        ∃ (x_3 : P.IsPrime) (x_4 : P.LiesOver p),
          ∃ n e,
            ∃ (_ : CompleteOrthogonalIdempotents e),
              ∃ P',
                ∃ (_ : ∀ (i : Fin n), (P' i).IsPrime) (_ : ∀ (i : Fin n), (P' i).LiesOver P),
                  Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) ∧
                    (∀ (i : Fin n), e i.castSucc ∉ P' i) ∧
                      ∀ (P'' : Ideal (R' ⊗[R] S)),
                        P''.IsPrime →
                          P''.LiesOver P → e (Fin.last n) ∈ P'' ∧ ∀ (i : Fin n), e i.castSucc ∉ P'' → P'' = P' i

Tactic:
by
  have ⟨R', _, _, _, P, _, _, n, e, he, P', _, _, hP, hP', H⟩ :=
    exists_etale_completeOrthogonalIdempotents_forall_liesOver_eq' (S := ULift.{u} S) p
  let e₁ : R' ⊗[R] S ≃ₐ[R'] R' ⊗[R] ULift.{u} S :=
    Algebra.TensorProduct.congr .refl ULift.algEquiv.symm
  refine ⟨R', _, _, ‹_›, P, ‹_›, ‹_›, n, e₁.symm ∘ e, he.map _,
    fun i ↦ (P' i).comap e₁.toAlgHom, inferInstance, inferInstance, hP, by simpa,
    fun P'' _ _ ↦ ?_⟩
  have := H (P''.comap e₁.symm.toAlgHom) inferInstance inferInstance
  refine ⟨by simpa using this.1, fun i hi ↦ ?_⟩
  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
p : PrimeSpectrum R
⊢ 0 < Module.rankAtStalk S p ↔ p ∈ Set.range (comap (algebraMap R S))

Tactic:
Module.rankAtStalk_eq,

Goal state after:
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
p : PrimeSpectrum R
⊢ 0 < Module.finrank p.asIdeal.ResidueField (p.asIdeal.Fiber S) ↔ p ∈ Set.range (comap (algebraMap R S))
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
h : Function.Surjective (comap (algebraMap R S))
p : Ideal R
inst✝ : p.IsMaximal
Q : Ideal S
isPrime✝ : Q.IsPrime
hQ : comap (algebraMap R S) { asIdeal := Q, isPrime := isPrime✝ } = { asIdeal := p, isPrime := ⋯ }
⊢ FaithfulSMul (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S)

Tactic:
have : Q.LiesOver p := ⟨congr($(hQ).asIdeal).symm⟩

Goal state after:
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
h : Function.Surjective (comap (algebraMap R S))
p : Ideal R
inst✝ : p.IsMaximal
Q : Ideal S
isPrime✝ : Q.IsPrime
hQ : comap (algebraMap R S) { asIdeal := Q, isPrime := isPrime✝ } = { asIdeal := p, isPrime := ⋯ }
this : Q.LiesOver p
⊢ FaithfulSMul (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case inr
X : Scheme
x : ↥X
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
this :
  ∀ {X : Scheme} (x : ↥X) (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f],
    (∃ S, X = Spec S) → 1 ≤ finrank f (f x)
hX : ¬∃ S, X = Spec S
x✝ : IsAffine X
heq : f x = (X.isoSpec.inv ≫ f) (X.isoSpec.hom x)
⊢ 1 ≤ finrank f (f x)

Tactic:
← finrank_comp_left_of_isIso X.isoSpec.inv,

Goal state after:
case inr
X : Scheme
x : ↥X
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
this :
  ∀ {X : Scheme} (x : ↥X) (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f],
    (∃ S, X = Spec S) → 1 ≤ finrank f (f x)
hX : ¬∃ S, X = Spec S
x✝ : IsAffine X
heq : f x = (X.isoSpec.inv ≫ f) (X.isoSpec.hom x)
⊢ 1 ≤ finrank (X.isoSpec.inv ≫ f) (f x)
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra S R
a : S
h : IsUnit a
x : R
⊢ ord R (a • x) = ord R x

Tactic:
rw [Algebra.smul_def a x]

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra S R
a : S
h : IsUnit a
x : R
⊢ ord R ((algebraMap S R) a * x) = ord R x
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
r₁ : b ⟶ a
l₂ : b ⟶ c
r₂ : c ⟶ b
l₃ : d ⟶ e
r₃ : e ⟶ d
l₄ : e ⟶ f
r₄ : f ⟶ e
l₅ : x ⟶ y
r₅ : y ⟶ x
l₆ : y ⟶ z
r₆ : z ⟶ y
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
adj₅ : l₅ ⊣ r₅
adj₆ : l₆ ⊣ r₆
α : g₁ ≫ l₃ ⟶ l₁ ≫ h₁
β : h₁ ≫ l₄ ⟶ l₂ ≫ k₁
γ : g₂ ≫ l₅ ⟶ l₃ ≫ h₂
δ : h₂ ≫ l₆ ⟶ l₄ ≫ k₂
⊢ (mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆)) (leftAdjointSquare.comp α β γ δ) =
    rightAdjointSquare.comp ((mateEquiv adj₁ adj₃) α) ((mateEquiv adj₂ adj₄) β) ((mateEquiv adj₃ adj₅) γ)
      ((mateEquiv adj₄ adj₆) δ)

Tactic:
have vcomp :=
    mateEquiv_vcomp (adj₁.comp adj₂) (adj₃.comp adj₄) (adj₅.comp adj₆)
      (leftAdjointSquare.hcomp α β) (leftAdjointSquare.hcomp γ δ)

Goal state after:
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
r₁ : b ⟶ a
l₂ : b ⟶ c
r₂ : c ⟶ b
l₃ : d ⟶ e
r₃ : e ⟶ d
l₄ : e ⟶ f
r₄ : f ⟶ e
l₅ : x ⟶ y
r₅ : y ⟶ x
l₆ : y ⟶ z
r₆ : z ⟶ y
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
adj₅ : l₅ ⊣ r₅
adj₆ : l₆ ⊣ r₆
α : g₁ ≫ l₃ ⟶ l₁ ≫ h₁
β : h₁ ≫ l₄ ⟶ l₂ ≫ k₁
γ : g₂ ≫ l₅ ⟶ l₃ ≫ h₂
δ : h₂ ≫ l₆ ⟶ l₄ ≫ k₂
vcomp :
  (mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆))
      (leftAdjointSquare.vcomp (leftAdjointSquare.hcomp α β) (leftAdjointSquare.hcomp γ δ)) =
    rightAdjointSquare.vcomp ((mateEquiv (adj₁.comp adj₂) (adj₃.comp adj₄)) (leftAdjointSquare.hcomp α β))
      ((mateEquiv (adj₃.comp adj₄) (adj₅.comp adj₆)) (leftAdjointSquare.hcomp γ δ))
⊢ (mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆)) (leftAdjointSquare.comp α β γ δ) =
    rightAdjointSquare.comp ((mateEquiv adj₁ adj₃) α) ((mateEquiv adj₂ adj₄) β) ((mateEquiv adj₃ adj₅) γ)
      ((mateEquiv adj₄ adj₆) δ)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: case mp
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : f ∉ z.asHomogeneousIdeal
⊢ ∃ u ∈ Set.range fun i ↦ basicOpen 𝒜 ((GradedRing.proj 𝒜 i) f), z ∈ u

Tactic:
rcases show ∃ i, GradedRing.proj 𝒜 i f ∉ z.asHomogeneousIdeal by
          contrapose! hz with H
          classical
          rw [← DirectSum.sum_support_decompose 𝒜 f]
          apply Ideal.sum_mem _ fun i _ => H i with ⟨i, hi⟩
        exact ⟨basicOpen 𝒜 (GradedRing.proj 𝒜 i f), ⟨i, rfl⟩, by rwa [mem_basicOpen]⟩

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 𝒜
⊢ ∀ {X Y : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ} (f : X ⟶ Y),
    (structurePresheafInCommRing 𝒜 ⋙ forget CommRingCat).map f ≫
        (Iso.refl ((structurePresheafInCommRing 𝒜 ⋙ forget CommRingCat).obj Y)).hom =
      (Iso.refl ((structurePresheafInCommRing 𝒜 ⋙ forget CommRingCat).obj X)).hom ≫ (structureSheafInType 𝒜).obj.map f

Tactic:
cat_disch

Goal state after:
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
f✝ : X ⟶ Y
g✝ : Y ⟶ Z
h : Z ⟶ T
f g : X ⟶ Y
hf : f = g
⊢ Hom.toRingCatSheafHom f ≫
      (Functor.sheafPushforwardContinuousNatTrans (Opens.mapIso g.base f.base ⋯).hom RingCat
            (Opens.grothendieckTopology ↥Y) (Opens.grothendieckTopology ↥X)).app
        X.ringCatSheaf =
    Hom.toRingCatSheafHom g

Tactic:
cat_disch

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Radical

Goal state before:
pp: case homogeneous_mem_or_mem.refine_1
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : I.IsPrime
x y : A
hx : IsHomogeneousElem 𝒜 x
hy : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal
H : x ∈ I ∨ y ∈ I
⊢ x ∈ I → x ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal

pp: case homogeneous_mem_or_mem.refine_2
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : I.IsPrime
x y : A
hx : IsHomogeneousElem 𝒜 x
hy : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal
H : x ∈ I ∨ y ∈ I
⊢ y ∈ I → y ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal

Tactic:
· exact Ideal.mem_homogeneousCore_of_homogeneous_of_mem hx

Goal state after:
case homogeneous_mem_or_mem.refine_2
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
h : I.IsPrime
x y : A
hx : IsHomogeneousElem 𝒜 x
hy : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal
H : x ∈ I ∨ y ∈ I
⊢ y ∈ I → y ∈ (Ideal.homogeneousCore 𝒜 I).toIdeal
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝¹ : CommRing A
inst✝ : SetLike σ A
𝒜 : ι → σ
x : Submonoid A
i1 : ι
n1 : A
hn1 : n1 ∈ 𝒜 i1
d1 : A
hd1 : d1 ∈ 𝒜 i1
h1 : ↑⟨d1, hd1⟩ ∈ x
i2 : ι
n2 : A
hn2 : n2 ∈ 𝒜 i2
d2 : A
hd2 : d2 ∈ 𝒜 i2
h2 : ↑⟨d2, hd2⟩ ∈ x
hdeg :
  { deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 }.deg =
    { deg := i2, num := ⟨n2, hn2⟩, den := ⟨d2, hd2⟩, den_mem := h2 }.deg
hnum :
  ↑{ deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 }.num =
    ↑{ deg := i2, num := ⟨n2, hn2⟩, den := ⟨d2, hd2⟩, den_mem := h2 }.num
hden :
  ↑{ deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 }.den =
    ↑{ deg := i2, num := ⟨n2, hn2⟩, den := ⟨d2, hd2⟩, den_mem := h2 }.den
⊢ { deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 } =
    { deg := i2, num := ⟨n2, hn2⟩, den := ⟨d2, hd2⟩, den_mem := h2 }

Tactic:
dsimp only [Subtype.coe_mk] at *

Goal state after:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝¹ : CommRing A
inst✝ : SetLike σ A
𝒜 : ι → σ
x : Submonoid A
i1 : ι
n1 : A
hn1 : n1 ∈ 𝒜 i1
d1 : A
hd1 : d1 ∈ 𝒜 i1
h1 : ↑⟨d1, hd1⟩ ∈ x
i2 : ι
n2 : A
hn2 : n2 ∈ 𝒜 i2
d2 : A
hd2 : d2 ∈ 𝒜 i2
h2 : ↑⟨d2, hd2⟩ ∈ x
hdeg : i1 = i2
hnum : n1 = n2
hden : d1 = d2
⊢ { deg := i1, num := ⟨n1, hn1⟩, den := ⟨d1, hd1⟩, den_mem := h1 } =
    { deg := i2, num := ⟨n2, hn2⟩, den := ⟨d2, hd2⟩, den_mem := h2 }
Module: Mathlib.RingTheory.GradedAlgebra.Radical

Goal state before:
pp: case a
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
J : Ideal A
HJ₁ : I ≤ J
HJ₂ : J.IsPrime
⊢ I ≤ (homogeneousCore 𝒜 J).toIdeal

Tactic:
exact hI.toIdeal_homogeneousCore_eq_self.symm.trans_le (Ideal.homogeneousCore_mono _ HJ₁)

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Radical

Goal state before:
pp: case a
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
⊢ InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime} ≤ InfSet.sInf {J | I ≤ J ∧ J.IsPrime}

Tactic:
· refine sInf_le_sInf_of_isCoinitialFor ?_
    rintro J ⟨HJ₁, HJ₂⟩
    refine ⟨(J.homogeneousCore 𝒜).toIdeal, ?_, J.toIdeal_homogeneousCore_le _⟩
    refine ⟨HomogeneousIdeal.isHomogeneous _, ?_, HJ₂.homogeneousCore⟩
    exact hI.toIdeal_homogeneousCore_eq_self.symm.trans_le (Ideal.homogeneousCore_mono _ HJ₁)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: case refine_1.refine_2
X Y Z T : Scheme
M✝ N K : X.Modules
φ✝ : M✝ ⟶ N
U V : X.Opens
R S : CommRingCat
φ : R ⟶ S
M : Sheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))
⊢ ∀ {X Y : (TopologicalSpace.Opens ↥(Spec R))ᵒᵖ} (f : X ⟶ Y),
    ((sheafCompose (Opens.grothendieckTopology ↥(Spec S))
                      (ModuleCat.restrictScalars (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ)))) ⋙
                    TopCat.Sheaf.pushforward (ModuleCat ↑Γ(Spec R, ⊤)) (Spec.map φ).base ⋙
                      sheafCompose (Opens.grothendieckTopology ↥(Spec R))
                        (ModuleCat.restrictScalars (CommRingCat.Hom.hom (ΓSpecIso R).inv))).obj
                M).obj.map
          f ≫
        ((ModuleCat.restrictScalarsComp'App (CommRingCat.Hom.hom (ΓSpecIso R).inv)
                (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ)))
                ((CommRingCat.Hom.hom (ΓSpecIso S).inv).comp (CommRingCat.Hom.hom φ)) ⋯
                (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj M).obj
                  ((Opens.map (Spec.map φ).base).op.obj Y))).symm ≪≫
            (ModuleCat.restrictScalarsComp (CommRingCat.Hom.hom φ) (CommRingCat.Hom.hom (ΓSpecIso S).inv)).app
              (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj M).obj
                ((Opens.map (Spec.map φ).base).op.obj Y))).hom =
      ((ModuleCat.restrictScalarsComp'App (CommRingCat.Hom.hom (ΓSpecIso R).inv)
                (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ)))
                ((CommRingCat.Hom.hom (ΓSpecIso S).inv).comp (CommRingCat.Hom.hom φ)) ⋯
                (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj M).obj
                  ((Opens.map (Spec.map φ).base).op.obj X))).symm ≪≫
            (ModuleCat.restrictScalarsComp (CommRingCat.Hom.hom φ) (CommRingCat.Hom.hom (ΓSpecIso S).inv)).app
              (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj M).obj
                ((Opens.map (Spec.map φ).base).op.obj X))).hom ≫
        ((sheafCompose (Opens.grothendieckTopology ↥(Spec S))
                      (ModuleCat.restrictScalars (CommRingCat.Hom.hom (ΓSpecIso S).inv)) ⋙
                    TopCat.Sheaf.pushforward (ModuleCat ↑S) (Spec.map φ).base ⋙
                      sheafCompose (Opens.grothendieckTopology ↥(Spec R))
                        (ModuleCat.restrictScalars (CommRingCat.Hom.hom φ))).obj
                M).obj.map
          f

Tactic:
cat_disch

Goal state after:
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: case refine_2
X Y Z T : Scheme
M N K : X.Modules
φ✝ : M ⟶ N
U V : X.Opens
R S : CommRingCat
φ : R ⟶ S
⊢ ∀ {X Y : Sheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))} (f : X ⟶ Y),
    (sheafCompose (Opens.grothendieckTopology ↥(Spec S))
                (ModuleCat.restrictScalars (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ)))) ⋙
              TopCat.Sheaf.pushforward (ModuleCat ↑Γ(Spec R, ⊤)) (Spec.map φ).base ⋙
                sheafCompose (Opens.grothendieckTopology ↥(Spec R))
                  (ModuleCat.restrictScalars (CommRingCat.Hom.hom (ΓSpecIso R).inv))).map
          f ≫
        (ObjectProperty.isoMk (Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
            (NatIso.ofComponents
              (fun U ↦
                (ModuleCat.restrictScalarsComp'App (CommRingCat.Hom.hom (ΓSpecIso R).inv)
                      (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ)))
                      ((CommRingCat.Hom.hom (ΓSpecIso S).inv).comp (CommRingCat.Hom.hom φ)) ⋯
                      (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj Y).obj
                        ((Opens.map (Spec.map φ).base).op.obj U))).symm ≪≫
                  (ModuleCat.restrictScalarsComp (CommRingCat.Hom.hom φ) (CommRingCat.Hom.hom (ΓSpecIso S).inv)).app
                    (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj Y).obj
                      ((Opens.map (Spec.map φ).base).op.obj U)))
              ⋯)).hom =
      (ObjectProperty.isoMk (Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
            (NatIso.ofComponents
              (fun U ↦
                (ModuleCat.restrictScalarsComp'App (CommRingCat.Hom.hom (ΓSpecIso R).inv)
                      (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ)))
                      ((CommRingCat.Hom.hom (ΓSpecIso S).inv).comp (CommRingCat.Hom.hom φ)) ⋯
                      (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj X).obj
                        ((Opens.map (Spec.map φ).base).op.obj U))).symm ≪≫
                  (ModuleCat.restrictScalarsComp (CommRingCat.Hom.hom φ) (CommRingCat.Hom.hom (ΓSpecIso S).inv)).app
                    (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj X).obj
                      ((Opens.map (Spec.map φ).base).op.obj U)))
              ⋯)).hom ≫
        (sheafCompose (Opens.grothendieckTopology ↥(Spec S))
                (ModuleCat.restrictScalars (CommRingCat.Hom.hom (ΓSpecIso S).inv)) ⋙
              TopCat.Sheaf.pushforward (ModuleCat ↑S) (Spec.map φ).base ⋙
                sheafCompose (Opens.grothendieckTopology ↥(Spec R))
                  (ModuleCat.restrictScalars (CommRingCat.Hom.hom φ))).map
          f

Tactic:
cat_disch

Goal state after: