mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
⊢ (∃ y, y • 1 = ↑v⁻¹ * ↑u) ↔ ∃ α, u = α • v

Tactic:
← star_eq_inv,

Goal state after:
R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
⊢ (∃ y, y • 1 = ↑(star v) * ↑u) ↔ ∃ α, u = α • v
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
x✝ : αˢʸᵐ
⊢ sym (⅟2 * (1 * unsym x✝ + unsym x✝ * 1)) = x✝

Tactic:
mul_one,

Goal state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
x✝ : αˢʸᵐ
⊢ sym (⅟2 * (1 * unsym x✝ + unsym x✝)) = x✝
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
x✝ : αˢʸᵐ
⊢ sym (⅟2 * (unsym x✝ * 1 + 1 * unsym x✝)) = x✝

Tactic:
mul_one,

Goal state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
x✝ : αˢʸᵐ
⊢ sym (⅟2 * (unsym x✝ + 1 * unsym x✝)) = x✝
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ sym
      (⅟2 * ⅟2 *
        (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
          unsym (a * a) * unsym b * unsym a)) =
    sym
      (⅟2 *
        (unsym a * (⅟2 * (unsym b * unsym (a * a) + unsym (a * a) * unsym b)) +
          ⅟2 * (unsym b * unsym (a * a) + unsym (a * a) * unsym b) * unsym a))

Tactic:
sym_inj,

Goal state after:
case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ⅟2 * ⅟2 *
      (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
        unsym (a * a) * unsym b * unsym a) =
    ⅟2 *
      (unsym a * (⅟2 * (unsym b * unsym (a * a) + unsym (a * a) * unsym b)) +
        ⅟2 * (unsym b * unsym (a * a) + unsym (a * a) * unsym b) * unsym a)
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
p : ↑↑(locallyRingedSpaceObj S).toPresheafedSpace
a : ↑((locallyRingedSpaceObj R).presheaf.stalk ((ConcreteCategory.hom (sheafedSpaceMap f).hom.base) p))
ha :
  IsUnit
    (↑(stalkIso (↑S) p)
      ((Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom f) ⋯)
        ((stalkIso (↑R) (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)).symm a)))
this : IsLocalHom (stalkIso (↑S) p)
⊢ IsUnit a

Tactic:
have : IsLocalHom (stalkIso R (p.comap f.hom)).symm := isLocalHom_equiv _

Goal state after:
R S : CommRingCat
f : R ⟶ S
p : ↑↑(locallyRingedSpaceObj S).toPresheafedSpace
a : ↑((locallyRingedSpaceObj R).presheaf.stalk ((ConcreteCategory.hom (sheafedSpaceMap f).hom.base) p))
ha :
  IsUnit
    (↑(stalkIso (↑S) p)
      ((Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom f) ⋯)
        ((stalkIso (↑R) (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)).symm a)))
this✝ : IsLocalHom (stalkIso (↑S) p)
this : IsLocalHom (stalkIso (↑R) (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)).symm
⊢ IsUnit a
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
inst✝ : IsIso f
⊢ map (inv f) = inv (map f)

Tactic:
change Scheme.Spec.map (inv f).op = inv (Scheme.Spec.map f.op)
  rw [op_inv, ← Scheme.Spec.map_inv]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: case refine_2
X : Type u
ι : Type u_1
Y : ι → Type u
f : (i : ι) → Y i ⟶ X
h : ∀ (x : (fun X ↦ X) X), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (f i))
x : X
⊢ ∃ Y_1 g, Presieve.ofArrows Y f g ∧ x ∈ Set.range ⇑(ConcreteCategory.hom g)

Tactic:
obtain ⟨i, hx⟩ := h x

Goal state after:
case refine_2
X : Type u
ι : Type u_1
Y : ι → Type u
f : (i : ι) → Y i ⟶ X
h : ∀ (x : (fun X ↦ X) X), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (f i))
x : X
i : ι
hx : x ∈ Set.range ⇑(ConcreteCategory.hom (f i))
⊢ ∃ Y_1 g, Presieve.ofArrows Y f g ∧ x ∈ Set.range ⇑(ConcreteCategory.hom g)
Module: Mathlib.CategoryTheory.Sites.MorphismProperty

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P✝ Q P : MorphismProperty C
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasPullbacks
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ P.precoverage.coverings X
this : S.HasPullbacks f
⊢ ∃ T ∈ P.precoverage.coverings Y, T.FactorsThruAlong S f

Tactic:
refine ⟨S.pullbackArrows f, ?_, .pullbackArrows f S⟩

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
P✝ Q P : MorphismProperty C
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasPullbacks
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ P.precoverage.coverings X
this : S.HasPullbacks f
⊢ Presieve.pullbackArrows f S ∈ P.precoverage.coverings Y
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range ⇑(pullback.snd f g) = ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f)

