mathlib-initiative/mathlib-tactics huggingface dataset:
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 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : ↥(unop U)) → at ↑x
ha : (isLocallyFraction 𝒜).pred a
hb : (isLocallyFraction 𝒜).pred b
x : ↥(unop U)
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal 𝒜).pred fun x ↦ (a * b) (i x)

Tactic:
rcases ha x with ⟨Va, ma, ia, ja, ⟨ra, ra_mem⟩, ⟨sa, sa_mem⟩, hwa, wa⟩

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : ↥(unop U)) → at ↑x
ha : (isLocallyFraction 𝒜).pred a
hb : (isLocallyFraction 𝒜).pred b
x : ↥(unop U)
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ unop U
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
hwa : ∀ (x : ↥Va), ↑⟨sa, sa_mem⟩ ∉ (↑x).asHomogeneousIdeal
wa :
  ∀ (x : ↥Va),
    (fun x ↦ a (ia x)) x =
      HomogeneousLocalization.mk { deg := ja, num := ⟨ra, ra_mem⟩, den := ⟨sa, sa_mem⟩, den_mem := ⋯ }
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal 𝒜).pred fun x ↦ (a * b) (i x)
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 : ↑(ProjectiveSpectrum.top 𝒜)
U : Opens ↑(ProjectiveSpectrum.top 𝒜)
hxU : x ∈ U
s : ToType ((Proj.structureSheaf 𝒜).presheaf.obj (op U))
V : Opens ↑(ProjectiveSpectrum.top 𝒜)
hxV : ↑⟨x, hxU⟩ ∈ V
i : V ⟶ unop (op U)
n : ℕ
a b : ↥(𝒜 n)
h : ∀ (x : ↥V), ↑b ∉ (↑x).asHomogeneousIdeal
e :
  ∀ (a_1 : ↑(ProjectiveSpectrum.top 𝒜)) (b_1 : a_1 ∈ V),
    ↑s ⟨a_1, ⋯⟩ = HomogeneousLocalization.mk { deg := n, num := a, den := b, den_mem := ⋯ }
⊢ Quotient.liftOn' (HomogeneousLocalization.mk { deg := n, num := a, den := b, den_mem := ⋯ })
      (fun f ↦
        (ConcreteCategory.hom ((Proj.structureSheaf 𝒜).presheaf.germ (ProjectiveSpectrum.basicOpen 𝒜 ↑f.den) x ⋯))
          (sectionInBasicOpen 𝒜 x f))
      ⋯ =
    (ConcreteCategory.hom ((Proj.structureSheaf 𝒜).presheaf.germ U x hxU)) s

Tactic:
Quotient.liftOn'_mk''

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
U : Opens ↑(ProjectiveSpectrum.top 𝒜)
hxU : x ∈ U
s : ToType ((Proj.structureSheaf 𝒜).presheaf.obj (op U))
V : Opens ↑(ProjectiveSpectrum.top 𝒜)
hxV : ↑⟨x, hxU⟩ ∈ V
i : V ⟶ unop (op U)
n : ℕ
a b : ↥(𝒜 n)
h : ∀ (x : ↥V), ↑b ∉ (↑x).asHomogeneousIdeal
e :
  ∀ (a_1 : ↑(ProjectiveSpectrum.top 𝒜)) (b_1 : a_1 ∈ V),
    ↑s ⟨a_1, ⋯⟩ = HomogeneousLocalization.mk { deg := n, num := a, den := b, den_mem := ⋯ }
