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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.i * q.i * q.j = c₁ • q.j + c₂ • (q.i * q.j)

Tactic:
i_mul_i,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ (c₁ • 1 + c₂ • q.i) * q.j = c₁ • q.j + c₂ • (q.i * q.j)
Module: Mathlib.Algebra.Ring.Action.Pointwise.Finset

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommMonoid M
inst✝² : DecidableEq M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
s : Finset R
t : Finset M
⊢ 0 ∈ ↑s • ↑t ↔ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty

Tactic:
Set.zero_mem_smul_iff

Goal state after:
R : Type u_1
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommMonoid M
inst✝² : DecidableEq M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
s : Finset R
t : Finset M
⊢ 0 ∈ ↑s ∧ (↑t).Nonempty ∨ 0 ∈ ↑t ∧ (↑s).Nonempty ↔ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ (q.i * c₂ • q.j - q.i * q.i * q.j) * q.j = -((c₁ * c₃) • 1)

Tactic:
i_mul_i,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ (q.i * c₂ • q.j - (c₁ • 1 + c₂ • q.i) * q.j) * q.j = -((c₁ * c₃) • 1)
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
⊢ F (c₂ • q.j) - F q.k = c₂ • F q.j - F q.k

Tactic:
map_smul

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
⊢ c₂ • F q.j - F q.k = c₂ • F q.j - F q.k
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case ofNat
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne
this : inst₁.toNatCast = inst₂.toNatCast
toAddMonoid_eq✝ : inst₁.toAddMonoid = inst₂.toAddMonoid
toNeg_eq✝ : inst₁.toNeg = inst₂.toNeg
toSub_eq✝ : inst₁.toSub = inst₂.toSub
toZSMul_eq✝ : inst₁.toZSMul = inst₂.toZSMul
n : ℕ
⊢ IntCast.intCast (Int.ofNat n) = IntCast.intCast (Int.ofNat n)

Tactic:
| ofNat n =>

Goal state after:
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
s₁ s₂ : R
h₁ : IsSumNonzeroSq s₁
h₂ : IsSumNonzeroSq s₂
⊢ IsSumNonzeroSq (s₁ + s₂)

Tactic:
induction h₁ <;> simp_all [sq_add, add_assoc]

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.IntPolynomial

Goal state before:
pp: K : Type u_1
inst✝ : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
⊢ (int R P hP).Monic ↔ P.Monic

Tactic:
rw [Monic, Monic, ← int_leadingCoeff_eq, OneMemClass.coe_eq_one]

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.IntPolynomial

Goal state before:
pp: K : Type u_1
inst✝² : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
⊢ ∑ i ∈ Finset.range ((int R P hP).natDegree + 1), (algebraMap (↥R) L) ((int R P hP).coeff i) * x ^ i =
    ∑ i ∈ Finset.range (P.natDegree + 1), P.coeff i • x ^ i

Tactic:
exact Finset.sum_congr rfl (fun n _ => by rw [Algebra.smul_def]; rfl)

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case refine_1
R : Type uR
inst✝⁵ : Semiring R
S : Type uS
inst✝⁴ : CommSemiring S
T : Type uT
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
r✝ : R → R → Prop
inst✝¹ : Semiring T
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
⊢ ∀ x ∈ {x | ∃ a b, r a b ∧ x + b = a}, (mkRingHom r) x = 0

Tactic:
rintro y ⟨a, b, h, su⟩
        symm at su
        rw [← sub_eq_iff_eq_add] at su
        rw [← su, map_sub, mkRingHom_rel h, sub_self]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f : CentroidHom α
x✝ : α
⊢ (star (star f)) x✝ = f x✝

Tactic:
rw [star_apply, star_apply, star_star, star_star]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
a b : FreeAlgebra R X
⊢ (MulOpposite.unop ∘ ⇑((lift R) (MulOpposite.op ∘ ι R))) (a + b) =
    (MulOpposite.unop ∘ ⇑((lift R) (MulOpposite.op ∘ ι R))) a +
      (MulOpposite.unop ∘ ⇑((lift R) (MulOpposite.op ∘ ι R))) b

Tactic:
by simp only [Function.comp_apply, map_add, MulOpposite.unop_add]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
n : ℕ
⊢ (erase n p).coeff n = 0