Tactic:
← show _ = (pullback.snd f g).base from
    PreservesPullback.iso_hom_snd Scheme.forgetToTop f g,

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range
      ⇑(ConcreteCategory.hom
          ((PreservesPullback.iso Scheme.forgetToTop f g).hom ≫
            pullback.snd (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g))) =
    ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: case neg.mpr
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↥X
hx : x ∉ Set.range ⇑iU
y : ↥V
hy : y ∈ ↑W
e : iV y = f x
⊢ x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W)

Tactic:
obtain ⟨x, rfl⟩ := (IsOpenImmersion.range_pullbackSnd iV f).ge ⟨y, e⟩

Goal state after:
case neg.mpr
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
y : ↥V
hy : y ∈ ↑W
x : ↥(pullback iV f)
hx : (pullback.snd iV f) x ∉ Set.range ⇑iU
e : iV y = f ((pullback.snd iV f) x)
⊢ (pullback.snd iV f) x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W)
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X✝ Y Z : Scheme
𝒰 : X✝.OpenCover
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
X : Scheme
U : (x : ↑X.toTopCat) → OpenNhds x
R : ↑X.toTopCat → CommRingCat
h : ∀ (x : ↑X.toTopCat), Nonempty (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)))
e : (x : ↑X.toTopCat) → X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)) := fun x ↦ ⋯.some
⊢ (∀ (x : ↥X),
      ∃ i,
        x ∈
          Set.range
            ⇑({ I₀ := ↥X, X := fun x ↦ Spec (R x), f := fun x ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ } }.f i)) ∧
    ∀ (i : { I₀ := ↥X, X := fun x ↦ Spec (R x), f := fun x ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ } }.I₀),
      IsOpenImmersion
        ({ I₀ := ↥X, X := fun x ↦ Spec (R x), f := fun x ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ } }.f i)

Tactic:
refine ⟨fun x ↦ ⟨x, ⟨(e x).hom.base ⟨x, (U x).2⟩, ?_⟩⟩, inferInstance⟩

Goal state after:
X✝ Y Z : Scheme
𝒰 : X✝.OpenCover
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
X : Scheme
U : (x : ↑X.toTopCat) → OpenNhds x
R : ↑X.toTopCat → CommRingCat
h : ∀ (x : ↑X.toTopCat), Nonempty (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)))
e : (x : ↑X.toTopCat) → X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)) := fun x ↦ ⋯.some
x : ↥X
⊢ ({ I₀ := ↥X, X := fun x ↦ Spec (R x), f := fun x ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ } }.f x)
      ((ConcreteCategory.hom (e x).hom.base) ⟨x, ⋯⟩) =
    x
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsLimit (forgetToSheafedSpace.mapCone (pullbackConeOfLeft f g))

Tactic:
apply (isLimitMapConePullbackConeEquiv _ _).symm.toFun
    apply isLimitOfIsLimitPullbackConeMap SheafedSpace.forgetToPresheafedSpace
    exact PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftIsLimit f.1 g.1

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: case h_nhds.refine_1
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
s : ↑((fun x ↦ Classical.choose ⋯) (Cover.idx X.affineCover a))
hxV : x ∈ ↑(PrimeSpectrum.basicOpen s)
hVU : ↑(PrimeSpectrum.basicOpen s) ⊆ U'
⊢ a ∈ ⇑(X.affineCover.f (Cover.idx X.affineCover a)) '' (PrimeSpectrum.basicOpen s).carrier

pp: case h_nhds.refine_2
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
s : ↑((fun x ↦ Classical.choose ⋯) (Cover.idx X.affineCover a))
hxV : x ∈ ↑(PrimeSpectrum.basicOpen s)
hVU : ↑(PrimeSpectrum.basicOpen s) ⊆ U'
⊢ ⇑(X.affineCover.f (Cover.idx X.affineCover a)) '' (PrimeSpectrum.basicOpen s).carrier ⊆ U

Tactic:
· exact ⟨x, hxV, e⟩

Goal state after:
case h_nhds.refine_2
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
s : ↑((fun x ↦ Classical.choose ⋯) (Cover.idx X.affineCover a))
hxV : x ∈ ↑(PrimeSpectrum.basicOpen s)
hVU : ↑(PrimeSpectrum.basicOpen s) ⊆ U'
⊢ ⇑(X.affineCover.f (Cover.idx X.affineCover a)) '' (PrimeSpectrum.basicOpen s).carrier ⊆ U
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: case h_nhds.refine_2
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
s : ↑((fun x ↦ Classical.choose ⋯) (Cover.idx X.affineCover a))
hxV : x ∈ ↑(PrimeSpectrum.basicOpen s)
hVU : ↑(PrimeSpectrum.basicOpen s) ⊆ U'
⊢ ⇑(X.affineCover.f (Cover.idx X.affineCover a)) '' (PrimeSpectrum.basicOpen s).carrier ⊆ U

