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

Goal state before:
pp: 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✝ : Algebra S R
r✝ : R → R → Prop
r : S
⊢ ∀ (x : RingQuot r✝),
    r • x =
      { toFun := fun r ↦ { toQuot := Quot.mk (Rel r✝) ((algebraMap S R) r) }, map_one' := ⋯, map_mul' := ⋯,
            map_zero' := ⋯, map_add' := ⋯ }
          r *
        x

Tactic:
rintro ⟨⟨a⟩⟩
    simp [smul_quot, Algebra.smul_def, mul_quot]

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

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : IsOrderedModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
⊢ star (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) = 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁

Tactic:
simp only [star_add, star_sub, star_mul, star_ofNat, T.A₀_sa, T.A₁_sa, T.B₀_sa,
        T.B₁_sa, mul_comm B₀, mul_comm B₁]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
y : FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ := (lift R) (MulOpposite.op ∘ ι R)
r✝ : R
⊢ MulOpposite.unop (y (MulOpposite.unop (y ((algebraMap R (FreeAlgebra R X)) r✝)))) =
    (algebraMap R (FreeAlgebra R X)) r✝

Tactic:
simp only [AlgHom.commutes, MulOpposite.algebraMap_apply, MulOpposite.unop_op]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
r : R
⊢ (monomial (n + 1)) (r * (⇑φ)^[n] 1) = (monomial (n + 1)) r

Tactic:
iterate_map_one,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
r : R
⊢ (monomial (n + 1)) (r * 1) = (monomial (n + 1)) r
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
a : R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
⊢ (monomial (n + 1)) (a * (⇑φ)^[n] 1) = (monomial (n + 1)) a

Tactic:
iterate_map_one,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
a : R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
⊢ (monomial (n + 1)) (a * 1) = (monomial (n + 1)) a
Module: Mathlib.Algebra.Star.TransferInstance

Goal state before:
pp: R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : AddMonoid S
inst✝ : StarAddMonoid S
⊢ StarAddMonoid R

Tactic:
by
  let := e.star
  let := e.addMonoid
  apply e.injective.starAddMonoid <;> (intros; exact e.apply_symm_apply _)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : StarRing S
this : Star R := e.star
⊢ StarRing R

Tactic:
let := e.nonUnitalNonAssocSemiring

Goal state after:
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : StarRing S
this✝ : Star R := e.star
this : NonUnitalNonAssocSemiring R := e.nonUnitalNonAssocSemiring
⊢ StarRing R
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: R : Type u_1
inst✝ : AddCommMonoid R
s : Multiset (Tropical R)
⊢ ∀ (a : List (Tropical R)), untrop (prod ⟦a⟧) = (map untrop ⟦a⟧).sum

Tactic:
by simpa using List.untrop_prod

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

Goal state before:
pp: 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
⊢ X.presheaf.stalk x = X.presheaf.stalk ((ConcreteCategory.hom (α ≫ β).base) x)

Tactic:
h_eq

Goal state after:
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
⊢ X.presheaf.stalk x = X.presheaf.stalk x
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: case w
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)
F : J ⥤ PresheafedSpace C
j j' : J
f : j ⟶ j'
⊢ (F.map f ≫
        { base := colimit.ι (F ⋙ forget C) j', c := limit.π (pushforwardDiagramToColimit F).leftOp (op j') }).base =
    ({ base := colimit.ι (F ⋙ forget C) j, c := limit.π (pushforwardDiagramToColimit F).leftOp (op j) } ≫
        ((Functor.const J).obj (colimit F)).map f).base

Tactic:
ext x
          exact colimit.w_apply (F ⋙ PresheafedSpace.forget C) f x

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

Goal state before:
pp: case h
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
s : Cocone F
j : J
U : Opens ↑↑s.pt
⊢ (((colimitCocone F).ι.app j ≫ desc F s).c ≫ whiskerRight (eqToHom ⋯) (F.obj j).presheaf).app (op U) =
    (s.ι.app j).c.app (op U)