⊢ (ConcreteCategory.hom
        ((Proj.structureSheaf 𝒜).presheaf.germ
          (ProjectiveSpectrum.basicOpen 𝒜 ↑{ deg := n, num := a, den := b, den_mem := ⋯ }.den) x ⋯))
      (sectionInBasicOpen 𝒜 x { deg := n, num := a, den := b, den_mem := ⋯ }) =
    (ConcreteCategory.hom ((Proj.structureSheaf 𝒜).presheaf.germ U x hxU)) s
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
e₁ : pullback f ⋙ pullback (𝟙 X) ≅ pullback (𝟙 X ≫ f) := pullbackComp (𝟙 X) f
e₂ : pullback f ⋙ pullback (𝟙 X) ≅ pullback f ⋙ 𝟭 X.Modules := (pullback f).isoWhiskerLeft (pullbackId X)
e₃ : pullback f ⋙ 𝟭 X.Modules ≅ pullback f := (pullback f).rightUnitor
⊢ e₁.inv ≫ e₂.hom ≫ e₃.hom = eqToHom ⋯

Tactic:
have : e₁.hom = e₂.hom ≫ e₃.hom :=
    congr_arg Iso.hom (SheafOfModules.pullback_comp_id.{u} f.toRingCatSheafHom)

Goal state after:
X Y : Scheme
f : X ⟶ Y
e₁ : pullback f ⋙ pullback (𝟙 X) ≅ pullback (𝟙 X ≫ f) := pullbackComp (𝟙 X) f
e₂ : pullback f ⋙ pullback (𝟙 X) ≅ pullback f ⋙ 𝟭 X.Modules := (pullback f).isoWhiskerLeft (pullbackId X)
e₃ : pullback f ⋙ 𝟭 X.Modules ≅ pullback f := (pullback f).rightUnitor
this : e₁.hom = e₂.hom ≫ e₃.hom
⊢ e₁.inv ≫ e₂.hom ≫ e₃.hom = eqToHom ⋯
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 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
N : ι
s : A
hs : s ∈ 𝒜 N
n : ℕ
hn : (fun x ↦ f ^ x) n ∈ 𝒜 N
⊢ ∃ n_1 a,
    ∃ (ha : a ∈ 𝒜 (n_1 • d)),
      Away.mk 𝒜 hf n_1 a ha = mk { deg := N, num := ⟨s, hs⟩, den := ⟨(fun x ↦ f ^ x) n, hn⟩, den_mem := ⋯ }

Tactic:
by_cases hfn : f ^ n = 0

Goal state after:
case pos
ι : 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
N : ι
s : A
hs : s ∈ 𝒜 N
n : ℕ
hn : (fun x ↦ f ^ x) n ∈ 𝒜 N
hfn : f ^ n = 0
⊢ ∃ n_1 a,
    ∃ (ha : a ∈ 𝒜 (n_1 • d)),
      Away.mk 𝒜 hf n_1 a ha = mk { deg := N, num := ⟨s, hs⟩, den := ⟨(fun x ↦ f ^ x) n, hn⟩, den_mem := ⋯ }

case neg
ι : 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
N : ι
s : A
hs : s ∈ 𝒜 N
n : ℕ
hn : (fun x ↦ f ^ x) n ∈ 𝒜 N
hfn : ¬f ^ n = 0
⊢ ∃ n_1 a,
    ∃ (ha : a ∈ 𝒜 (n_1 • d)),
      Away.mk 𝒜 hf n_1 a ha = mk { deg := N, num := ⟨s, hs⟩, den := ⟨(fun x ↦ f ^ x) n, hn⟩, den_mem := ⋯ }
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f g✝ : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
⊢ (basicOpen 𝒜 f ⊓ basicOpen 𝒜 g).carrier = (basicOpen 𝒜 x).carrier

Tactic:
← basicOpen_mul,

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f g✝ : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
⊢ (basicOpen 𝒜 (f * g)).carrier = (basicOpen 𝒜 x).carrier
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
x x' : ↑Γ(X, ⊤)
t t' : A
d d' : ℕ
H : f t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
⊢ ↑(X.basicOpen x) ⟶ ↑(basicOpen 𝒜 t)