Tactic:
Set.image_subset_iff

Goal state after:
case h_nhds.refine_2
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
s : ↑((fun x ↦ Classical.choose ⋯) (Cover.idx X.affineCover a))
hxV : x ∈ ↑(PrimeSpectrum.basicOpen s)
hVU : ↑(PrimeSpectrum.basicOpen s) ⊆ U'
⊢ (PrimeSpectrum.basicOpen s).carrier ⊆ ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
e₁ : Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U).presheaf.map (eqToHom ⋯).op
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op

Tactic:
have : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W := W.map_functor_eq (U := V)

Goal state after:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
e₁ : Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U).presheaf.map (eqToHom ⋯).op
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
s t : LocalizedModule.Away f M
h_eq : (toBasicOpenₗ R M f) s = (toBasicOpenₗ R M f) t
⊢ s = t

Tactic:
induction s using LocalizedModule.induction_on with | h a b =>
  induction t using LocalizedModule.induction_on with | h c d =>
  suffices f ∈ ((⊥ : Submodule R M).colon {d • a - b • c}).radical by
    rw [LocalizedModule.mk_eq]
    obtain ⟨n, hn⟩ := this
    exact ⟨⟨f ^ n, n, rfl⟩, by simpa [sub_eq_zero, smul_sub] using! Submodule.mem_colon.mp hn _ rfl⟩
  simp only [toBasicOpenₗ_mk] at h_eq
  rw [← PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical, PrimeSpectrum.mem_vanishingIdeal]
  intro p hfp
  contrapose hfp
  obtain ⟨u, hu⟩ := LocalizedModule.mk_eq.mp congr(($h_eq).1 ⟨p, hfp⟩)
  rw [PrimeSpectrum.mem_zeroLocus, Set.not_subset]
  exact ⟨u.1, by simpa [sub_eq_zero, smul_sub], u.2⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
i j : ↥U
this : const (f i) (g i) (basicOpen (g i)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
⊢ const (g i • f j) (g i * g j) (basicOpen (g i * g j)) ⋯ =
    (ConcreteCategory.hom ((structureSheafInType R M).obj.map (homOfLE ?m.192).op)) s

Tactic:
refine .trans (Subtype.ext <| funext fun a ↦ ?_) congr((structureSheafInType R M).obj.map
        (homOfLE ((PrimeSpectrum.basicOpen_mul (g i) (g j)).trans_le inf_le_right)).op $(H j))
      exact LocalizedModule.mk_eq.mpr ⟨1, by simp [Submonoid.smul_def, ← smul_assoc]; ring_nf⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
s : (structureSheafInType R M).obj.obj (op (basicOpen f))
ι : Type u
w✝ : Fintype ι
a : ι → M
b : ι → R
ibU : ∀ (i : ι), basicOpen (b i) ≤ basicOpen f
iU : basicOpen f ≤ ⨆ i, basicOpen (b i)
hab : ∀ (i j : ι), b j • a i = b i • a j
H :
  ∀ (i : ι),
    (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s = const (a i) (b i) (basicOpen (b i)) ⋯
this : PrimeSpectrum.zeroLocus (Set.range b) ⊆ PrimeSpectrum.zeroLocus {f}
x : PrimeSpectrum R
hx : x ∈ PrimeSpectrum.zeroLocus (Set.range b)
⊢ f ∈ x.asIdeal

Tactic:
by simpa using this hx

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
inst✝ : IsAffine X
f : X ⟶ Y
H : IsOpenImmersion f
⊢ IsAffineOpen (Scheme.Hom.opensRange f)

Tactic:
by
  refine .of_isIso (IsOpenImmersion.isoOfRangeEq f (Y.ofRestrict _) ?_).inv
  exact Subtype.range_val.symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
⊢ IsTopologicalBasis (Set.range fun i ↦ ↑↑i)

Tactic:
rw [← Set.image_eq_range]

Goal state after:
X : Scheme
⊢ IsTopologicalBasis (SetLike.coe '' X.affineOpens)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
⊢ (s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))) → coequalizer f g ⟶ s.pt

Tactic:
refine fun s ↦ coequalizer.desc s.inl ?_

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
⊢ f ≫ s.inl = g ≫ s.inl
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
f : M
s : ↥x.asIdeal.primeCompl
⊢ (ModuleCat.Hom.hom (toStalkₗ' R M x)) f =
    (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ (basicOpen ↑s) x ⋯))
      (↑s • const f (↑s) (basicOpen ↑s) ⋯)

Tactic:
← toOpenₗ_germ (basicOpen ↑s) _ s.2,

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
f : M
s : ↥x.asIdeal.primeCompl
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (toOpenₗ R M (basicOpen ↑s)) ≫ (structurePresheafInModuleCat R M).germ (basicOpen ↑s) x ⋯))
      f =
    (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ (basicOpen ↑s) x ⋯))
      (↑s • const f (↑s) (basicOpen ↑s) ⋯)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
this : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
⊢ Scheme.Hom.app f (Y.basicOpen r) =
    CommRingCat.ofHom
        (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r))
          (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)))
          (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
      X.presheaf.map (eqToHom ⋯).op

Tactic:
have := h.isLocalization_basicOpen (f.app U r)

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r))
⊢ Scheme.Hom.app f (Y.basicOpen r) =
    CommRingCat.ofHom
        (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r))
          (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)))
          (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
      X.presheaf.map (eqToHom ⋯).op
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: case H
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ (Opens.map f.base).obj
      (Y.toRingedSpace.basicOpen
        (have this := (ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U))) s;
        this)) =
    (Opens.map g.base).obj
      (Y.toRingedSpace.basicOpen
        (have this := (ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U))) s;
        this))

Tactic:
preimage_basicOpen f,

Goal state after:
case H
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ X.toRingedSpace.basicOpen
      ((ConcreteCategory.hom
          (f.c.app
            (op (unop (op ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).1 (unop (op U))))))))
        (have this := (ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U))) s;
        this)) =
    (Opens.map g.base).obj
      (Y.toRingedSpace.basicOpen
        (have this := (ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U))) s;
        this))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
A : CommRingCat
f : X ⟶ Spec A
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop (specTargetImageFactorization f)))

Tactic:
let φ : A ⟶ Γ(X, ⊤) := (((ΓSpec.adjunction).homEquiv X (op A)).symm f).unop
  let φ' : specTargetImage f ⟶ Scheme.Γ.obj (op X) := CommRingCat.ofHom (RingHom.kerLift φ.hom)
  change Function.Injective <| ((ΓSpec.adjunction.homEquiv X _) φ'.op).appTop
  rw [ΓSpec_adjunction_homEquiv_eq]
  apply (RingHom.kerLift_injective φ.hom).comp
  exact ((ConcreteCategory.isIso_iff_bijective (Scheme.ΓSpecIso _).hom).mp inferInstance).injective

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case refine_1
h : MkCore
i j : h.J
x : ↥(h.V j i)
⊢ ↑x ∈ h.V j j

Tactic:
rw [h.V_id]

Goal state after:
case refine_1
h : MkCore
i j : h.J
x : ↥(h.V j i)
⊢ ↑x ∈ ⊤
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case convert_1.left
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan fun j ↦ WalkingPair.casesOn j X Y := Cofan.mk S fun j ↦ WalkingPair.casesOn j f g
i : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl (BinaryCofan.mk f g).pt) ⋯
fi : (j : WalkingPair) → WalkingPair.casesOn j X Y ⟶ S := fun j ↦ WalkingPair.casesOn j f g
⊢ IsOpenImmersion (fi WalkingPair.left)

Tactic:
(simp [fi]; infer_instance)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case convert_1.right
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan fun j ↦ WalkingPair.casesOn j X Y := Cofan.mk S fun j ↦ WalkingPair.casesOn j f g
i : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl (BinaryCofan.mk f g).pt) ⋯
fi : (j : WalkingPair) → WalkingPair.casesOn j X Y ⟶ S := fun j ↦ WalkingPair.casesOn j f g
⊢ IsOpenImmersion (fi WalkingPair.right)

Tactic:
(simp [fi]; infer_instance)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ (pullbackP1Iso 𝒰 f g i).hom ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i = pullback.fst (p1 𝒰 f g) (𝒰.f i)

Tactic:
by
  rw [← gluing_ι, ← pullbackP1Iso_inv_fst, Iso.hom_inv_id_assoc]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        D.ιInvApp U ≫
          D.diagramOverOpenπ U j ≫
            (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map
                (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))) ≫
              𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j)))) =
    D.diagramOverOpenπ U j ≫
      (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map
          (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))) ≫
        𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j))))

Tactic:
rw [limit.w_assoc]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        D.ιInvApp U ≫
          limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j))) ≫
            𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j)))) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j))) ≫
      𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j))))