Tactic:
simp [coeff_erase]

Goal state after:
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ✝ : Type u_1
inst✝¹⁴ : PartialOrder Γ✝
R✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
inst✝¹³ : CommRing R✝
inst✝¹² : AddCommGroup V✝
inst✝¹¹ : Module R✝ V✝
inst✝¹⁰ : AddCommGroup W✝
inst✝⁹ : Module R✝ W✝
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
⊢ ∀ (x y : U),
    (of R) (A.compHahnSeries B (x + y)).ofIterate =
      (of R) (A.compHahnSeries B x).ofIterate + (of R) (A.compHahnSeries B y).ofIterate

Tactic:
by
    intro u v
    ext g
    simp [HahnSeries.ofIterate]

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

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : ↥U → Opens ↑↑X.toPresheafedSpace
iVU : (x : ↥U) → V x ⟶ U
m : ∀ (x : ↥U), ↑x ∈ V x
h_unit : ∀ (x : ↥U), IsUnit ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f)
hcover : U ≤ iSup V
g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))
hg : ∀ (x : ↥U), (ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f * g x = 1
x y : ↥U
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ (ConcreteCategory.hom ((sheaf X).presheaf.germ (V x ⊓ V y) z ⋯))
      ((ConcreteCategory.hom ((sheaf X).obj.map ((V x).infLELeft (V y)).op)) (g x)) =
    (ConcreteCategory.hom ((sheaf X).presheaf.germ (V x ⊓ V y) z ⋯))
      ((ConcreteCategory.hom ((sheaf X).obj.map ((V x).infLERight (V y)).op)) (g y))

Tactic:
germ_res_apply,

Goal state after:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : ↥U → Opens ↑↑X.toPresheafedSpace
iVU : (x : ↥U) → V x ⟶ U
m : ∀ (x : ↥U), ↑x ∈ V x
h_unit : ∀ (x : ↥U), IsUnit ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f)
hcover : U ≤ iSup V
g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))
hg : ∀ (x : ↥U), (ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f * g x = 1
x y : ↥U
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ (ConcreteCategory.hom ((sheaf X).presheaf.germ (V x) z ⋯)) (g x) =
    (ConcreteCategory.hom ((sheaf X).presheaf.germ (V x ⊓ V y) z ⋯))
      ((ConcreteCategory.hom ((sheaf X).obj.map ((V x).infLERight (V y)).op)) (g y))
Module: Mathlib.Topology.Sheaves.SheafOfFunctions

Goal state before:
pp: X : TopCat
T : ↑X → Type u_1
ι : Type u_2
U : ι → Opens ↑X
sf : (i : ι) → ToType ((X.presheafToTypes T).obj (Opposite.op (U i)))
hsf : (X.presheafToTypes T).IsCompatible U sf
⊢ ∃! s, (X.presheafToTypes T).IsGluing U sf s

Tactic:
by
  -- We use the sheaf condition in terms of unique gluing
  -- U is a family of open sets, indexed by `ι` and `sf` is a compatible family of sections.
  -- In the informal comments below, I'll just write `U` to represent the union.
    -- Our first goal is to define a function "lifted" to all of `U`.
    -- We do this one point at a time. Using the axiom of choice, we can pick for each
    -- `x : ↑(iSup U)` an index `i : ι` such that `x` lies in `U i`
    choose index index_spec using fun x : ↑(iSup U) => Opens.mem_iSup.mp x.2
    -- Using this data, we can glue our functions together to a single section
    let s : ∀ x : ↑(iSup U), T x := fun x => sf (index x) ⟨x.1, index_spec x⟩
    refine ⟨s, ?_, ?_⟩
    · intro i
      funext x
      -- Now we need to verify that this lifted function restricts correctly to each set `U i`.
      -- Of course, the difficulty is that at any given point `x ∈ U i`,
      -- we may have used the axiom of choice to pick a different `j` with `x ∈ U j`
      -- when defining the function.
      -- Thus we'll need to use the fact that the restrictions are compatible.
      exact congr_fun (hsf (index ⟨x, _⟩) i) ⟨x, ⟨index_spec ⟨x.1, _⟩, x.2⟩⟩
    · -- Now we just need to check that the lift we picked was the only possible one.
      -- So we suppose we had some other gluing `t` of our sections
      intro t ht
      -- and observe that we need to check that it agrees with our choice
      -- for each `x ∈ ↑(iSup U)`.
      funext x
      exact congr_fun (ht (index x)) ⟨x.1, index_spec x⟩

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

Goal state before:
pp: case naturality
J : Type u'
inst✝⁵ : Category.{v', u'} J
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasColimitsOfShape J TopCat
inst✝² : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝¹ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
inst✝ : HasColimit F
U : Opens ↑↑(Limits.colimit F)
⊢ autoParam
    (∀ {X Y : Jᵒᵖ} (f : X ⟶ Y),
      ((pushforwardDiagramToColimit F).leftOp ⋙
                (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj
                  ((Opens.map
                          (colimit.isoColimitCocone
                                  { cocone := colimitCocone F,
                                    isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
                    (op U))).map
            f ≫
          (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom =
        (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f)
    NatIso.ofComponents._auto_1

Tactic:
· intro X Y f
    change ((F.map f.unop).c.app _ ≫ _ ≫ _) ≫ (F.obj (unop Y)).presheaf.map _ = _ ≫ _
    rw [TopCat.Presheaf.Pushforward.comp_inv_app]
    erw [Category.id_comp]
    rw [Category.assoc]
    erw [← (F.obj (unop Y)).presheaf.map_comp, (F.map f.unop).c.naturality_assoc,
      ← (F.obj (unop Y)).presheaf.map_comp]
    rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
⊢ f ≫ toPushforwardStalk f p =
    CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op ⊤))) ≫
      (structurePresheafInCommRingCat ↑R).germ ⊤ p trivial ≫
        (TopCat.Presheaf.stalkFunctor CommRingCat p).map (Spec.sheafedSpaceMap f).hom.c

Tactic:
TopCat.Presheaf.stalkFunctor_map_germ

Goal state after:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
⊢ f ≫ toPushforwardStalk f p =
    CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op ⊤))) ≫
      (Spec.sheafedSpaceMap f).hom.c.app (op ⊤) ≫
        ((TopCat.Presheaf.pushforward CommRingCat (Spec.sheafedSpaceMap f).hom.base).obj
              (Spec.sheafedSpaceObj S).presheaf).germ
          ⊤ p trivial
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : X.Opens
⊢ app (𝟙 X) U ≫ X.presheaf.map (eqToHom ⋯).op = X.presheaf.map (eqToHom ⋯).op

Tactic:
id_app,

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : X.Opens
⊢ 𝟙 Γ(X, U) ≫ X.presheaf.map (eqToHom ⋯).op = X.presheaf.map (eqToHom ⋯).op
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
i : ι
hx : x ∈ Set.range ⇑(ConcreteCategory.hom (f i))
⊢ ∃ Y_1 g, Presieve.ofArrows Y f g ∧ x ∈ Set.range ⇑(ConcreteCategory.hom g)

Tactic:
use Y i, f i, ⟨i⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : AlgebraicGeometry.IsOpenImmersion f
⊢ toScheme Y f.toPshHom = X

Tactic:
apply scheme_eq_of_locallyRingedSpace_eq
  exact locallyRingedSpace_toLocallyRingedSpace f.toLRSHom

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ HasLimit (cospan ((cospan f g ⋙ forget).map WalkingCospan.Hom.inl) ((cospan f g ⋙ forget).map WalkingCospan.Hom.inr))

Tactic:
exact inferInstanceAs (HasLimit (cospan ((forget).map f) ((forget).map g)))

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
⊢ Hom.app (f ∣_ U) V = Hom.app f (U.ι ''ᵁ V) ≫ X.presheaf.map (eqToHom ⋯).op

Tactic:
obtain ⟨V, rfl⟩ : ∃ V', U.ι ⁻¹ᵁ U.ι ''ᵁ V' = V := ⟨_, U.ι.preimage_image_eq V⟩
  simpa [← Functor.map_comp_assoc, ← Functor.map_comp] using!
    congr(Y.presheaf.map (eqToHom (congr_arg (U.ι ''ᵁ ·) (U.ι.preimage_image_eq V).symm)).op ≫
      $(Scheme.Hom.congr_app (morphismRestrict_ι f U) (U.ι ''ᵁ V)))

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
x : ↑X.toTopCat
p : PrimeSpectrum ↑(Γ.obj (op X)) := X.toΓSpecFun x
S : CommRingCat := (structureSheaf ↑(Γ.obj (op X))).presheaf.stalk p
t : ↑S
ht : IsUnit ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x)) t)
r : ↑(Γ.obj (op X))
s : ↥p.asIdeal.primeCompl
he : t * (algebraMap ↑(Γ.obj (op X)) ↑S) ↑(r, s).2 = (algebraMap ↑(Γ.obj (op X)) ↑S) (r, s).1
⊢ IsUnit t

