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

Goal state before:
pp: case inr
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : -p * -p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : -p = C (-↑u) * X ^ k + C (-↑v) * X ^ m + C (-↑w) * X ^ n
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x) (-↑v) ↑z
h1 : ↑y = -↑v
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

Tactic:
← mirror_neg

Goal state after:
case inr
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : -p * (-p).mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : -p = C (-↑u) * X ^ k + C (-↑v) * X ^ m + C (-↑w) * X ^ n
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x) (-↑v) ↑z
h1 : ↑y = -↑v
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
z : QuadraticAlgebra R a b
⊢ { toFun := fun s ↦ QuadraticAlgebra.C ((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
          map_add' := ⋯ }
        s *
      z =
    z *
      { toFun := fun s ↦ QuadraticAlgebra.C ((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
          map_add' := ⋯ }
        s

Tactic:
by ext <;> simp [Algebra.commutes]

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

Goal state before:
pp: case sq_add.inr
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
s✝ a s : R
hs✝ : IsSumSq s
ih : s ≠ 0 → IsSumNonzeroSq s
hs : a * a + s ≠ 0
ne_a : a ≠ 0
⊢ IsSumNonzeroSq (a * a + s)

Tactic:
rcases eq_or_ne s 0 with (rfl | ne_s)
      · simpa using IsSumNonzeroSq.sq ne_a
      · exact IsSumNonzeroSq.sq_add ne_a (ih ne_s)

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
n : ℕ
x✝ : n ∈ Finset.range (P.natDegree + 1)
⊢ (algebraMap (↥R) L) ((int R P hP).coeff n) * x ^ n = P.coeff n • x ^ n

Tactic:
Algebra.smul_def

Goal state after:
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
n : ℕ
x✝ : n ∈ Finset.range (P.natDegree + 1)
⊢ (algebraMap (↥R) L) ((int R P hP).coeff n) * x ^ n = (algebraMap K L) (P.coeff n) * x ^ n
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
g_hom : Type u_3
R : Type u_4
inst✝⁴ : NonAssocSemiring k
inst✝³ : One G
inst✝² : Semiring R
inst✝¹ : FunLike g_hom G R
inst✝ : OneHomClass g_hom G R
f : k →+* R
g : g_hom
⊢ (liftNC ↑f ⇑g) 1 = 1

Tactic:
by
  simp only [one_def, liftNC_single, AddMonoidHom.coe_coe, map_one, mul_one]

Goal state after:
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)
x✝ : ∃ y, y • 1 = star ↑v * ↑u
y : S
h : y • 1 = star ↑v * ↑u
huv : ↑u = y • ↑v
⊢ ↑v = star y • ↑u

Tactic:
simpa [← mul_assoc] using congr(u * (star $h)).symm

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

Goal state before:
pp: case inr.inl
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
hx : x ≤ z
⊢ y ≤ x + z

pp: case inr.inr
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
hx : z ≤ x
⊢ y ≤ x + z

Tactic:
· rwa [add_eq_left hx]

Goal state after:
case inr.inr
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
hx : z ≤ x
⊢ y ≤ x + z
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: case cons
R : Type u_1
inst✝ : LinearOrder R
hd : R
tl : List R
IH : trop tl.minimum = (map (trop ∘ WithTop.some) tl).sum
⊢ trop (hd :: tl).minimum = (map (trop ∘ WithTop.some) (hd :: tl)).sum

Tactic:
simp [List.minimum_cons, ← IH]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : MulOneClass G
R : Type u_3
inst✝ : Semiring R
f : k →+* R
g : G →* R
c : k
φ : SkewMonoidAlgebra k G
⊢ (liftNC ↑f ⇑g) (c • φ) = f c * (liftNC ↑f ⇑g) φ

Tactic:
suffices this :
    (liftNC ↑f g).comp (smulAddHom k (SkewMonoidAlgebra k G) c) =
      (AddMonoidHom.mulLeft (f c)).comp (liftNC ↑f g) by simpa using congr($this φ)
  refine addHom_ext' fun a => AddMonoidHom.ext fun b => ?_
  simp [smul_single, mul_assoc]

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

Goal state before:
pp: R : Type u_5
A : Type u_6
C : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : NonUnitalNonAssocSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
inst✝⁶ : StarRing A
inst✝⁵ : StarModule R A
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : StarAddMonoid C
inst✝¹ : StarModule R C
inst✝ : CoalgebraStruct R C
h : star (toConv comul) = toConv (↑(TensorProduct.comm R C C) ∘ₗ comul)
f g : WithConv (C →ₗ[R] A)
⊢ star (f * g) = star g * star f

Tactic:
simp_rw [convMul_def, intrinsicStar_comp', intrinsicStar_mul', intrinsicStar_map,
    h, comp_assoc, ← comp_assoc _ _ (map _ _), map_comp_comm_eq,
    ← comp_assoc _ (TensorProduct.comm R A A).toLinearMap]
  ext; simp

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

Goal state before:
pp: X✝ X : LocallyRingedSpace
x : ↑↑X.toPresheafedSpace
⊢ IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (𝟙 X.toPresheafedSpace) x))

Tactic:
dsimp; rw [PresheafedSpace.stalkMap.id]; infer_instance

Goal state after:
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T✝ : ↑X → Type u_1
T : ↑X → Type u_2
P : PrelocalPredicate T
U : Opens ↑X
f : (x : ↥U) → T ↑x
w :
  ∀ (x : ↥U),
    ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, ∀ (x : ↥V), ∃ V_1, ∃ (_ : ↑x ∈ V_1), ∃ i_1, P.pred fun x ↦ (fun x ↦ f (i x)) (i_1 x)
x : ↥U
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P.pred fun x ↦ f (i x)

Tactic:
specialize w x
    rcases w with ⟨V, m, i, p⟩
    specialize p ⟨x.1, m⟩
    rcases p with ⟨V', m', i', p'⟩
    exact ⟨V', m', i' ≫ i, p'⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U V : (Opens ↑↑X)ᵒᵖ
i : U ⟶ V
⊢ X.presheaf.map i ≫ X.presheaf.map (eqToHom ⋯) =
    ((X.presheaf.map (eqToHom ⋯) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop U))))) ≫
        Y.presheaf.map ((opensFunctor f).op.map i)) ≫
      f.c.app (op ((opensFunctor f).obj (unop V)))

Tactic:
simp only [Functor.op_obj, op_unop, ← X.presheaf.map_comp, Functor.op_map, Category.assoc,
    NatTrans.naturality, Quiver.Hom.unop_op, IsIso.inv_hom_id_assoc,
    TopCat.Presheaf.pushforward_obj_map]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U V : (Opens ↑↑X)ᵒᵖ
i : U ⟶ V
⊢ X.presheaf.map (i ≫ eqToHom ⋯) =
    X.presheaf.map (eqToHom ⋯ ≫ ((Opens.map f.base).map ((opensFunctor f).map i.unop)).op)
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
g : ↥X → ↥Y
h : ⇑f = g
x : ↥X
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      ({ base := ofHom { toFun := g, continuous_toFun := ⋯ },
            c := f.c ≫ (Presheaf.pushforwardEq ⋯ X.presheaf).hom }.stalkMap
        x))

Tactic:
subst h
    convert! f.prop x using 4
    cat_disch

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : Y.Opens
⊢ ↑(f ''ᵁ f ⁻¹ᵁ U) = ↑(opensRange f ⊓ U)

Tactic:
simp [Set.image_preimage_eq_range_inter]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
R : CommRingCat
f : ↑R
⊢ IsOpenImmersion (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away f))))

Tactic:
apply SheafedSpace.IsOpenImmersion.of_stalk_iso (H := ?_)

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
R : CommRingCat
f : ↑R
⊢ IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (LocallyRingedSpace.Hom.toShHom
              (Hom.toLRSHom (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away f)))))).hom.base)

C : Type u
inst✝ : Category.{v, u} C
R : CommRingCat
f : ↑R
hf✝ :
  IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (LocallyRingedSpace.Hom.toShHom
              (Hom.toLRSHom (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away f)))))).hom.base)
⊢ ∀ (x : ↥(Spec (CommRingCat.of (Localization.Away f)))),
    IsIso
      (PresheafedSpace.Hom.stalkMap
        (LocallyRingedSpace.Hom.toShHom
            (Hom.toLRSHom (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away f)))))).hom
        x)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsOpenImmersion f ∧ Epi f.base ↔ IsIso f.base ∧ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)

Tactic:
IsOpenImmersion.iff_isIso_stalkMap,

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ (IsOpenEmbedding ⇑f ∧ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)) ∧ Epi f.base ↔
    IsIso f.base ∧ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ ∀ (j : WalkingCospan),
    (limit.cone (cospan f.base g.base)).π.app j =
      ((forget C).mapCone (pullbackConeOfLeft f g)).π.app j ≫ (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app j

Tactic:
rintro (_ | _ | _)

Goal state after:
case w.none
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ (limit.cone (cospan f.base g.base)).π.app none =
    ((forget C).mapCone (pullbackConeOfLeft f g)).π.app none ≫ (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app none

case w.some.left
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ (limit.cone (cospan f.base g.base)).π.app (some WalkingPair.left) =
    ((forget C).mapCone (pullbackConeOfLeft f g)).π.app (some WalkingPair.left) ≫
      (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app (some WalkingPair.left)

case w.some.right
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ (limit.cone (cospan f.base g.base)).π.app (some WalkingPair.right) =
    ((forget C).mapCone (pullbackConeOfLeft f g)).π.app (some WalkingPair.right) ≫
      (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app (some WalkingPair.right)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : PresheafedSpace C
Y : SheafedSpace C
f : X ⟶ Y.toPresheafedSpace
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ X.presheaf.IsSheaf

Tactic:
apply TopCat.Presheaf.isSheaf_of_iso (sheafIsoOfIso (isoRestrict f).symm).symm
    apply TopCat.Sheaf.pushforward_sheaf_of_sheaf
    exact (Y.restrict H.base_open).IsSheaf

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

Goal state before:
pp: K : Precoverage Scheme
X✝ Y✝ Z : Scheme
𝒰 : Cover K X✝
f✝ : X✝ ⟶ Z
g : Y✝ ⟶ Z
inst✝³ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f✝) g
P Q : MorphismProperty Scheme
inst✝² : P.ContainsIdentities
inst✝¹ : P.RespectsIso
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
x : ↥Y
⊢ f ((inv f) x) = x

Tactic:
simp [← Hom.comp_apply]

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

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

Tactic:
apply hasLimit_of_iso (diagramIsoCospan _).symm

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

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

Tactic:
apply hasLimit_of_iso (diagramIsoCospan _).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hf : Scheme.Hom.opensRange f = ⊤
⊢ Epi f.base

Tactic:
TopCat.epi_iff_surjective,

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hf : Scheme.Hom.opensRange f = ⊤
⊢ Function.Surjective ⇑f
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : ↑Γ(X, U)
e : f ⁻¹ᵁ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) = X.basicOpen r
⊢ Hom.opensRange f ⊓ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) =
    Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r)

Tactic:
inf_eq_right

Goal state after:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : ↑Γ(X, U)
e : f ⁻¹ᵁ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) = X.basicOpen r
⊢ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) ≤ Hom.opensRange f
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.hom.base
⊢ IsIso f

Tactic:
have : IsIso (forgetToPresheafedSpace.map f) := PresheafedSpace.IsOpenImmersion.to_iso f.hom

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : SheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.hom.base
this : IsIso (forgetToPresheafedSpace.map f)
⊢ IsIso f
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: case intro
X : Scheme
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
H : ∀ (i : 𝒰.I₀), CompactSpace ↥(𝒰.X i)
val✝ : Fintype 𝒰.I₀
⊢ CompactSpace ↥X

Tactic:
← isCompact_univ_iff,

Goal state after:
case intro
X : Scheme
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
H : ∀ (i : 𝒰.I₀), CompactSpace ↥(𝒰.X i)
val✝ : Fintype 𝒰.I₀
⊢ IsCompact Set.univ
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
R : CommRingCat
ι : Type u_1
s : ι → ↑R
hs : Ideal.span (Set.range s) = ⊤
x : ↥(Spec R)
H : ∃ i, s i ∉ x.asIdeal
i : ι := H.choose
this : Set.range (PrimeSpectrum.comap (algebraMap (↑R) (Localization.Away (s i)))) = ↑(PrimeSpectrum.basicOpen (s i))
⊢ x ∈
    Set.range
      ⇑(Spec.map
          (CommRingCat.ofHom
            (algebraMap (↑R)
              (Localization.Away
                (s
                  (have this := H;
                  this.choose))))))

Tactic:
exact (eq_iff_iff.mp congr(x ∈ $this)).mpr H.choose_spec

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
f g : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : U ≤ basicOpen g
hu₂ : U ≤ basicOpen f
⊢ const f g U hu₁ * const g f U hu₂ = 1

Tactic:
rw [const_mul, const_congr rfl (mul_comm g f), const_self]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
⊢ (V.ι ⁻¹ᵁ U).ι ≫ (Iso.refl ↑V).hom = (Scheme.Hom.isoImage V.ι (V.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯

Tactic:
simp [← cancel_mono V.ι]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U V : Y.Opens
e : U ≤ V
⊢ f ∣_ U ≫ Y.homOfLE e = X.homOfLE ⋯ ≫ f ∣_ V

Tactic:
simp [← cancel_mono V.ι]

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)) ⋯
n : ℕ
c : ι →₀ R
hc : (c.sum fun i a ↦ a • b i) = f ^ (n + 1)
⊢ ∃ a, (toBasicOpenₗ R M f) a = s

Tactic:
Finsupp.sum_fintype _ _ (by simp)

Goal state after:
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)) ⋯
n : ℕ
c : ι →₀ R
hc : ∑ i, c i • b i = f ^ (n + 1)
⊢ ∃ a, (toBasicOpenₗ R M f) a = s
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
⊢ PrimeSpectrum.comap (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)) (hV.primeIdealOf ⟨x, hx⟩) =
    hU.primeIdealOf ⟨f x, ⋯⟩

Tactic:
change Spec.map (f.appLE U V hVU) (hV.primeIdealOf ⟨x, hx⟩) = (hU.primeIdealOf ⟨f x, hVU hx⟩)

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
⊢ (Spec.map (Scheme.Hom.appLE f U V hVU)) (hV.primeIdealOf ⟨x, hx⟩) = hU.primeIdealOf ⟨f x, ⋯⟩
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mpr
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
z : ↑(D.V (⟨i, x⟩.fst, ⟨j, y⟩.fst))
e₁ : (ConcreteCategory.hom (D.f i j)) z = (ConcreteCategory.hom (D.f i j)) z
e₂ :
  (ConcreteCategory.hom (D.f j i)) ((ConcreteCategory.hom (D.t i j)) z) =
    (ConcreteCategory.hom (D.f j i)) ((ConcreteCategory.hom (D.t i j)) z)
⊢ (ConcreteCategory.hom (D.ι i)) ((ConcreteCategory.hom (D.f i j)) z) =
    (ConcreteCategory.hom (D.ι j)) ((ConcreteCategory.hom (D.f j i)) ((ConcreteCategory.hom (D.t i j)) z))

Tactic:
D.glue_condition_apply

Goal state after:
case mpr
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
z : ↑(D.V (⟨i, x⟩.fst, ⟨j, y⟩.fst))
e₁ : (ConcreteCategory.hom (D.f i j)) z = (ConcreteCategory.hom (D.f i j)) z
e₂ :
  (ConcreteCategory.hom (D.f j i)) ((ConcreteCategory.hom (D.t i j)) z) =
    (ConcreteCategory.hom (D.f j i)) ((ConcreteCategory.hom (D.t i j)) z)
⊢ (ConcreteCategory.hom (D.ι i)) ((ConcreteCategory.hom (D.f i j)) z) =
    (ConcreteCategory.hom (D.ι i)) ((ConcreteCategory.hom (D.f i j)) z)
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mpr
D : GlueData
i j : D.J
x✝ : ↑D.glued
x : ↑(D.V (i, j))
hx : (ConcreteCategory.hom (D.f i j ≫ D.ι i)) x = x✝
⊢ (ConcreteCategory.hom (D.ι j)) ((ConcreteCategory.hom (D.f j i)) ((ConcreteCategory.hom (D.t i j)) x)) = x✝

Tactic:
D.glue_condition_apply

Goal state after:
case mpr
D : GlueData
i j : D.J
x✝ : ↑D.glued
x : ↑(D.V (i, j))
hx : (ConcreteCategory.hom (D.f i j ≫ D.ι i)) x = x✝
⊢ (ConcreteCategory.hom (D.ι i)) ((ConcreteCategory.hom (D.f i j)) x) = x✝
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case right.right
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
i : (ofOpenSubsets U).J
x : ↑(of α)
hx' : x ∈ U i
hx : (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩ ∈ s
⊢ (ConcreteCategory.hom (fromOpenSubsetsGlue U)) ((ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩) ∈
    Set.range ⇑(ConcreteCategory.hom (U i).inclusion')

Tactic:
rw [ι_fromOpenSubsetsGlue_apply]

Goal state after:
case right.right
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
i : (ofOpenSubsets U).J
x : ↑(of α)
hx' : x ∈ U i
hx : (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩ ∈ s
⊢ (ConcreteCategory.hom (U i).inclusion') ⟨x, hx'⟩ ∈ Set.range ⇑(ConcreteCategory.hom (U i).inclusion')
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : ↑(of α)
hx' : x ∈ U i
⊢ (ConcreteCategory.hom (fromOpenSubsetsGlue U)) ((ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩) ∈ ⋃ i, ↑(U i)

Tactic:
rw [ι_fromOpenSubsetsGlue_apply]

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : ↑(of α)
hx' : x ∈ U i
⊢ (ConcreteCategory.hom (U i).inclusion') ⟨x, hx'⟩ ∈ ⋃ i, ↑(U i)
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 j k : 𝒰.I₀
⊢ t' 𝒰 f g i j k ≫
      pullback.fst (fV 𝒰 f g j k) (fV 𝒰 f g j i) ≫
        pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f k) ≫ pullback.snd (𝒰.f j ≫ f) g =
    pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
      pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ pullback.snd (𝒰.f i ≫ f) g

Tactic:
by
  simp only [t', Category.assoc, pullbackSymmetry_hom_comp_fst_assoc,
    pullbackRightPullbackFstIso_inv_snd_fst_assoc, pullback.lift_fst_assoc, t_fst_snd,
    pullbackRightPullbackFstIso_hom_fst_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case refine_1
σ : Type v
g : σ → Scheme
inst✝ : Small.{u, v} σ
i j : σ
x : ↥(g i)
y : ↥(g j)
⊢ (∃ k fi fj x_1, ((Discrete.functor g).map fi) x_1 = x ∧ ((Discrete.functor g).map fj) x_1 = y) → ⟨i, x⟩ = ⟨j, y⟩

Tactic:
rintro ⟨k, ⟨⟨⟨⟩⟩⟩, ⟨⟨⟨⟩⟩⟩, x, rfl, rfl⟩; simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case a
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
x : ↥X
⊢ coprod.inl x ∈ coprod.map f g ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl

Tactic:
exact ⟨f x, by simp [← Scheme.Hom.comp_apply, -Scheme.Hom.comp_base]⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝³ : Category.{v, w} J
F : J ⥤ Scheme
inst✝² : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝¹ : (F ⋙ forget).IsLocallyDirected
inst✝ : Quiver.IsThin J
i j : J
x : ↥↑(V F i j)
⊢ (tAux F i j) x ∈ Set.range ⇑(V F j i).ι

Tactic:
obtain ⟨l, x, rfl⟩ := (Scheme.Opens.iSupOpenCover _).exists_eq x

Goal state after:
J : Type w
inst✝³ : Category.{v, w} J
F : J ⥤ Scheme
inst✝² : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝¹ : (F ⋙ forget).IsLocallyDirected
inst✝ : Quiver.IsThin J
i j : J
l : (Opens.iSupOpenCover fun i_1 ↦ Hom.opensRange (F.map i_1.snd.1)).I₀
x : ↥((Opens.iSupOpenCover fun i_1 ↦ Hom.opensRange (F.map i_1.snd.1)).X l)
⊢ (tAux F i j) (((Opens.iSupOpenCover fun i_1 ↦ Hom.opensRange (F.map i_1.snd.1)).f l) x) ∈ Set.range ⇑(V F j i).ι
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case inl
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of R))
⊢ ((coprodSpec R S) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) (Sum.inl x))).asIdeal =
    ((PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inl x)).asIdeal

Tactic:
simp only [coprodMk_inl, coprodMk_inr, ← Scheme.Hom.comp_apply,
      coprodSpec, coprod.inl_desc, coprod.inr_desc]

Goal state after:
case inl
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of R))
⊢ ((Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x).asIdeal =
    ((PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inl x)).asIdeal