mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
y' : M
hy'✝ : y' ∈ (f.extendFun hx).domain
hy' : y' ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = y'
k : K
hk : k • x = b
⊢ toLex ((truncLTLinearMap K c) (ofLex (↑↑f ⟨a, ha⟩)) + (truncLTLinearMap K c) (ofLex ((RingHom.id K) k • f.eval x))) ∈
    ((↑f).supSpanSingleton x (f.eval x) hx).toFun.range

Tactic:
toLex_add,

Goal state after:
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
y' : M
hy'✝ : y' ∈ (f.extendFun hx).domain
hy' : y' ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = y'
k : K
hk : k • x = b
⊢ toLex ((truncLTLinearMap K c) (ofLex (↑↑f ⟨a, ha⟩))) +
      toLex ((truncLTLinearMap K c) (ofLex ((RingHom.id K) k • f.eval x))) ∈
    ((↑f).supSpanSingleton x (f.eval x) hx).toFun.range
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
i : Fin 2
m✝ : Fin 2 →₀ ℕ
⊢ MvPolynomial.coeff m✝
      (((aevalAeval (MvPolynomial.X 0) (MvPolynomial.X 1)).comp (MvPolynomial.aeval ![C X, Y])) (MvPolynomial.X i)) =
    MvPolynomial.coeff m✝ ((AlgHom.id R (MvPolynomial (Fin 2) R)) (MvPolynomial.X i))

Tactic:
fin_cases i <;> simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = f
⊢ h ∣ f.mirror

Tactic:
← hk

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = f
⊢ h ∣ k.mirror
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = f.mirror
⊢ g ∣ f.mirror

Tactic:
← hk

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = f.mirror
⊢ g ∣ k
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hkn : k ≤ n
i : Fin 2
⊢ (fun₀ | 0 => m 0 | 1 => m 1) i = m i

Tactic:
fin_cases i <;> simp

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a : α
⊢ a ∈ destutter' R a l