Tactic:
simp only [op_obj, desc, descCApp, Presheaf.comp_app, comp_c_app, colimitCocone_ι_app_c, assoc]
    rw [limitObjIsoLimitCompEvaluation_inv_π_app_assoc]
    simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case refine_2
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
x : ↥X
H : ∀ f ∈ s, x ∉ X.basicOpen f
f : ↑Γ(X, U)
⊢ ∀ (x_1 y : ↑Γ(X, U)),
    x_1 ∈ Submodule.span (↑Γ(X, U)) s →
      y ∈ Submodule.span (↑Γ(X, U)) s → x ∉ X.basicOpen x_1 → x ∉ X.basicOpen y → x ∉ X.basicOpen (x_1 + y)

Tactic:
exact fun a b _ _ ha hb H ↦ (X.basicOpen_add_le a b H).elim ha hb

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
ι : Type u_1
f : ι → Set ↑Γ(X, U)
⊢ X.zeroLocus (⋃ i, f i) = ⋂ i, X.zeroLocus (f i)

Tactic:
simpa [zeroLocus, AlgebraicGeometry.RingedSpace.zeroLocus] using Set.iInter_comm _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U V : X.Opens
h : U = V
W : (Spec Γ(X, V)).Opens
⊢ Hom.app (Spec.map (X.presheaf.map (eqToHom h).op)) W = eqToHom ⋯

Tactic:
have : Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 _ := by
    rw [X.presheaf.map_id, op_id, Scheme.Spec.map_id]

Goal state after:
X : Scheme
U V : X.Opens
h : U = V
W : (Spec Γ(X, V)).Opens
this : Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
⊢ Hom.app (Spec.map (X.presheaf.map (eqToHom h).op)) W = eqToHom ⋯
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: case refine_1
X : Type u
ι : Type u_1
Y : ι → Type u
f : (i : ι) → Y i ⟶ X
h : Presieve.ofArrows Y f ∈ jointlySurjectivePrecoverage.coverings X
x : (fun X ↦ X) X
⊢ ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (f i))

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
⊢ ∃ Y_1 g, Presieve.ofArrows Y f g ∧ x ∈ Set.range ⇑(ConcreteCategory.hom g)

Tactic:
· obtain ⟨Y, g, ⟨i⟩, hx⟩ := h x
    use i

Goal state after:
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
⊢ ∃ Y_1 g, Presieve.ofArrows Y f g ∧ x ∈ Set.range ⇑(ConcreteCategory.hom g)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑g '' Set.range ⇑(pullback.snd f g) = Set.range ⇑f ∩ Set.range ⇑g

Tactic:
range_pullbackSnd,

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑g '' ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) = Set.range ⇑f ∩ Set.range ⇑g
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 : ↥X
⊢ ∃ y, x ∈ Set.range ⇑(𝒰.f (Cover.idx 𝒰 ↑y))

Tactic:
have h' : x ∈ (⊤ : Set X) := trivial

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
x : ↥X
h' : x ∈ ⊤
⊢ ∃ y, x ∈ Set.range ⇑(𝒰.f (Cover.idx 𝒰 ↑y))
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
⊢ (Opens.map f.base).op.obj (op ((opensFunctor f).obj U)) = op U

Tactic:
have := Set.preimage_image_eq U.1 H.base_open.injective

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 (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
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
⊢ op U = (Opens.map f.base).op.obj (op ((opensFunctor f).obj U))

Tactic:
have := Set.preimage_image_eq U.1 H.base_open.injective

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 (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))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
inst✝ : Epi f.base
this : Epi (forgetToSheafedSpace.map f).hom.base
⊢ IsIso (forgetToSheafedSpace.map f)

Tactic:
apply SheafedSpace.IsOpenImmersion.to_iso

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
W : (↑U).Opens
e : W ≤ U.ι ⁻¹ᵁ V
⊢ Hom.appLE U.ι V W e = X.presheaf.map (homOfLE ⋯).op

