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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p q : SkewPolynomial R
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
h_add : ∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂
⊢ (p + q).sum f = p.sum f + q.sum f

Tactic:
simp only [sum_def']

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p q : SkewPolynomial R
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
h_add : ∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂
⊢ (SkewMonoidAlgebra.sum (p + q) fun n r ↦ f (toAdd n) r) =
    (SkewMonoidAlgebra.sum p fun n r ↦ f (toAdd n) r) + SkewMonoidAlgebra.sum q fun n r ↦ f (toAdd n) r
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : AddMonoid k
S : Type u_3
inst✝ : SMulZeroClass S k
a : S
b : SkewMonoidAlgebra k G
⊢ (a • b).coeff = a • b.coeff

Tactic:
rw [← ofCoeff_smul]

Goal state after:
Module: Mathlib.Algebra.Symmetrized

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

Tactic:
← mul_add,

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

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

Tactic:
← mul_add,

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

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

Tactic:
← mul_add,

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

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

Tactic:
← mul_add,

Goal state after:
case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ⅟2 * ⅟2 *
      (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
        unsym (a * a) * unsym b * unsym a) =
    ⅟2 *
      (⅟2 *
        (unsym a * (unsym b * unsym (a * a) + unsym (a * a) * unsym b) +
          (unsym b * unsym (a * a) + unsym (a * a) * unsym b) * unsym a))
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 φ)

Goal state after:
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).comp ((smulAddHom k (SkewMonoidAlgebra k G)) c) = (AddMonoidHom.mulLeft (f c)).comp (liftNC ↑f ⇑g)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k✝ : Type u_1
G : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : DistribMulAction R M
α : Type u_6
a : α
k : R
m : M
⊢ (↑(singleAddHom a)).toFun (k • m) = (MonoidHom.id R) k • (↑(singleAddHom a)).toFun m

Tactic:
simp [singleAddHom, smul_single, MonoidHom.id_apply]

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

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
h : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
g' : ↑(X.presheaf.stalk x)
heq : (ConcreteCategory.hom (X.presheaf.germ U x hx)) f * g' = 1
⊢ ∃ V i, ∃ (_ : x ∈ V), IsUnit ((ConcreteCategory.hom (X.presheaf.map i.op)) f)

Tactic:
obtain ⟨V, hxV, g, rfl⟩ := X.presheaf.exists_germ_eq g'

Goal state after:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
h : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : x ∈ V
g : ToType (X.presheaf.obj (op V))
heq : (ConcreteCategory.hom (X.presheaf.germ U x hx)) f * (ConcreteCategory.hom (X.presheaf.germ V x hxV)) g = 1
⊢ ∃ V i, ∃ (_ : x ∈ V), IsUnit ((ConcreteCategory.hom (X.presheaf.map i.op)) f)
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
x x' : ↑X.toTopCat
hxx' : x = x'
⊢ Hom.stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯ = Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap f x'

Tactic:
subst hxx'

Goal state after:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑X.toTopCat
⊢ Hom.stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯ = Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap f x
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
V : Opens ↑↑Y
U : Opens ↑↑X
h : V = (opensFunctor f).obj U
⊢ IsIso (f.c.app (op V))