Tactic:
by
  induction l with
  | nil => simp
  | cons b l hl =>
    rw [destutter']
    split_ifs
    · simp
    · assumption

Goal state after:
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: case monomial.succ
R : Type u_1
inst✝⁴ : Semiring R
p : R[X]
S : Type u_2
inst✝³ : NonAssocSemiring S
inst✝² : Module R S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
a : R
n : ℕ
⊢ ((monomial (n + 1)) a).smeval 0 = ((monomial (n + 1)) a).coeff 0 • 1

Tactic:
rw [coeff_monomial_succ, smeval_monomial, npow_add, npow_one, mul_zero, zero_smul,
        smul_zero]

Goal state after:
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p : ℤ[X]
hp : p.IsUnitTrinomial
⊢ ¬IsUnit p

Tactic:
obtain ⟨k, m, n, hkm, hmn, u, v, w, rfl⟩ := hp

Goal state after:
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ ¬IsUnit (trinomial k m n ↑u ↑v ↑w)
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p : ℤ[X]
hp : p.IsUnitTrinomial
⊢ #p.support = 3

Tactic:
obtain ⟨k, m, n, hkm, hmn, u, v, w, rfl⟩ := hp

Goal state after:
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ #(trinomial k m n ↑u ↑v ↑w).support = 3
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p : ℤ[X]
hp : p.IsUnitTrinomial
k : ℕ
hk : k ∈ p.support
⊢ IsUnit (p.coeff k)

Tactic:
obtain ⟨k, m, n, hkm, hmn, u, v, w, rfl⟩ := hp

Goal state after:
k✝ k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hk : k✝ ∈ (trinomial k m n ↑u ↑v ↑w).support
⊢ IsUnit ((trinomial k m n ↑u ↑v ↑w).coeff k✝)
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : SignType.sign P.leadingCoeff = SignType.sign P.nextCoeff
hpz : ¬P = 0
⊢ P.eraseLead.signVariations = P.signVariations

Tactic:
have h₂ : nextCoeff P ≠ 0 := by intro; simp_all

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : SignType.sign P.leadingCoeff = SignType.sign P.nextCoeff
hpz : ¬P = 0
h₂ : P.nextCoeff ≠ 0
⊢ P.eraseLead.signVariations = P.signVariations
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R✝ : Type u_4
α : Type u_5
inst✝¹⁶ : NonUnitalNonAssocSemiring α
inst✝¹⁵ : Monoid M
inst✝¹⁴ : Monoid N
inst✝¹³ : Semiring R✝
inst✝¹² : DistribMulAction M α
inst✝¹¹ : SMulCommClass M α α
inst✝¹⁰ : IsScalarTower M α α
inst✝⁹ : DistribMulAction N α
inst✝⁸ : SMulCommClass N α α
inst✝⁷ : IsScalarTower N α α
inst✝⁶ : Module R✝ α
inst✝⁵ : SMulCommClass R✝ α α
inst✝⁴ : IsScalarTower R✝ α α
R : Type u_6
inst✝³ : CommSemiring «R»
inst✝² : Module «R» α
inst✝¹ : SMulCommClass «R» α α
inst✝ : IsScalarTower «R» α α
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp only [ZeroMemClass.coe_zero, map_zero]
    exact rfl

Goal state after:
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f g : ↥(Subsemiring.center (CentroidHom α))
a : α
⊢ (star (f * g)) a = (star (g * f)) a

Tactic:
by rw [CommMonoid.mul_comm f g]

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
⊢ Finset.map toAdd.toEmbedding (single (ofAdd n) a).support ⊆ {n}

Tactic:
refine Finset.subset_map_symm.mp SkewMonoidAlgebra.support_single_subset

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p : SkewPolynomial R
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
s : Finset ℕ
hs : p.support ⊆ s
x✝ : ℕ
a✝ : x✝ ∈ s
hx : p.coeff x✝ = 0
⊢ f x✝ (p.coeff x✝) = 0

Tactic:
simp [hx, hf]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : (ConcreteCategory.hom (α ≫ β).base) x = x
⊢ eqToHom ⋯ ≫
      Hom.stalkMap α ((ConcreteCategory.hom (α ≫ β).base) x) ≫ Hom.stalkMap β ((ConcreteCategory.hom α.base) x) =
    𝟙 (Y.presheaf.stalk ((ConcreteCategory.hom α.base) x))

Tactic:
erw [← stalkMap.comp β α (α.base x)]

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : (ConcreteCategory.hom (α ≫ β).base) x = x
⊢ eqToHom ⋯ ≫ Hom.stalkMap (β ≫ α) ((ConcreteCategory.hom α.base) x) =
    𝟙 (Y.presheaf.stalk ((ConcreteCategory.hom α.base) x))
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : ↥↑U) → T ↑y),
    P.pred fU →
      ∀ (fV : (y : ↥↑V) → T ↑y), P.pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥↑W), fU (iU w) = fV (iV w)
tU tV : (fun X ↦ X) ((subsheafToTypes P).presheaf.stalk x)
h : (ConcreteCategory.hom (stalkToFiber P x)) tU = (ConcreteCategory.hom (stalkToFiber P x)) tV
⊢ tU = tV

Tactic:
let Q :
    ∃ (W : (OpenNhds x)ᵒᵖ) (s : ∀ w : (unop W).1, T w) (hW : P.pred s),
      tU = (subsheafToTypes P).presheaf.germ _ x (unop W).2 ⟨s, hW⟩ ∧
        tV = (subsheafToTypes P).presheaf.germ _ x (unop W).2 ⟨s, hW⟩ :=
    ?_
  · choose W s hW e using Q
    exact e.1.trans e.2.symm
  -- Then use induction to pick particular representatives of `tU tV : stalk x`
  dsimp at tU tV h
  obtain ⟨U, ⟨fU, hU⟩, rfl⟩ := jointly_surjective' tU
  obtain ⟨V, ⟨fV, hV⟩, rfl⟩ := jointly_surjective' tV
  -- Decompose everything into its constituent parts:
  simp only [Functor.whiskeringLeft_obj_obj, Functor.comp_obj, Functor.op_obj,
    subpresheafToTypes_obj, stalkToFiber_ι] at h
  specialize w (unop U) (unop V) fU hU fV hV h
  rcases w with ⟨W, iU, iV, w⟩
  -- and put it back together again in the correct order.
  refine ⟨op W, fun w ↦ fU (iU w : (unop U).1), P.res ?_ _ hU, ?_⟩
  · rcases W with ⟨W, m⟩
    exact iU
  · exact ⟨colimit_sound iU.op (Subtype.ext rfl), colimit_sound iV.op (Subtype.ext (funext w).symm)⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).stalk
      p)