Tactic:
dsimp at he

Goal state after:
X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
x : ↑X.toTopCat
p : PrimeSpectrum ↑(Γ.obj (op X)) := X.toΓSpecFun x
S : CommRingCat := (structureSheaf ↑(Γ.obj (op X))).presheaf.stalk p
t : ↑S
ht : IsUnit ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x)) t)
r : ↑(Γ.obj (op X))
s : ↥p.asIdeal.primeCompl
he : t * (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) ↑s = (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r
⊢ IsUnit t
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case refine_2
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ IsPullback (g ∣_ UX) (resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯) (resLE iX US UX hUSX) (f ∣_ US)

Tactic:
refine .of_bot ?_ ?_ (isPullback_morphismRestrict f US)

Goal state after:
case refine_2.refine_1
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ IsPullback (g ∣_ UX) (resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯ ≫ (f ⁻¹ᵁ US).ι) (resLE iX US UX hUSX ≫ US.ι) f

case refine_2.refine_2
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ g ∣_ UX ≫ resLE iX US UX hUSX = resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯ ≫ f ∣_ US
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)
r : R
m : ↑((structurePresheafInModuleCat R M).stalk x)
⊢ (ConcreteCategory.hom (toStalk R x)) r • (modulePresheafStalkIso R M x).symm m =
    (modulePresheafStalkIso R M x).symm (r • m)