Tactic:
simp only [Hom.appLE, ι_app, toScheme_presheaf_map, Quiver.Hom.unop_op,
    Hom.opensFunctor_map_homOfLE, ← Functor.map_comp]

Goal state after:
X : Scheme
U V : X.Opens
W : (↑U).Opens
e : W ≤ U.ι ⁻¹ᵁ V
⊢ X.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op) = X.presheaf.map (homOfLE ⋯).op
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 t : LocalizedModule.Away f M
⊢ (toBasicOpenₗ R M f) s = (toBasicOpenₗ R M f) t → s = t

Tactic:
h_eq

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
s t : LocalizedModule.Away f M
h_eq : (toBasicOpenₗ R M f) s = (toBasicOpenₗ R M f) t
⊢ s = t
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
⊢ (ConcreteCategory.hom (localizationtoStalkₗ R M x)) (LocalizedModule.mk f s) =
    (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ (basicOpen ↑s) x ⋯)) (const f (↑s) (basicOpen ↑s) ⋯)

Tactic:
by
  apply ((Module.End.isUnit_iff _).mp (isUnit_toStalkₗ' _ s.1 s.2)).1 ?_
  dsimp [localizationtoStalkₗ]
  rw [← map_smul, LocalizedModule.smul'_mk, ← Submonoid.smul_def, LocalizedModule.mk_cancel,
    ← LocalizedModule.mkLinearMap_apply, IsLocalizedModule.lift_apply, ← map_smul,
    ← toOpenₗ_germ (basicOpen ↑s) _ s.2, smul_const]
  dsimp [toOpenₗ]
  congr 1
  exact const_eq_const_of_smul_eq_smul (H := by simp) ..

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
r : ↑Γ(X, ⊤)
⊢ IsAffineOpen ((X.basicOpen r).ι ⁻¹ᵁ U)

Tactic:
apply (X.basicOpen r).ι.isAffineOpen_iff_of_isOpenImmersion.mp

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
r : ↑Γ(X, ⊤)
⊢ IsAffineOpen ((X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U)
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)
m : M
α : stalk (moduleStructurePresheaf R M).presheaf x ≅
  (forget₂ (ModuleCat R) Ab).obj ((structurePresheafInModuleCat R M).stalk x) :=
  Limits.colimit.isoColimitCocone
    {
      cocone :=
        (forget₂ (ModuleCat R) Ab).mapCocone
          (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)),
      isColimit :=
        Limits.isColimitOfPreserves (forget₂ (ModuleCat R) Ab)
          (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)) }
this :
  germ (moduleStructurePresheaf R M).presheaf ⊤ x ⋯ ≫ α.hom =
    (forget₂ (ModuleCat R) Ab).map ((structurePresheafInModuleCat R M).germ ⊤ x ⋯)