U : TopologicalSpace.Opens ↑(Spec.topObj (CommRingCat.of ↑R))
hp : p ∈ U
s :
  ToType
    (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).obj
      (op U))
r : ↑(CommRingCat.of ↑R)
hpr : p ∈ PrimeSpectrum.basicOpen r
hrU : PrimeSpectrum.basicOpen r ≤ U
s' :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).obj
      (op (PrimeSpectrum.basicOpen r)))
h :
  s' =
    (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).map
          (homOfLE hrU).op))
      s
e :
  (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          (PrimeSpectrum.basicOpen r) p hpr))
      s' =
    y
⊢ ∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1

Tactic:
clear! U

Goal state after:
R S : CommRingCat
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).stalk
      p)
r : ↑(CommRingCat.of ↑R)
hpr : p ∈ PrimeSpectrum.basicOpen r
s' :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).obj
      (op (PrimeSpectrum.basicOpen r)))
e :
  (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          (PrimeSpectrum.basicOpen r) p hpr))
      s' =
    y
⊢ ∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: U V X Y : Scheme
g : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
f : X ⟶ Y
inst✝¹ : IsOpenImmersion iU
inst✝ : IsOpenImmersion iV
H : iU ≫ f = g ≫ iV
H' : f ⁻¹ᵁ Scheme.Hom.opensRange iV = Scheme.Hom.opensRange iU
⊢ IsPullback g iU iV f

Tactic:
let e := IsOpenImmersion.isoOfRangeEq (pullback.snd iV f) iU
    (by simpa [range_pullbackSnd] using congr(($H').1))
  convert!
    (IsPullback.of_horiz_isIso
          (show CommSq e.inv iU (pullback.snd iV f) (𝟙 X) from ⟨by simp [e]⟩)).paste_horiz
      (IsPullback.of_hasPullback iV f)
  simp [← cancel_mono iV, e, pullback.condition, H]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
⊢ Y.presheaf.map (homOfLE ⋯).op ≫ (ΓIso f U).inv = Scheme.Hom.app f U

Tactic:
by
  simp [Scheme.Hom.appLE_eq_app]

Goal state after:
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
𝒰 : X.OpenCover
H : CompactSpace ↥X
this : ∃ t, ⋃ x ∈ t, Set.range ⇑(𝒰.f (Cover.idx 𝒰 x)) = ⊤
t : Finset ↥X := this.choose
⊢ X.OpenCover

Tactic:
have h : ∀ x : X, ∃ y : t, x ∈ Set.range (𝒰.f (𝒰.idx y)) := by
    intro x
    have h' : x ∈ (⊤ : Set X) := trivial
    rw [← Classical.choose_spec this, Set.mem_iUnion] at h'
    rcases h' with ⟨y, _, ⟨hy, rfl⟩, hy'⟩
    exact ⟨⟨y, hy⟩, hy'⟩

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
𝒰 : X.OpenCover
H : CompactSpace ↥X
this : ∃ t, ⋃ x ∈ t, Set.range ⇑(𝒰.f (Cover.idx 𝒰 x)) = ⊤
t : Finset ↥X := this.choose
h : ∀ (x : ↥X), ∃ y, x ∈ Set.range ⇑(𝒰.f (Cover.idx 𝒰 ↑y))
⊢ X.OpenCover
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Y.restrict ⋯ ⟶ X

Tactic:
use PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.1 g.1
    intro x
    have := PresheafedSpace.stalkMap.congr_hom _ _
        (PresheafedSpace.IsOpenImmersion.pullback_cone_of_left_condition f.1 g.1) x
    rw [PresheafedSpace.stalkMap.comp, PresheafedSpace.stalkMap.comp] at this
    rw [← IsIso.eq_inv_comp] at this
    rw [this]
    dsimp
    apply RingHom.isLocalHom_comp

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
P : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
r : ↥(sectionsSubalgebra R U)
a : (x : ↥U) → Localizations M ↑x
ha✝ : a ∈ (sectionsSubmodule M U).carrier
x : ↥U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V
hVU : V ⟶ U
rx rs : R
hr : ∀ (x : ↥V), ∃ (hs : rs ∉ (↑x).asIdeal), (fun x ↦ ↑r (hVU x)) x = LocalizedModule.mk rx ⟨rs, hs⟩
W : Opens ↑(PrimeSpectrum.Top R)
hxW : ↑x ∈ W
hWU : W ⟶ U
ax : M
as : R
ha : ∀ (x : ↥W), ∃ (hs : as ∉ (↑x).asIdeal), (fun x ↦ a (hWU x)) x = LocalizedModule.mk ax ⟨as, hs⟩
y : ↥(V ⊓ W)
hrsy : rs ∉ (↑⟨↑y, ⋯⟩).asIdeal
hry : (fun x ↦ ↑r (hVU x)) ⟨↑y, ⋯⟩ = LocalizedModule.mk rx ⟨rs, hrsy⟩
⊢ ∃ (hs : as * rs ∉ (↑y).asIdeal), (fun x ↦ (r • a) ((homOfLE ⋯) x)) y = LocalizedModule.mk (rx • ax) ⟨as * rs, hs⟩

Tactic:
obtain ⟨hasy, hay⟩ := ha ⟨y.1, y.2.2⟩

Goal state after:
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
P : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
r : ↥(sectionsSubalgebra R U)
a : (x : ↥U) → Localizations M ↑x
ha✝ : a ∈ (sectionsSubmodule M U).carrier
x : ↥U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V
hVU : V ⟶ U
rx rs : R
hr : ∀ (x : ↥V), ∃ (hs : rs ∉ (↑x).asIdeal), (fun x ↦ ↑r (hVU x)) x = LocalizedModule.mk rx ⟨rs, hs⟩
W : Opens ↑(PrimeSpectrum.Top R)
hxW : ↑x ∈ W
hWU : W ⟶ U
ax : M
as : R
ha : ∀ (x : ↥W), ∃ (hs : as ∉ (↑x).asIdeal), (fun x ↦ a (hWU x)) x = LocalizedModule.mk ax ⟨as, hs⟩
y : ↥(V ⊓ W)
hrsy : rs ∉ (↑⟨↑y, ⋯⟩).asIdeal
hry : (fun x ↦ ↑r (hVU x)) ⟨↑y, ⋯⟩ = LocalizedModule.mk rx ⟨rs, hrsy⟩
hasy : as ∉ (↑⟨↑y, ⋯⟩).asIdeal
hay : (fun x ↦ a (hWU x)) ⟨↑y, ⋯⟩ = LocalizedModule.mk ax ⟨as, hasy⟩
⊢ ∃ (hs : as * rs ∉ (↑y).asIdeal), (fun x ↦ (r • a) ((homOfLE ⋯) x)) y = LocalizedModule.mk (rx • ax) ⟨as * rs, hs⟩
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : R
f : M
n : ℕ
⊢ (IsLocalizedModule.lift (Submonoid.powers s) (LocalizedModule.mkLinearMap (Submonoid.powers s) M)
        (toOpenₗ R M (basicOpen s)) ⋯)
      ((LocalizedModule.mkLinearMap (Submonoid.powers s) M) f) =
    s ^ n • const f (s ^ n) (basicOpen s) ⋯

Tactic:
IsLocalizedModule.lift_apply,

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : R
f : M
n : ℕ
⊢ (toOpenₗ R M (basicOpen s)) f = s ^ n • const f (s ^ n) (basicOpen s) ⋯
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
r : R
m : (structureSheafInType R M).obj.obj (op U)
⊢ (↑(AddCommGrpCat.Hom.hom (Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU))).toFun (r • m) =
    (ConcreteCategory.hom (toStalk R x)) ((RingHom.id R) r) •
      (ConcreteCategory.hom (Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU)) m

Tactic:
rw [← algebraMap_germ_apply U x hxU]

Goal state after:
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
r : R
m : (structureSheafInType R M).obj.obj (op U)
⊢ (↑(AddCommGrpCat.Hom.hom (Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU))).toFun (r • m) =
    (ConcreteCategory.hom ((structurePresheafInCommRingCat R).germ U x hxU))
        ((algebraMap R ((structureSheafInType R R).obj.obj (op U))) ((RingHom.id R) r)) •
      (ConcreteCategory.hom (Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU)) m
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
⊢ (IsLocalizedModule.lift x.asIdeal.primeCompl (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)
        (ModuleCat.Hom.hom (toStalkₗ' R M x)) ⋯)
      ((LocalizedModule.mkLinearMap x.asIdeal.primeCompl M) f) =
    ↑s •
      (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ (basicOpen ↑s) x ⋯))
        (const f (↑s) (basicOpen ↑s) ⋯)

Tactic:
IsLocalizedModule.lift_apply,

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 (toStalkₗ' R M x)) f =
    ↑s •
      (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ (basicOpen ↑s) x ⋯))
        (const f (↑s) (basicOpen ↑s) ⋯)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
x✝ : M
⊢ (ModuleCat.Hom.hom (stalkToLocalizationₗ R M x))
      ((IsLocalizedModule.lift x.asIdeal.primeCompl (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)
          (ModuleCat.Hom.hom (toStalkₗ' R M x)) ⋯)
        ((LocalizedModule.mkLinearMap x.asIdeal.primeCompl M) x✝)) =
    (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M) x✝

Tactic:
IsLocalizedModule.lift_apply,

Goal state after:
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
x✝ : M
⊢ (ModuleCat.Hom.hom (stalkToLocalizationₗ R M x)) ((ModuleCat.Hom.hom (toStalkₗ' R M x)) x✝) =
    (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M) x✝
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
U V : Opens ↑(PrimeSpectrum.Top R)
iVU : V ⟶ U
s : ↑((structureSheaf R).obj.obj (op U))
p : ↥(unop (op V))
⊢ (Localization.localRingHom (PrimeSpectrum.comap (RingHom.id R) ↑p).asIdeal (↑p).asIdeal (RingHom.id R) ⋯)
      (↑s ⟨PrimeSpectrum.comap (RingHom.id R) ↑p, ⋯⟩) =
    ↑((CommRingCat.Hom.hom ((structureSheaf R).obj.map iVU.op)) s) p

Tactic:
exact congr($(Localization.localRingHom_id ..) _)

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⨆ f, X.basicOpen ↑f = U ↔ ⋃ i, (PrimeSpectrum.basicOpen ↑i).carrier = Set.univ

Tactic:
trans hU.fromSpec ⁻¹' (⨆ f : s, X.basicOpen (f : Γ(X, U))).1 = hU.fromSpec ⁻¹' U.1

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⨆ f, X.basicOpen ↑f = U ↔ ⇑hU.fromSpec ⁻¹' (⨆ f, X.basicOpen ↑f).carrier = ⇑hU.fromSpec ⁻¹' U.carrier

X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⇑hU.fromSpec ⁻¹' (⨆ f, X.basicOpen ↑f).carrier = ⇑hU.fromSpec ⁻¹' U.carrier ↔
    ⋃ i, (PrimeSpectrum.basicOpen ↑i).carrier = Set.univ
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case refine_3
R S : CommRingCat
f : R ⟶ S
r : ↑R
hcomp :
  CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r)) ≫
      CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r) =
    f ≫ CommRingCat.ofHom (algebraMap (↑S) (Localization.Away ((CommRingCat.Hom.hom f) r)))
⊢ (((Spec S).isoOfEq ⋯ ≪≫ basicOpenIsoSpecAway ((CommRingCat.Hom.hom f) r)).hom ≫
        (Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))).hom) ≫
      Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) =
    ((Arrow.mk (Spec.map f ∣_ basicOpen r)).hom ≫ (basicOpenIsoSpecAway r).hom) ≫
      Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r)))

Tactic:
simp only [Arrow.mk_hom, Category.assoc, ← Spec.map_comp]

Goal state after:
case refine_3
R S : CommRingCat
f : R ⟶ S
r : ↑R
hcomp :
  CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r)) ≫
      CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r) =
    f ≫ CommRingCat.ofHom (algebraMap (↑S) (Localization.Away ((CommRingCat.Hom.hom f) r)))
⊢ ((Spec S).isoOfEq ⋯ ≪≫ basicOpenIsoSpecAway ((CommRingCat.Hom.hom f) r)).hom ≫
      Spec.map
        (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r)) ≫
          CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)) =
    Spec.map f ∣_ basicOpen r ≫
      (basicOpenIsoSpecAway r).hom ≫ Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r)))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal ↑Γ(X, U)
t : Set ι
ht : t.Finite
ht' : t.Nonempty
⊢ X.zeroLocus ↑(⨅ i ∈ t, I i) = ⋃ i ∈ t, X.zeroLocus ↑(I i)

Tactic:
rw [zeroLocus_biInf I ht, Set.union_eq_left]

Goal state after:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal ↑Γ(X, U)
t : Set ι
ht : t.Finite
ht' : t.Nonempty
⊢ (↑U)ᶜ ⊆ ⋃ i ∈ t, X.zeroLocus ↑(I i)