Tactic:
map_smul

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
r : R
m : ↑((structurePresheafInModuleCat R M).stalk x)
⊢ (ConcreteCategory.hom (toStalk R x)) r • (modulePresheafStalkIso R M x).symm m =
    r • (modulePresheafStalkIso R M x).symm m
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
⊢ IsPushout (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X)) (coequalizer.π f g) (f ≫ coequalizer.π f g)

Tactic:
refine ⟨⟨by ext <;> simp [coequalizer.condition f g]⟩, ⟨PushoutCocone.IsColimit.mk _ ?_ ?_ ?_ ?_⟩⟩
  · refine fun s ↦ coequalizer.desc s.inl ?_
    have H₁ : f ≫ s.inl = s.inr := by simpa using congr(coprod.inl ≫ $s.condition)
    have H₂ : g ≫ s.inl = s.inr := by simpa using congr(coprod.inr ≫ $s.condition)
    exact H₁.trans H₂.symm
  · exact fun s ↦ by simp
  · exact fun s ↦ by simpa using congr(coprod.inl ≫ $s.condition)
  · exact fun s m hm _ ↦ by ext; simp [*]

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
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.mk x✝ 1)) =
    LocalizedModule.mk x✝ 1

Tactic:
rw [← LocalizedModule.mkLinearMap_apply, IsLocalizedModule.lift_apply,
      elementwise_of% toStalkₗ'_stalkToFiberRingHom (M := M) x]

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
⊢ (ConcreteCategory.hom (ModuleCat.ofHom (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M))) x✝ =
    (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M) x✝
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)
r : R
m : M
⊢ (ConcreteCategory.hom (germ (moduleStructurePresheaf R M).presheaf ⊤ x ⋯)) ((toOpenₗ R M ⊤) (r • m)) =
    (ConcreteCategory.hom (toStalk R x)) r •
      (ConcreteCategory.hom (germ (moduleStructurePresheaf R M).presheaf ⊤ x ⋯)) ((toOpenₗ R M ⊤) m)

