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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this✝ : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
W : TopologicalSpace.Opens ↥X
hW : W ∈ X.affineOpens
hxW : x ∈ ↑W
hWV : W ≤ toNormalization f ⁻¹ᵁ V y
this : IsAffine ↑W
V' : (normalization f).Opens := opensRange (X.homOfLE hWV ≫ toNormalization f ∣_ V y ≫ (V y).ι)
hV' : IsAffineOpen V'
hV'V : V' ≤ V y
hV'W : toNormalization f ⁻¹ᵁ V' = W
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
f₁ : ↑Γ(normalization f, fromNormalization f ⁻¹ᵁ U)
f₂ : ↑Γ(normalization f, V')
e : (normalization f).basicOpen f₁ = (normalization f).basicOpen f₂
hxf : (toNormalization f) x ∈ (normalization f).basicOpen f₁
⊢ ∃ U r,
    IsAffineOpen U ∧
      IsAffineOpen (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r) ∧
        x ∈ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r ∧ (normalization f).basicOpen r ≤ V y

Tactic:
refine ⟨U, f₁, hU, ?_, hxf, (e.trans_le (f.normalization.basicOpen_le _)).trans hV'V⟩

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this✝ : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
W : TopologicalSpace.Opens ↥X
hW : W ∈ X.affineOpens
hxW : x ∈ ↑W
hWV : W ≤ toNormalization f ⁻¹ᵁ V y
this : IsAffine ↑W
V' : (normalization f).Opens := opensRange (X.homOfLE hWV ≫ toNormalization f ∣_ V y ≫ (V y).ι)
hV' : IsAffineOpen V'
hV'V : V' ≤ V y
hV'W : toNormalization f ⁻¹ᵁ V' = W
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
f₁ : ↑Γ(normalization f, fromNormalization f ⁻¹ᵁ U)
f₂ : ↑Γ(normalization f, V')
e : (normalization f).basicOpen f₁ = (normalization f).basicOpen f₂
hxf : (toNormalization f) x ∈ (normalization f).basicOpen f₁
⊢ IsAffineOpen (toNormalization f ⁻¹ᵁ (normalization f).basicOpen f₁)
Module: Mathlib.RingTheory.Etale.Descent

Goal state before:
pp: case left
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✝ : Smooth T (T ⊗[R] S)
this : FinitePresentation R S
x✝ : Algebra T (S ⊗[R] T) := TensorProduct.rightAlgebra
e : S ⊗[R] T ≃ₐ[T] T ⊗[R] S := AlgEquiv.ofRingEquiv ⋯
⊢ Module.Projective S Ω[S⁄R]

Tactic:
have : FormallySmooth T (S ⊗[R] T) := .of_equiv e.symm

Goal state after:
case left
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✝ : Smooth T (T ⊗[R] S)
this✝ : FinitePresentation R S
x✝ : Algebra T (S ⊗[R] T) := TensorProduct.rightAlgebra
e : S ⊗[R] T ≃ₐ[T] T ⊗[R] S := AlgEquiv.ofRingEquiv ⋯
this : FormallySmooth T (S ⊗[R] T)
⊢ Module.Projective S Ω[S⁄R]
Module: Mathlib.AlgebraicGeometry.LimitsOver

Goal state before:
pp: X : Scheme
P : MorphismProperty Scheme
inst✝⁵ : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst✝⁴ : Category.{v_1, u_1} J
F : J ⥤ P.Over ⊤ S
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).left
inst✝² : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, u_1} J
this : HasColimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)
e : (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).left ≅
  colimit ((F ⋙ MorphismProperty.Over.forget P ⊤ S) ⋙ Over.forget S) :=
  preservesColimitIso (Over.forget S) (F ⋙ MorphismProperty.Over.forget P ⊤ S)
𝒰 : (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).left.OpenCover :=
  Scheme.Cover.pushforwardIso
    (Scheme.IsLocallyDirected.openCover ((F ⋙ MorphismProperty.Over.forget P ⊤ S) ⋙ Over.forget S)) e.inv
i : 𝒰.I₀
⊢ P (𝒰.f i ≫ (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).hom)