Tactic:
subst h
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s : PullbackCone f g
U : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
s' : PullbackCone f.base g.base := PullbackCone.mk s.fst.base s.snd.base ⋯
this : limit.lift (cospan f.base g.base) s' ≫ limit.π (cospan f.base g.base) WalkingCospan.right = s.snd.base
| ⇑(ConcreteCategory.hom
        (limit.lift (cospan f.base g.base) s' ≫ limit.π (cospan f.base g.base) WalkingCospan.right)) ⁻¹'
    ↑(⋯.functor.obj (unop U))

Tactic:
dsimp [s']

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s : PullbackCone f g
U : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
s' : PullbackCone f.base g.base := PullbackCone.mk s.fst.base s.snd.base ⋯
this : limit.lift (cospan f.base g.base) s' ≫ limit.π (cospan f.base g.base) WalkingCospan.right = s.snd.base
| ⇑(TopCat.Hom.hom (limit.π (cospan f.base g.base) WalkingCospan.right)) ∘
      ⇑(TopCat.Hom.hom (limit.lift (cospan f.base g.base) (PullbackCone.mk s.fst.base s.snd.base ⋯))) ⁻¹'
    ⇑(ConcreteCategory.hom (pullback.snd f.base g.base)) '' ↑(unop U)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_2
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
x : (Opens ↑↑X)ᵒᵖ
⊢ ((pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst).c ≫ Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf).app
      x =
    s.fst.c.app x

Tactic:
induction x with | op x => ?_
    change ((_ ≫ _) ≫ _ ≫ _) ≫ _ = _
    simp_rw [Category.assoc]
    erw [← s.pt.presheaf.map_comp]
    erw [s.snd.c.naturality_assoc]
    have := congr_app s.condition (op (opensFunctor f |>.obj x))
    dsimp only [comp_c_app, unop_op] at this
    rw [← IsIso.comp_inv_eq] at this
    replace this := reassoc_of% this
    erw [← this, hf.invApp_app_assoc, s.fst.c.naturality_assoc]
    simp [eqToHom_map]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: case mk
Y : Scheme
toLocallyRingedSpace✝ : LocallyRingedSpace
local_affine✝ :
  ∀ (x : ↑toLocallyRingedSpace✝.toTopCat),
    ∃ U R, Nonempty (toLocallyRingedSpace✝.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))
H :
  { toLocallyRingedSpace := toLocallyRingedSpace✝, local_affine := local_affine✝ }.toLocallyRingedSpace =
    Y.toLocallyRingedSpace
⊢ { toLocallyRingedSpace := toLocallyRingedSpace✝, local_affine := local_affine✝ } = Y

Tactic:
cases Y

Goal state after:
case mk.mk
toLocallyRingedSpace✝¹ : LocallyRingedSpace
local_affine✝¹ :
  ∀ (x : ↑toLocallyRingedSpace✝¹.toTopCat),
    ∃ U R, Nonempty (toLocallyRingedSpace✝¹.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))
toLocallyRingedSpace✝ : LocallyRingedSpace
local_affine✝ :
  ∀ (x : ↑toLocallyRingedSpace✝.toTopCat),
    ∃ U R, Nonempty (toLocallyRingedSpace✝.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))
H :
  { toLocallyRingedSpace := toLocallyRingedSpace✝¹, local_affine := local_affine✝¹ }.toLocallyRingedSpace =
    { toLocallyRingedSpace := toLocallyRingedSpace✝, local_affine := local_affine✝ }.toLocallyRingedSpace
⊢ { toLocallyRingedSpace := toLocallyRingedSpace✝¹, local_affine := local_affine✝¹ } =
    { toLocallyRingedSpace := toLocallyRingedSpace✝, local_affine := local_affine✝ }
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✝ : (preservesLimitIso forget (cospan f g)).hom ≫ limit.π (cospan f g ⋙ forget) right = (pullback.snd f g).hom
this :
  (HasLimit.isoOfNatIso (diagramIsoCospan (cospan f g ⋙ forget))).hom ≫
      limit.π (cospan ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr)) right =
    limit.π (cospan f g ⋙ forget) right ≫ (diagramIsoCospan (cospan f g ⋙ forget)).hom.app right
⊢ PresheafedSpace.IsOpenImmersion ((preservesLimitIso forget (cospan f g)).hom ≫ limit.π (cospan f g ⋙ forget) right)

Tactic:
dsimp at this

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this✝ : (preservesLimitIso forget (cospan f g)).hom ≫ limit.π (cospan f g ⋙ forget) right = (pullback.snd f g).hom
this :
  (HasLimit.isoOfNatIso (diagramIsoCospan (cospan f g ⋙ forget))).hom ≫ limit.π (cospan f.hom g.hom) right =
    limit.π (cospan f g ⋙ forget) right ≫ 𝟙 Y.toPresheafedSpace
⊢ PresheafedSpace.IsOpenImmersion ((preservesLimitIso forget (cospan f g)).hom ≫ limit.π (cospan f g ⋙ forget) right)
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✝ : (preservesLimitIso forget (cospan g f)).hom ≫ limit.π (cospan g f ⋙ forget) left = (pullback.fst g f).hom
this :
  (HasLimit.isoOfNatIso (diagramIsoCospan (cospan g f ⋙ forget))).hom ≫
      limit.π (cospan ((cospan g f ⋙ forget).map Hom.inl) ((cospan g f ⋙ forget).map Hom.inr)) left =
    limit.π (cospan g f ⋙ forget) left ≫ (diagramIsoCospan (cospan g f ⋙ forget)).hom.app left
⊢ PresheafedSpace.IsOpenImmersion ((preservesLimitIso forget (cospan g f)).hom ≫ limit.π (cospan g f ⋙ forget) left)

Tactic:
dsimp at this

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this✝ : (preservesLimitIso forget (cospan g f)).hom ≫ limit.π (cospan g f ⋙ forget) left = (pullback.fst g f).hom
this :
  (HasLimit.isoOfNatIso (diagramIsoCospan (cospan g f ⋙ forget))).hom ≫ limit.π (cospan g.hom f.hom) left =
    limit.π (cospan g f ⋙ forget) left ≫ 𝟙 Y.toPresheafedSpace