Tactic:
map_smul

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)
r : R
m : M
⊢ (ConcreteCategory.hom (germ (moduleStructurePresheaf R M).presheaf ⊤ x ⋯)) (r • (toOpenₗ R M ⊤) m) =
    (ConcreteCategory.hom (toStalk R x)) r •
      (ConcreteCategory.hom (germ (moduleStructurePresheaf R M).presheaf ⊤ x ⋯)) ((toOpenₗ R M ⊤) m)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ IsLocalization.Away f ↑Γ(X, X.basicOpen f)

Tactic:
by
  apply
    (IsLocalization.isLocalization_iff_of_ringEquiv (Submonoid.powers f)
      (asIso <| basicOpenSectionsToAffine hU f).commRingCatIsoToRingEquiv).mpr
  convert! StructureSheaf.IsLocalization.to_basicOpen _ f using 1
  apply Algebra.algebra_ext
  intro _
  congr 1
  dsimp [CommRingCat.ofHom, RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp,
    basicOpenSectionsToAffine]
  rw [hU.fromSpec.naturality_assoc, hU.fromSpec_app_self]
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
g : ↑Γ(X, X.basicOpen f)
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
⊢ ∃ f', X.basicOpen f' = X.basicOpen g

Tactic:
obtain ⟨x, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.surj'' (Submonoid.powers f) g

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, U)
n : ℕ
⊢ ∃ f',
    X.basicOpen f' =
      X.basicOpen
        (x • ↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) ↑Γ(X, X.basicOpen f)) ⟨(fun x ↦ f ^ x) n, ⋯⟩))
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)
⊢ IsLocalization.AtPrime (↑((structurePresheafInCommRingCat R).stalk x)) x.asIdeal

Tactic:
refine (isLocalizedModule_iff_isLocalization' _ _).mp ?_
  convert!
    IsLocalizedModule.of_linearEquiv x.asIdeal.primeCompl (toStalkₗ R R x)
      (commRingCatStalkEquivModuleStalk R x)
  let α : TopCat.Presheaf.stalk (moduleStructurePresheaf R R).presheaf x ≅
    (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).obj
      ((structurePresheafInCommRingCat R).stalk x) :=
    (Limits.colimit.isoColimitCocone ⟨_, Limits.isColimitOfPreserves
    (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat)
    (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙
      structurePresheafInCommRingCat R))⟩)
  have : (TopCat.Presheaf.germ (moduleStructurePresheaf R R).presheaf ⊤ x (by simp)) ≫ α.hom =
      (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).map
        ((structurePresheafInCommRingCat R).germ ⊤ x (by simp)) :=
    Limits.colimit.isoColimitCocone_ι_hom ..
  ext
  dsimp [toStalkₗ]
  simp only [map_one]
  refine .trans ?_ congr($this _).symm
  exact (((structurePresheafInCommRingCat R).germ ⊤ x (by simp)).hom.comp
    (algebraMap R Γ(R, _))).map_one.symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ hU.fromSpec (hU.primeIdealOf x) = ↑x

Tactic:
dsimp only [IsAffineOpen.fromSpec, Subtype.coe_mk, IsAffineOpen.primeIdealOf]
  rw [← Scheme.Hom.comp_apply, Iso.hom_inv_id_assoc]
  rfl

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: 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))
⊢ IsOpen
    (⇑(TopCat.homeoOfIso (PreservesCoequalizer.iso (SheafedSpace.forget CommRingCat) (Hom.toShHom f) (Hom.toShHom g))) ∘
        ⇑(ConcreteCategory.hom
            (coequalizer.π ((SheafedSpace.forget CommRingCat).map (Hom.toShHom f))
              ((SheafedSpace.forget CommRingCat).map (Hom.toShHom g)))) ⁻¹'
      ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) ''
        (imageBasicOpen f g U s).carrier)

Tactic:
← TopCat.coe_comp

Goal state after:
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))
⊢ IsOpen
    (⇑(ConcreteCategory.hom
          (coequalizer.π ((SheafedSpace.forget CommRingCat).map (Hom.toShHom f))
              ((SheafedSpace.forget CommRingCat).map (Hom.toShHom g)) ≫
            (PreservesCoequalizer.iso (SheafedSpace.forget CommRingCat) (Hom.toShHom f) (Hom.toShHom g)).hom)) ⁻¹'
      ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) ''
        (imageBasicOpen f g U s).carrier)