⊢ (ConcreteCategory.hom α.hom) ((toStalkₗ R M x) m) = (ModuleCat.Hom.hom (toStalkₗ' R M x)) m

Tactic:
exact congr($this _)

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: R : CommRingCatᵒᵖ
⊢ IsIso (adjunction.counit.app R)

Tactic:
adjunction_counit_app

Goal state after:
R : CommRingCatᵒᵖ
⊢ IsIso (Scheme.ΓSpecIso (unop R)).inv.op
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
⊢ D.t i j ≫ D.t j i = 𝟙 (D.V (i, j))

Tactic:
have eq : (pullbackSymmetry (D.f i i) (D.f i j)).hom =
      pullback.snd _ _ ≫ inv (pullback.fst _ _) := by simp

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
eq :
  (pullbackSymmetry (D.f i i) (D.f i j)).hom = pullback.snd (D.f i i) (D.f i j) ≫ inv (pullback.fst (D.f i j) (D.f i i))
⊢ D.t i j ≫ D.t j i = 𝟙 (D.V (i, j))
Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers

Goal state before:
pp: X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : ⇑(hom f) ⁻¹' U = ⇑(hom g) ⁻¹' U
lem : ∀ (x y : (fun X ↦ X) Y), Function.Coequalizer.Rel (⇑(hom f)) (⇑(hom g)) x y → (x ∈ U ↔ y ∈ U)
⊢ ⇑(hom π) ⁻¹' ⇑(hom π) '' U = U

Tactic:
have eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U := by
    aesop (add safe constructors _root_.Equivalence)

Goal state after:
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : ⇑(hom f) ⁻¹' U = ⇑(hom g) ⁻¹' U
lem : ∀ (x y : (fun X ↦ X) Y), Function.Coequalizer.Rel (⇑(hom f)) (⇑(hom g)) x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y ↦ x ∈ U ↔ y ∈ U
⊢ ⇑(hom π) ⁻¹' ⇑(hom π) '' U = U
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
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
r : R
m : (structureSheafInType R M).obj.obj (op U)
x✝ : ↥(unop (op V))
⊢ ↑⟨comapFun f U V hUV ↑(r • m), ⋯⟩ x✝ = ↑(σ r • ⟨comapFun f U V hUV ↑m, ⋯⟩) x✝

Tactic:
by
    dsimp [comapFun]
    rw [map_smulₛₗ, ← IsScalarTower.algebraMap_smul S]

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
x y : ↑(∐ D.U)
h :
  (ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) x =
    (ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) y
diagram : WalkingParallelPair ⥤ Type u := parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap ⋙ forget TopCat
this✝ : (ConcreteCategory.hom (colimit.ι diagram one)) x = (ConcreteCategory.hom (colimit.ι diagram one)) y
this :
  (ConcreteCategory.hom
        (colimit.ι diagram one ≫
          colim.map (diagramIsoParallelPair diagram).hom ≫
            (colimit.isoColimitCocone
                (Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left)
                  (diagram.map WalkingParallelPairHom.right))).hom))
      x =
    (ConcreteCategory.hom
        (colimit.ι diagram one ≫
          colim.map (diagramIsoParallelPair diagram).hom ≫
            (colimit.isoColimitCocone
                (Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left)
                  (diagram.map WalkingParallelPairHom.right))).hom))
      y
⊢ Relation.EqvGen
    (Function.Coequalizer.Rel ⇑(ConcreteCategory.hom D.diagram.fstSigmaMap)
      ⇑(ConcreteCategory.hom D.diagram.sndSigmaMap))
    x y

Tactic:
simp only [eqToHom_refl, colimit.ι_map_assoc, diagramIsoParallelPair_hom_app,
    colimit.isoColimitCocone_ι_hom, Category.id_comp] at this

Goal state after:
D : GlueData
x y : ↑(∐ D.U)
h :
  (ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) x =
    (ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) y
diagram : WalkingParallelPair ⥤ Type u := parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap ⋙ forget TopCat
this✝ : (ConcreteCategory.hom (colimit.ι diagram one)) x = (ConcreteCategory.hom (colimit.ι diagram one)) y
this :
  (ConcreteCategory.hom
        ((Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left)
                  (diagram.map WalkingParallelPairHom.right)).cocone.ι.app
          one))
      x =
    (ConcreteCategory.hom
        ((Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left)
                  (diagram.map WalkingParallelPairHom.right)).cocone.ι.app
          one))
      y