⊢ PresheafedSpace.IsOpenImmersion ((preservesLimitIso forget (cospan g f)).hom ≫ limit.π (cospan g f ⋙ forget) left)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝¹ : HasColimit F
i : Discrete ι
inst✝ : HasStrictTerminalObjects C
U : Opens ↑↑(F.obj i).toPresheafedSpace
h₁ :
  colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv =
    forgetToPresheafedSpace.map (colimit.ι F i)
h₂ :
  colimit.ι F i =
    { hom := colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv }
⊢ IsIso ((colimit.ι F i).hom.c.app (op (⋯.functor.obj U)))

Tactic:
have H :
      IsOpenEmbedding
        (colimit.ι (F ⋙ SheafedSpace.forgetToPresheafedSpace) i ≫
            (preservesColimitIso SheafedSpace.forgetToPresheafedSpace F).inv).base := by
      have := h₁.symm
      convert! sigma_ι_isOpenEmbedding F i

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝¹ : HasColimit F
i : Discrete ι
inst✝ : HasStrictTerminalObjects C
U : Opens ↑↑(F.obj i).toPresheafedSpace
h₁ :
  colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv =
    forgetToPresheafedSpace.map (colimit.ι F i)
h₂ :
  colimit.ι F i =
    { hom := colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv }
H :
  IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv).base)
⊢ IsIso ((colimit.ι F i).hom.c.app (op (⋯.functor.obj U)))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsLimit
    (PullbackCone.mk
      (SheafedSpace.forgetToPresheafedSpace.map
        (forgetToSheafedSpace.map
          { toHom := PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom, prop := ⋯ }))
      (SheafedSpace.forgetToPresheafedSpace.map (forgetToSheafedSpace.map (Y.ofRestrict ⋯))) ⋯)

Tactic:
exact PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftIsLimit f.1 g.1

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsLimit
    (PullbackCone.mk
      ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map
        { toHom := PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom, prop := ⋯ })
      ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map (Y.ofRestrict ⋯)) ⋯)

Tactic:
exact PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftIsLimit f.1 g.1

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑X.toTopCat
this :
  ⇑(ConcreteCategory.hom (Hom.toShHom f).hom.base) ⁻¹' ⇑(ConcreteCategory.hom (Hom.toShHom f).hom.base) '' U.carrier =
    U.carrier
⊢ (Opens.map f.base).op.obj (op ((opensFunctor f).obj U)) = op U

Tactic:
dsimp at this

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑X.toTopCat
this : ⇑(ConcreteCategory.hom f.base) ⁻¹' ⇑(ConcreteCategory.hom f.base) '' ↑U = ↑U
⊢ (Opens.map f.base).op.obj (op ((opensFunctor f).obj U)) = op U
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑X.toTopCat
this :
  ⇑(ConcreteCategory.hom (Hom.toShHom f).hom.base) ⁻¹' ⇑(ConcreteCategory.hom (Hom.toShHom f).hom.base) '' U.carrier =
    U.carrier
⊢ op U = (Opens.map f.base).op.obj (op ((opensFunctor f).obj U))

Tactic:
dsimp at this

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑X.toTopCat
this : ⇑(ConcreteCategory.hom f.base) ⁻¹' ⇑(ConcreteCategory.hom f.base) '' ↑U = ↑U
⊢ op U = (Opens.map f.base).op.obj (op ((opensFunctor f).obj U))
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
s : Type u_1
X : Scheme
U : s → X.Opens
hU : IsOpenCover U
x : ↥X
hx : x ∈ ⨆ i, U i
⊢ ∃ i, x ∈ Set.range ⇑({ I₀ := s, X := fun i ↦ ↑(U i), f := fun i ↦ (U i).ι }.f i)

Tactic:
Opens.mem_iSup

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
s : Type u_1
X : Scheme
U : s → X.Opens
hU : IsOpenCover U
x : ↥X
hx : ∃ i, x ∈ U i
⊢ ∃ i, x ∈ Set.range ⇑({ I₀ := s, X := fun i ↦ ↑(U i), f := fun i ↦ (U i).ι }.f i)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V W : X.Opens
e₁ : U ≤ V
e₂ : V ≤ W
⊢ X.homOfLE e₁ ≫ X.homOfLE e₂ = X.homOfLE ⋯

Tactic:
← cancel_mono W.ι,

Goal state after:
X : Scheme
U V W : X.Opens
e₁ : U ≤ V
e₂ : V ≤ W
⊢ (X.homOfLE e₁ ≫ X.homOfLE e₂) ≫ W.ι = X.homOfLE ⋯ ≫ W.ι
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
x : ↥X
hx : x ∈ U
⊢ (X.homOfLE e) ⟨x, hx⟩ = ⟨x, ⋯⟩

Tactic:
by
  rw [homOfLE_base]
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case refine_3
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ X.homOfLE hV ∣_ W.ι ⁻¹ᵁ U ≫ (Scheme.Hom.isoImage W.ι (W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom =
    (Scheme.Hom.isoImage V.ι (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯

Tactic:
{ simp [← cancel_mono (Scheme.Opens.ι _)] }

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

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

Tactic:
{ simp [← cancel_mono (Scheme.Opens.ι _)] }

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

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

Tactic:
{ simp [← cancel_mono (Scheme.Opens.ι _)] }

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case refine_6
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ X.homOfLE hV ≫ (Iso.refl ↑W).hom = (Iso.refl ↑V).hom ≫ X.homOfLE hV

Tactic:
{ simp [← cancel_mono (Scheme.Opens.ι _)] }

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
⊢ Opens.IsBasis X.affineOpens

Tactic:
Opens.isBasis_iff_nbhd

Goal state after:
X : Scheme
⊢ ∀ {U : TopologicalSpace.Opens ↥X} {x : ↥X}, x ∈ U → ∃ U' ∈ X.affineOpens, x ∈ U' ∧ U' ≤ U
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
i : ↑(Γ.obj (op X))
x✝ : i ∈ s
⊢ (⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' ↑(basicOpen i))ᶜ = (↑(X.toRingedSpace.basicOpen i))ᶜ

Tactic:
erw [X.toΓSpec_preimage_basicOpen_eq i]

Goal state after:
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
s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
⊢ (f ≫ coequalizer.π f g) ≫ coequalizer.desc s.inl ⋯ = s.inr

Tactic:
by simpa using congr(coprod.inl ≫ $s.condition)

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

Tactic:
change _ = toStalk R x r • TopCat.Presheaf.germ (moduleStructurePresheaf R M).presheaf _ _ _ _

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

Goal state before:
pp: X : Scheme
this : Γ.rightOp.map (ΓSpec.adjunction.unit.app X) ≫ ΓSpec.adjunction.counit.app (Γ.rightOp.obj X) = 𝟙 (Γ.rightOp.obj X)
⊢ Hom.appTop X.toSpecΓ = (ΓSpecIso Γ(X, ⊤)).hom

Tactic:
dsimp at this

Goal state after:
X : Scheme
this : (Hom.appTop X.toSpecΓ).op ≫ (ΓSpecIso Γ(X, ⊤)).inv.op = 𝟙 (op Γ(X, ⊤))
⊢ Hom.appTop X.toSpecΓ = (ΓSpecIso Γ(X, ⊤)).hom
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: R : CommRingCat
this :
  ΓSpec.adjunction.unit.app (Scheme.Spec.obj (op R)) ≫ Scheme.Spec.map (ΓSpec.adjunction.counit.app (op R)) =
    𝟙 (Scheme.Spec.obj (op R))
⊢ Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ

Tactic:
dsimp at this

Goal state after:
R : CommRingCat
this : (Spec R).toSpecΓ ≫ Spec.map (Scheme.ΓSpecIso R).inv = 𝟙 (Spec R)
⊢ Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ
Module: Mathlib.AlgebraicGeometry.AffineScheme

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

Tactic:
have := isLocalization_basicOpen hU f

Goal state after:
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
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v, u₁} C
D : GlueData C
inst✝² : HasMulticoequalizer D.diagram
F : C ⥤ Type v
inst✝¹ : PreservesColimit D.diagram.multispan F
inst✝ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
x : F.obj D.glued
e : F.obj D.glued ≅ (D.mapGlueData F).glued := D.gluedIso F
i : (D.mapGlueData F).J
y : (D.mapGlueData F).U i
eq : (ConcreteCategory.hom (F.map (D.ι i))) y = (ConcreteCategory.hom (𝟙 (F.obj D.glued))) x
⊢ ∃ i y, (ConcreteCategory.hom (F.map (D.ι i))) y = x

Tactic:
exact ⟨i, y, eq⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ PrimeSpectrum.zeroLocus (⋃ i, {↑i}) = ∅ ↔ PrimeSpectrum.zeroLocus ↑(Ideal.span s) = ∅

Tactic:
PrimeSpectrum.zeroLocus_span

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ PrimeSpectrum.zeroLocus (⋃ i, {↑i}) = ∅ ↔ PrimeSpectrum.zeroLocus s = ∅