Tactic:
refine ?_ ≫ (basicOpenIsoSpec _ _ hd h0d).inv

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
x x' : ↑Γ(X, ⊤)
t t' : A
d d' : ℕ
H : f t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
⊢ ↑(X.basicOpen x) ⟶ Spec (CommRingCat.of (Away 𝒜 t))
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec (CommRingCat.of ↑R)).Modules
f : (↑R)ᵒᵖ
⊢ Submonoid.powers (unop f) ≤
    Submonoid.comap
      (algebraMap (↑R)
        (Module.End ↑R
          ↑((modulesSpecToSheaf.obj M).obj.obj (op ((inducedFunctor PrimeSpectrum.basicOpen).obj (unop f))))))
      (IsUnit.submonoid
        (Module.End ↑R
          ↑((modulesSpecToSheaf.obj M).obj.obj (op ((inducedFunctor PrimeSpectrum.basicOpen).obj (unop f))))))

Tactic:
simp only [inducedFunctor_obj, Submonoid.powers_le, Submonoid.mem_comap]

Goal state after:
R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec (CommRingCat.of ↑R)).Modules
f : (↑R)ᵒᵖ
⊢ (algebraMap (↑R) (Module.End ↑R ↑((modulesSpecToSheaf.obj M).obj.obj (op (PrimeSpectrum.basicOpen (unop f))))))
      (unop f) ∈
    IsUnit.submonoid (Module.End ↑R ↑((modulesSpecToSheaf.obj M).obj.obj (op (PrimeSpectrum.basicOpen (unop f)))))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor

Goal state before:
pp: A σ : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
⊢ map (GradedRingHom.id 𝒜) ⋯ = 𝟙 (Proj 𝒜)

Tactic:
by
  refine (affineOpenCover _).openCover.hom_ext _ _ fun s ↦ ?_
  convert! awayι_comp_map (.id 𝒜) _ _ _ s.2.2 using 1
  simp

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

Goal state before:
pp: R : CommRingCat
M N : TopCat.Sheaf (ModuleCat ↑R) ↑(Spec R).toPresheafedSpace
φ : M ⟶ N
h : IsIso (φ.hom.app (op ⊤))
hM : IsLocalizing M
hN : IsLocalizing N
⊢ IsIso φ

Tactic:
refine TopCat.Sheaf.isIso_iff_isIso_basis (φ := φ) isBasis_basic_opens (fun f => ?_)
  refine ModuleCat.isIso_of_isLocalizedModule_comp (hM f) ?_
  rw [φ.hom.naturality]
  exact IsLocalizedModule.of_linearEquiv_right _ _ (asIso (φ.hom.app (op ⊤))).toLinearEquiv

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case refine_2
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
x : A
hx : x ∈ carrier f_deg q
⊢ ∀ {i : ℕ} (m_1 : ↥(𝒜 i)), ↑m_1 • x ∈ carrier f_deg q