Tactic:
simpa [𝒰, e] using! (F.obj i).prop

Goal state after:
Module: Mathlib.AlgebraicGeometry.LimitsOver

Goal state before:
pp: X : Scheme
P : MorphismProperty Scheme
inst✝⁵ : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst✝⁴ : Category.{v_1, u_1} J
F : J ⥤ P.Over ⊤ S
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).left
inst✝² : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, u_1} J
j : J
e : (colimit F).left ≅ colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) :=
  preservesColimitIso (MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) F
⊢ IsOpenImmersion ((MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S).map (colimit.ι F j))

Tactic:
rw [← MorphismProperty.cancel_right_of_respectsIso (P := @IsOpenImmersion) _ e.hom]

Goal state after:
X : Scheme
P : MorphismProperty Scheme
inst✝⁵ : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst✝⁴ : Category.{v_1, u_1} J
F : J ⥤ P.Over ⊤ S
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).left
inst✝² : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, u_1} J
j : J
e : (colimit F).left ≅ colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) :=
  preservesColimitIso (MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) F
⊢ IsOpenImmersion ((MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S).map (colimit.ι F j) ≫ e.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
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
map₂_right_unitor : ∀ {a b : B} (f : a ⟶ b), map₂ (ρ_ f).hom = eqToHom ⋯ ≫ (ρ_ (map f)).hom
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ map ((f ≫ g) ≫ h) = (map f ≫ map g) ≫ map h

Tactic:
by simp only [map_comp]

Goal state after:
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
map₂_right_unitor : ∀ {a b : B} (f : a ⟶ b), map₂ (ρ_ f).hom = eqToHom ⋯ ≫ (ρ_ (map f)).hom
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ map f ≫ map g ≫ map h = map (f ≫ g ≫ h)

Tactic:
by simp only [map_comp]

Goal state after:
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 Over.w (prodComparison (algSpec R) X Y)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R : CommRingCat
⊢ Over.Hom.left (Over.homMk (𝟙 (Spec R)) ⋯) = Over.Hom.left (OplaxMonoidal.η (algSpec R))

Tactic:
by
      rw [Functor.OplaxMonoidal.η_of_cartesianMonoidalCategory, ← preservesTerminalIso_hom,
        preservesTerminalIso_algSpec]; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: case h₀
R✝¹ R✝ A : CommRingCat
X M G : Scheme
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Bialgebra R T
⊢ (Over.Hom.left
          (η ≫
            Hom.asOver
              (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ≪≫ pullbackSpecIso' R S T).hom
              (Spec (of S))) ≫
        (pullbackSpecIso' R S T).inv) ≫
      pullback.fst (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R)) =
    (Over.Hom.left η ≫ (pullbackSpecIso' R S T).inv) ≫
      pullback.fst (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R))

Tactic:
simp [Scheme.monObjAsOverPullback_one, ε_algSpec_left (R := CommRingCat.of _),
        pullbackSpecIso', specOverSpec_over, ← Spec.map_comp, ← CommRingCat.ofHom_comp,
        AlgHom.toUnder, Under.homMk_right, Bialgebra.TensorProduct.counitAlgHom_def,
        AlgHom.comp_toRingHom, RingHom.comp_assoc]

Goal state after:
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
⊢ ∃ 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:
let e₁ : R' ⊗[R] S ≃ₐ[R'] R' ⊗[R] ULift.{u} S :=
    Algebra.TensorProduct.congr .refl ULift.algEquiv.symm

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
⊢ ∃ 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
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : IsFinite f
inst✝ : LocallyOfFinitePresentation f
hY : ¬∃ R, Y = Spec R
R : CommRingCat
g : Spec R ⟶ Y
w✝ : IsOpenImmersion g
x : ↥(Spec R)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f],
    (∃ R, Y = Spec R) → ∀ (x : ↥Y), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, finrank f x' = finrank f x
U : Set ↥(Spec R)
hU : IsOpen U
hxU : x ∈ U
H : ∀ x' ∈ U, finrank (pullback.snd f g) x' = finrank (pullback.snd f g) x
y' : ↥(Spec R)
hyU : y' ∈ U
⊢ finrank (pullback.snd f g) y' = finrank (pullback.snd f g) x

Tactic:
exact H y' hyU

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d : B
l₁ : c ⟶ d
r₁ : d ⟶ c
adj₁ : l₁ ⊣ r₁
⊢ (conjugateEquiv adj₁ adj₁).symm (𝟙 r₁) = 𝟙 l₁

Tactic:
by
  rw [Equiv.symm_apply_eq, conjugateEquiv_id]

Goal state after:
Module: Mathlib.Data.FunLike.Graded

Goal state before:
pp: E : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
τ : Type u_5
ι : Type u_6
inst✝³ : SetLike σ A
inst✝² : SetLike τ B
𝒜 : ι → σ
ℬ : ι → τ
inst✝¹ : EquivLike E A B
inst✝ : GradedEquivLike E 𝒜 ℬ
e : E
i : ι
x✝ : ↥(𝒜 i)
⊢ (fun y ↦ ⟨EquivLike.inv e ↑y, ⋯⟩) (subtypeMap e i x✝) = x✝

Tactic:
by ext; exact EquivLike.inv_apply_apply e _

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

Goal state before:
pp: ι : 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
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
rid₁ : x ∉ I
rid₂ : y ∉ I
set₁ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}
set₁_eq : set₁ = {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}
set₂ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
set₂_eq : set₂ = {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
nonempty : ∀ x ∉ I, {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}.Nonempty
max₁ : ι := set₁.max' ⋯
max₂ : ι := set₂.max' ⋯
mem_max₁ : max₁ ∈ DFinsupp.support ((decompose 𝒜) x) ∧ (proj 𝒜 max₁) x ∉ I
mem_max₂ : max₂ ∈ DFinsupp.support ((decompose 𝒜) y) ∧ (proj 𝒜 max₂) y ∉ I
hxy : (proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
mem_I : (proj 𝒜 max₁) x * (proj 𝒜 max₂) y ∈ I
⊢ (proj 𝒜 max₁) x ∉ I ∧ (proj 𝒜 max₂) y ∉ I

Tactic:
exact ⟨mem_max₁.2, mem_max₂.2⟩

Goal state after:
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
α : Type u_4
inst✝² : SMul α A
inst✝¹ : IsScalarTower α A A
inst✝ : SMulMemClass σ α A
m : α
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
⊢ Localization.mk (m • ↑c1.num) ⟨↑c1.den, ⋯⟩ = Localization.mk (m • ↑c2.num) ⟨↑c2.den, ⋯⟩

Tactic:
convert! congr_arg (fun z : at x => m • z) h

Goal state after:
case e'_2
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
𝒜 : ι → σ
x : Submonoid A
α : Type u_4
inst✝² : SMul α A
inst✝¹ : IsScalarTower α A A
inst✝ : SMulMemClass σ α A
m : α
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
⊢ Localization.mk (m • ↑c1.num) ⟨↑c1.den, ⋯⟩ = m • Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩

case e'_3
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
𝒜 : ι → σ
x : Submonoid A
α : Type u_4
inst✝² : SMul α A
inst✝¹ : IsScalarTower α A A
inst✝ : SMulMemClass σ α A
m : α
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
⊢ Localization.mk (m • ↑c2.num) ⟨↑c2.den, ⋯⟩ = m • Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
n : ℕ
hn : f ^ n = ↑z.den
e : f ^ n = 0
this : Subsingleton (HomogeneousLocalization 𝒜 (Submonoid.powers f))
⊢ False

Tactic:
exact IsEmpty.elim (inferInstanceAs (IsEmpty (PrimeSpectrum (A⁰_ f)))) q

Goal state after:
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
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
d : ι
n : ℕ
hf : f ∈ 𝒜 d
a : A
ha : a ∈ 𝒜 (n • d)
⊢ val ((awayMap 𝒜 hg hx) (Away.mk 𝒜 hf n a ha)) = val (Away.mk 𝒜 ⋯ n (a * g ^ n) ⋯)

Tactic:
exact val_awayMap_mk ..

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

Goal state before:
pp: case surj
A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := ⋯
⊢ ∀ (z : Away 𝒜 x), ∃ x_1, z * (algebraMap (Away 𝒜 f) (Away 𝒜 x)) ↑x_1.2 = (algebraMap (Away 𝒜 f) (Away 𝒜 x)) x_1.1

pp: case exists_of_eq
A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := ⋯
⊢ ∀ {x_1 y : Away 𝒜 f},
    (algebraMap (Away 𝒜 f) (Away 𝒜 x)) x_1 = (algebraMap (Away 𝒜 f) (Away 𝒜 x)) y → ∃ c, ↑c * x_1 = ↑c * y

Tactic:
· intro z
    obtain ⟨n, s, hs, rfl⟩ := Away.mk_surjective 𝒜 (hx ▸ SetLike.mul_mem_graded hf hg) z
    rcases d with - | d
    · contradiction
    let t : Away 𝒜 f := Away.mk 𝒜 hf (n * (e + 1)) (s * g ^ (n * d)) <| by
      convert! SetLike.mul_mem_graded hs (SetLike.pow_mem_graded _ hg) using 2; simp; ring
    refine ⟨⟨t, ⟨_, ⟨n, rfl⟩⟩⟩, ?_⟩
    ext
    simp only [RingHom.algebraMap_toAlgebra, map_pow, awayMap_mk, val_mul, val_mk, val_pow,
      Localization.mk_pow, Localization.mk_mul, t]
    rw [Localization.mk_eq_mk_iff, Localization.r_iff_exists]
    exact ⟨1, by simp; ring⟩

Goal state after:
case exists_of_eq
A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := ⋯
⊢ ∀ {x_1 y : Away 𝒜 f},
    (algebraMap (Away 𝒜 f) (Away 𝒜 x)) x_1 = (algebraMap (Away 𝒜 f) (Away 𝒜 x)) y → ∃ c, ↑c * x_1 = ↑c * y
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case pos.refine_2.e_x
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubgroupClass σ A
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a : A
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
ai : ι' → ℕ
H : ∑ i, ai i • dv i = n
⊢ ∏ i, v i ^ ai i = ↑{ deg := n, num := ((decompose 𝒜) (∏ i, v i ^ ai i)) n, den := ⟨f ^ j, hb'⟩, den_mem := ⋯ }.num

Tactic:
refine (DirectSum.decompose_of_mem_same _ ?_).symm

Goal state after:
case pos.refine_2.e_x
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubgroupClass σ A
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a : A
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
ai : ι' → ℕ
H : ∑ i, ai i • dv i = n
⊢ ∏ i, v i ^ ai i ∈ 𝒜 n
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case h
R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec (CommRingCat.of ↑R)).Modules
f g : (↑R)ᵒᵖ
i : f ⟶ g
N : ModuleCat ↑(CommRingCat.of ↑R) := (modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)
x : ↑((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤))
⊢ (IsLocalizedModule.lift (Submonoid.powers (unop g))
        (ModuleCat.Hom.hom
          (tilde.toOpen ((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop g))))
        (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op)) ⋯)
      ((ModuleCat.Hom.hom
          (tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop g))))
        x) =
    (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map i.unop.hom.op))
      ((IsLocalizedModule.lift (Submonoid.powers (unop f))
          (ModuleCat.Hom.hom
            (tilde.toOpen ((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop f))))
          (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op)) ⋯)
        ((ModuleCat.Hom.hom
            (tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop f))))
          x))

Tactic:
simp only [IsLocalizedModule.lift_apply, ← ModuleCat.comp_apply, ← Functor.map_comp]

Goal state after:
case h
R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec (CommRingCat.of ↑R)).Modules
f g : (↑R)ᵒᵖ
i : f ⟶ g
N : ModuleCat ↑(CommRingCat.of ↑R) := (modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)
x : ↑((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤))
⊢ (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op)) x =
    (ConcreteCategory.hom ((modulesSpecToSheaf.obj M).obj.map ((homOfLE ⋯).op ≫ i.unop.hom.op))) x