⊢ Relation.EqvGen
    (Function.Coequalizer.Rel ⇑(ConcreteCategory.hom D.diagram.fstSigmaMap)
      ⇑(ConcreteCategory.hom D.diagram.sndSigmaMap))
    x y
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i : D.J
U : Opens ↑(D.U i)
j : D.J
⊢ IsOpen (⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' ↑U)

Tactic:
preimage_image_eq_image

Goal state after:
D : GlueData
i : D.J
U : Opens ↑(D.U i)
j : D.J
⊢ IsOpen (⇑(ConcreteCategory.hom (D.f j i)) '' ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' ↑U)
Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ coprod.inr ≫ (zeroCoprodIso X).hom = 𝟙 X

Tactic:
dsimp [zeroCoprodIso, binaryCofanZeroLeft]
  simp

Goal state after:
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.snd (fV 𝒰 f g j k) (fV 𝒰 f g j i) ≫ pullback.snd (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i) =
    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.fst (𝒰.f i ≫ f) g

Tactic:
by
  simp only [t', Category.assoc, pullbackSymmetry_hom_comp_snd_assoc,
    pullbackRightPullbackFstIso_inv_fst_assoc, pullback.lift_fst_assoc, t_snd,
    pullbackRightPullbackFstIso_hom_fst_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
⊢ IsOpenImmersion coprod.inr

Tactic:
← ι_right_coprodIsoSigma_inv

Goal state after:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
⊢ IsOpenImmersion
    (Sigma.ι (fun i ↦ WalkingPair.casesOn i.down X Y) { down := WalkingPair.right } ≫ (coprodIsoSigma X Y).inv)
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
inst✝ : Small.{u, w} J
i j k : Shrink.{u, w} J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by simp [t]

Goal state after:
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✝
s : PullbackCone f✝ g✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
x : ↥(pullback f g)
i : (Cover.ulift 𝒰).I₀
⊢ pullback.map ((Cover.ulift 𝒰).f i ≫ f) g f g ((Cover.ulift 𝒰).f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ =
    (Iso.refl (pullback ((Cover.ulift 𝒰).f i ≫ f) g)).hom ≫
      (Cover.pushforwardIso (gluing (Cover.ulift 𝒰) f g).openCover
            (limit.isoLimitCone
                { cone := PullbackCone.mk (p1 (Cover.ulift 𝒰) f g) (p2 (Cover.ulift 𝒰) f g) ⋯,
                  isLimit := gluedIsLimit (Cover.ulift 𝒰) f g }).inv).f
        ((Equiv.refl (Cover.ulift 𝒰).I₀) i)

Tactic:
by
        simp_rw [Cover.pushforwardIso_I₀, Cover.pushforwardIso_f, GlueData.openCover_f,
          GlueData.openCover_I₀, gluing_J]
        exact pullback.hom_ext (by simp [p1]) (by simp [p2])

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
H : P g
i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀
e : pullback (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≅
  pullback (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g) :=
  pullbackSymmetry (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≪≫
    pullbackRightPullbackFstIso f g ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≪≫
      asIso
          (pullback.map ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i ≫ f) g
            (pullback.snd f (S.affineCover.f i) ≫ S.affineCover.f i) g
            (𝟙 ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i)) (𝟙 Y) (𝟙 S) ⋯ ⋯) ≪≫
        (pullbackRightPullbackFstIso (S.affineCover.f i) g (pullback.snd f (S.affineCover.f i))).symm
this✝ :
  e.hom ≫ pullback.fst (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g) =
    pullback.snd (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i)
this : Q.IsLocal := isLocal_affineProperty P
⊢ Q (pullback.snd g (S.affineCover.f i))

Tactic:
apply of_isPullback (.of_hasPullback _ _) H

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
e : X ⟶ Y
inst✝ : Surjective e
hge : e ≫ g = f
⊢ Set.range ⇑f = Set.range ⇑g

Tactic:
← hge

Goal state after:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
e : X ⟶ Y
inst✝ : Surjective e
hge : e ≫ g = f
⊢ Set.range ⇑(e ≫ g) = Set.range ⇑g
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y S X' Y' S' : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝² : IsOpenImmersion i₁
inst✝¹ : IsOpenImmersion i₂
inst✝ : Mono i₃
⊢ IsOpenImmersion (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)

Tactic:
pullback_map_eq_pullbackFstFstIso_inv

Goal state after:
X Y S X' Y' S' : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝² : IsOpenImmersion i₁
inst✝¹ : IsOpenImmersion i₂
inst✝ : Mono i₃
⊢ IsOpenImmersion
    ((pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).inv ≫
      pullback.snd (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂) ≫
        pullback.fst (pullback.snd f' g') i₂)