pp: case refine_3
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
x : A
hx : x ∈ carrier f_deg q
⊢ ∀ (m_1 m' : A), m_1 • x ∈ carrier f_deg q → m' • x ∈ carrier f_deg q → (m_1 + m') • x ∈ carrier f_deg q

Tactic:
· rintro n ⟨a, ha⟩ i
    simp_rw [proj_apply, smul_eq_mul, coe_decompose_mul_of_left_mem 𝒜 i ha]
    let product : A⁰_ f :=
      (HomogeneousLocalization.mk
          ⟨_, ⟨a ^ m, pow_mem_graded m ha⟩, ⟨_, ?_⟩, ⟨n, rfl⟩⟩ : A⁰_ f) *
        (HomogeneousLocalization.mk
          ⟨_, ⟨proj 𝒜 (i - n) x ^ m, by mem_tac⟩, ⟨_, ?_⟩, ⟨i - n, rfl⟩⟩ : A⁰_ f)
    · split_ifs with h
      · convert_to product ∈ q.1
        · dsimp [product]
          rw [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk,
            HomogeneousLocalization.val_mul, HomogeneousLocalization.val_mk,
            HomogeneousLocalization.val_mk]
          · simp_rw [mul_pow]; rw [Localization.mk_mul]
            · congr; rw [← pow_add, Nat.add_sub_of_le h]
        · apply Ideal.mul_mem_left (α := A⁰_ f) _ _ (hx _)
          rw [(_ : m • n = _)]
          · mem_tac
          · simp only [smul_eq_mul, mul_comm]
      · simpa only [map_zero, zero_pow hm.ne'] using zero_mem f_deg hm q i
    rw [(_ : m • (i - n) = _)]
    · mem_tac
    · simp only [smul_eq_mul, mul_comm]

Goal state after:
case refine_3
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
x : A
hx : x ∈ carrier f_deg q
⊢ ∀ (m_1 m' : A), m_1 • x ∈ carrier f_deg q → m' • x ∈ carrier f_deg q → (m_1 + m') • x ∈ carrier f_deg q
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
g : ↑R
hg : basicOpen g ≤ V
hV : Aux M V
f : ↑R
hfg : basicOpen f ≤ basicOpen g
t : ↑Γ(M, basicOpen g)
ht : (ConcreteCategory.hom (M.presheaf.map (homOfLE hfg).op)) t = 0
n : ℕ
t' : ↑Γ(M, V)
ht' : (ConcreteCategory.hom (M.presheaf.map (homOfLE hg).op)) t' = g ^ n • t
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) t' = 0

Tactic:
rw [← homOfLE_comp hfg hg, op_comp, M.presheaf.map_comp_apply, ht', M.map_smul_Spec, ht]

Goal state after:
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
g : ↑R
hg : basicOpen g ≤ V
hV : Aux M V
f : ↑R
hfg : basicOpen f ≤ basicOpen g
t : ↑Γ(M, basicOpen g)
ht : (ConcreteCategory.hom (M.presheaf.map (homOfLE hfg).op)) t = 0
n : ℕ
t' : ↑Γ(M, V)
ht' : (ConcreteCategory.hom (M.presheaf.map (homOfLE hg).op)) t' = g ^ n • t
⊢ g ^ n • 0 = 0
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
g : ↑R
hg : basicOpen g ≤ V
hV : Aux M V
f : ↑R
hfg : basicOpen f ≤ basicOpen g
t : ↑Γ(M, basicOpen g)
ht : (ConcreteCategory.hom (M.presheaf.map (homOfLE hfg).op)) t = 0
n : ℕ
t' : ↑Γ(M, V)
ht' : (ConcreteCategory.hom (M.presheaf.map (homOfLE hg).op)) t' = g ^ n • t
⊢ ∃ n, f ^ n • t = 0

Tactic:
obtain ⟨m, hm⟩ := hV.uniqueness _ (le_trans hfg hg) t' <| by
      rw [← homOfLE_comp hfg hg, op_comp, M.presheaf.map_comp_apply, ht', M.map_smul_Spec, ht]
      simp

Goal state after:
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
g : ↑R
hg : basicOpen g ≤ V
hV : Aux M V
f : ↑R
hfg : basicOpen f ≤ basicOpen g
t : ↑Γ(M, basicOpen g)
ht : (ConcreteCategory.hom (M.presheaf.map (homOfLE hfg).op)) t = 0
n : ℕ
t' : ↑Γ(M, V)
ht' : (ConcreteCategory.hom (M.presheaf.map (homOfLE hg).op)) t' = g ^ n • t
m : ℕ
hm : f ^ m • t' = 0
⊢ ∃ n, f ^ n • t = 0
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
g : ↑R
a : R ⟶ CommRingCat.of (Localization.Away g) := CommRingCat.ofHom (algebraMap (↑R) (Localization.Away g))
ψ : Spec (CommRingCat.of (Localization.Away g)) ⟶ Spec (CommRingCat.of ↑R) := Spec.map a
M' : (Spec (CommRingCat.of (Localization.Away g))).Modules := M.restrict ψ
h : Aux M' ⊤
f : ↑R
hf : basicOpen f ≤ basicOpen g
⊢ basicOpen f = ψ ''ᵁ basicOpen ((ConcreteCategory.hom a) f)

Tactic:
rw [← SpecMap_preimage_basicOpen, Scheme.Hom.image_preimage_eq_opensRange_inf]

Goal state after:
R : CommRingCat
M : (Spec R).Modules
g : ↑R
a : R ⟶ CommRingCat.of (Localization.Away g) := CommRingCat.ofHom (algebraMap (↑R) (Localization.Away g))
ψ : Spec (CommRingCat.of (Localization.Away g)) ⟶ Spec (CommRingCat.of ↑R) := Spec.map a
M' : (Spec (CommRingCat.of (Localization.Away g))).Modules := M.restrict ψ
h : Aux M' ⊤
f : ↑R
hf : basicOpen f ≤ basicOpen g
⊢ basicOpen f = Scheme.Hom.opensRange ψ ⊓ basicOpen f
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case h
R : CommRingCat
M : (Spec R).Modules
g : ↑R
a : R ⟶ CommRingCat.of (Localization.Away g) := ⋯
ψ : Spec (CommRingCat.of (Localization.Away g)) ⟶ Spec (CommRingCat.of ↑R) := ⋯
M' : (Spec (CommRingCat.of (Localization.Away g))).Modules := ⋯
h : Aux M' ⊤
heq : ∀ (f : ↑R), basicOpen f ≤ basicOpen g → basicOpen f = ψ ''ᵁ basicOpen ((ConcreteCategory.hom a) f)
iso : Γ(M.restrict ψ, ⊤) ≅ Γ(M, basicOpen g) := ⋯
e : (f : ↑R) → basicOpen f ≤ basicOpen g → (Γ(M', basicOpen ((ConcreteCategory.hom a) f)) ≅ Γ(M, basicOpen f)) := ⋯
f : ↑R
hf : basicOpen f ≤ basicOpen g
s : ↑Γ(M, basicOpen f)
n : ℕ
t : ↑Γ(M', ⊤)
ht :
  (ConcreteCategory.hom (M'.presheaf.map (homOfLE ⋯).op)) t =
    (ConcreteCategory.hom a) f ^ n • (ConcreteCategory.hom (e f hf).inv) s
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) ((ConcreteCategory.hom iso.hom) t) = f ^ n • s

Tactic:
have := congr((e _ hf).hom $ht)

Goal state after:
case h
R : CommRingCat
M : (Spec R).Modules
g : ↑R
a : R ⟶ CommRingCat.of (Localization.Away g) := CommRingCat.ofHom (algebraMap (↑R) (Localization.Away g))
ψ : Spec (CommRingCat.of (Localization.Away g)) ⟶ Spec (CommRingCat.of ↑R) := Spec.map a
M' : (Spec (CommRingCat.of (Localization.Away g))).Modules := M.restrict ψ
h : Aux M' ⊤
heq : ∀ (f : ↑R), basicOpen f ≤ basicOpen g → basicOpen f = ψ ''ᵁ basicOpen ((ConcreteCategory.hom a) f)
iso : Γ(M.restrict ψ, ⊤) ≅ Γ(M, basicOpen g) :=
  Scheme.Modules.restrictAppIso ψ M ⊤ ≪≫ Functor.mapIso M.presheaf (eqToIso ⋯).op
e : (f : ↑R) → basicOpen f ≤ basicOpen g → (Γ(M', basicOpen ((ConcreteCategory.hom a) f)) ≅ Γ(M, basicOpen f)) :=
  fun f hf ↦
    Scheme.Modules.restrictAppIso ψ M (basicOpen ((ConcreteCategory.hom a) f)) ≪≫
      Functor.mapIso M.presheaf (eqToIso ⋯).op
f : ↑R
hf : basicOpen f ≤ basicOpen g
s : ↑Γ(M, basicOpen f)
n : ℕ
t : ↑Γ(M', ⊤)
ht :
  (ConcreteCategory.hom (M'.presheaf.map (homOfLE ⋯).op)) t =
    (ConcreteCategory.hom a) f ^ n • (ConcreteCategory.hom (e f hf).inv) s
this :
  (ConcreteCategory.hom (e f hf).hom) ((ConcreteCategory.hom (M'.presheaf.map (homOfLE ⋯).op)) t) =
    (ConcreteCategory.hom (e f hf).hom) ((ConcreteCategory.hom a) f ^ n • (ConcreteCategory.hom (e f hf).inv) s)
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) ((ConcreteCategory.hom iso.hom) t) = f ^ n • s
Module: Mathlib.CategoryTheory.Sites.Point.Basic

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝⁵ : Category.{v', u'} A
inst✝⁴ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst✝³ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory A FC
P : Cᵒᵖ ⥤ A
inst✝¹ : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝ : LocallySmall.{w, v, u} C
p₁ p₂ : ToType (Φ.presheafFiber.obj P)
⊢ ∃ X x z₁ z₂,
    (ConcreteCategory.hom (Φ.toPresheafFiber X x P)) z₁ = p₁ ∧ (ConcreteCategory.hom (Φ.toPresheafFiber X x P)) z₂ = p₂

Tactic:
by
  obtain ⟨⟨X, x⟩, z₁, z₂, rfl, rfl⟩ := Types.FilteredColimit.jointly_surjective_of_isColimit₂
    (isColimitOfPreserves (forget A)
      (colimit.isColimit ((CategoryOfElements.π Φ.fiber).op ⋙ P))) p₁ p₂
  exact ⟨X, x, z₁, z₂, rfl, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
inst✝¹ : LocallySmall.{w, v, u} C
U T : C
f : U ⟶ T
inst✝ : Mono f
⊢ Function.Injective ⇑(ConcreteCategory.hom (Φ.fiber.map f))

Tactic:
by
  rw [← mono_iff_injective]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝³ : Category.{v₀, u₀} C₀
inst✝² : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : (data a.Y).I₀
X₀ : C₀
b : X₀ ⟶ (data a.Y).X i
Y : C
j : (data X).I₀
c : F.obj X₀ ⟶ F.obj ((data X).X j)
fac₁ : c ≫ (data X).f j = F.map b ≫ (data a.Y).f i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
⊢ (((lift hG₀ hG s ≫ G.map a.f.op) ≫ G.map ((data a.Y).f i).op) ≫ G.map (F.map b).op) ≫ G.map (F.map d).op =
    ((s.ι a ≫ G.map ((data a.Y).f i).op) ≫ G.map (F.map b).op) ≫ G.map (F.map d).op

Tactic:
have he : S (F.map e ≫ (data X).f j) := by
          rw [fac₂, assoc, fac₁]
          simpa only [assoc] using S.1.downward_closed a.hf (F.map d ≫ F.map b ≫ (data a.Y).f i)

Goal state after:
C₀ : Type u₀
C : Type u
inst✝³ : Category.{v₀, u₀} C₀
inst✝² : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : (data a.Y).I₀
X₀ : C₀
b : X₀ ⟶ (data a.Y).X i
Y : C
j : (data X).I₀
c : F.obj X₀ ⟶ F.obj ((data X).X j)
fac₁ : c ≫ (data X).f j = F.map b ≫ (data a.Y).f i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
he : (↑S).arrows (F.map e ≫ (data X).f j)
⊢ (((lift hG₀ hG s ≫ G.map a.f.op) ≫ G.map ((data a.Y).f i).op) ≫ G.map (F.map b).op) ≫ G.map (F.map d).op =
    ((s.ι a ≫ G.map ((data a.Y).f i).op) ≫ G.map (F.map b).op) ≫ G.map (F.map d).op
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : SetLike σ A
inst✝⁸ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝⁷ : GradedRing 𝒜
O : Type u_3
inst✝⁶ : CommRing O
inst✝⁵ : IsDomain O
inst✝⁴ : ValuationRing O
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra O K
inst✝¹ : IsFractionRing O K
φ₀ : ↥(𝒜 0) →+* O
ι : Type u_5
inst✝ : Finite ι
x : ι → A
h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤
j : ι
φ : Away 𝒜 (x j) →+* K
hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 (Submonoid.powers (x j)))
d : ι → ℕ
hdi : ∀ (i : ι), 0 < d i
hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)
val✝ : Fintype ι
ψ : ι → ValueGroup O K := fun i ↦ (valuation O K) (φ (Away.isLocalizationElem ⋯ ⋯) ^ ∏ k ∈ Finset.univ.erase i, d k)
this✝¹ : Nonempty ι
Kmax : ValueGroup O K := (Finset.image ψ Finset.univ).max' ⋯
i₀ : ι
hi1 : ψ i₀ = Kmax
hi₀ : ∀ (j : ι), ψ j ≤ ψ i₀
hKmax : 0 < Kmax
this✝ : Algebra (Away 𝒜 (x j)) (Away 𝒜 (x j * x i₀)) := (awayMap 𝒜 ⋯ ⋯).toAlgebra
this : IsLocalization.Away (Away.isLocalizationElem ⋯ ⋯) (Away 𝒜 (x j * x i₀))
hunit : IsUnit (φ (Away.isLocalizationElem ⋯ ⋯))
φ' : Away 𝒜 (x j * x i₀) →+* K := IsLocalization.Away.lift (Away.isLocalizationElem ⋯ ⋯) hunit
hφ'1 : ∀ (s : Away 𝒜 (x j)), φ' ((awayMap 𝒜 ⋯ ⋯) s) = φ s
sx : Away 𝒜 (x i₀)
a : ℕ
ai : ι → ℕ
hai✝ : ∑ i, ai i • d i = a • d i₀
hai : ∑ x, ai x * d x = a * d i₀
H : (∏ i, x i ^ ai i) * x i₀ ^ (a * (d j - 1)) ∈ 𝒜 ((a * d i₀) • d j)
⊢ (∏ i, ψ i ^ (d i * ai i)) * ψ i₀ ^ (d i₀ * a * (d j - 1)) ≤ (∏ i, ψ i₀ ^ (d i * ai i)) * ψ i₀ ^ (d i₀ * a * (d j - 1))

Tactic:
gcongr with i; exacts [fun i _ ↦ zero_le, zero_le, hi₀ i]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : P.ContainsIdentities
inst✝ : IsZariskiLocalAtSource P
⊢ zariskiPrecoverage ≤ propQCPrecoverage P

Tactic:
by
  rw [propQCPrecoverage, le_inf_iff]
  refine ⟨zariskiPrecoverage_le_qcPrecoverage, precoverage_mono fun X Y f hf ↦ ?_⟩
  apply IsZariskiLocalAtSource.of_isOpenImmersion

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact

Goal state before:
pp: case refine_3.inr
P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
T : Scheme
𝒰 : Cover (propQCPrecoverage P) T
this : ∀ ⦃T : Scheme⦄ (𝒰 : Cover (propQCPrecoverage P) T), (∃ R, T = Spec R) → Presieve.IsSheafFor F 𝒰.presieve₀
hT : ¬∃ R, T = Spec R
⊢ Presieve.IsSheafFor F 𝒰.presieve₀

Tactic:
refine T.affineOneHypercover.isSheafFor_of_pullback hzar ?_ ?_
      · intro i
        rw [← Sieve.pullbackArrows_comm, ← Presieve.ofArrows_pullback,
          ← Presieve.isSheafFor_iff_generate]
        exact this (𝒰.pullback₂ (T.affineCover.f i)) ⟨_, rfl⟩
      · intro i j k
        rw [← Sieve.pullbackArrows_comm, ← Presieve.isSeparatedFor_iff_generate]
        apply Presieve.IsSheafFor.isSeparatedFor
        rw [← Presieve.ofArrows_pullback]
        exact this (𝒰.pullback₂ _) ⟨_, rfl⟩

Goal state after: