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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
q' : ι → R[X]
r' : (i : ι) → Fin (n i) → R[X]
hr' : ∀ i ∈ s, ∀ (j : Fin (n i)), (r' i j).degree < (g i).degree
hr : ∀ i ∈ s, r i = q' i * g i ^ n i + ∑ j, r' i j * g i ^ ↑j
⊢ ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k =
    ∑ i ∈ s, q' i * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r' i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k

Tactic:
← Finset.sum_add_distrib

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
q' : ι → R[X]
r' : (i : ι) → Fin (n i) → R[X]
hr' : ∀ i ∈ s, ∀ (j : Fin (n i)), (r' i j).degree < (g i).degree
hr : ∀ i ∈ s, r i = q' i * g i ^ n i + ∑ j, r' i j * g i ^ ↑j
⊢ ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k =
    ∑ x ∈ s, (q' x * ∏ i ∈ s, g i ^ n i + ∑ j, r' x j * g x ^ ↑j * ∏ k ∈ s.erase x, g k ^ n k)
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
x y : R
⊢ y = (x ◃ x) ◃ x ◃⁻¹ y

Tactic:
rw [self_act_act_eq]

Goal state after:
R : Type u_1
inst✝ : Rack R
x y : R
⊢ y = x ◃ x ◃⁻¹ y
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
⊢ ∀ {x y : R}, act' (x ◃ y) = act' x ◃ act' y

Tactic:
by
    intro x y
    exact ad_conj x y

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
x✝ y✝ : EnvelGroup R
x y : PreEnvelGroup R
⊢ Quotient.liftOn (⟦x⟧ * ⟦y⟧) (mapAux f) ⋯ = ⟦x⟧.liftOn (mapAux f) ⋯ * ⟦y⟧.liftOn (mapAux f) ⋯

Tactic:
change Quotient.liftOn ⟦mul x y⟧ (toEnvelGroup.mapAux f) _ = _
          simp [toEnvelGroup.mapAux]

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

Goal state before:
pp: case sq_add
R : Type u_1
inst✝¹ : AddCommMonoid R
inst✝ : Mul R
hz : ∀ {a : R}, a * a = 0 → a = 0
ha : ∀ {s₁ s₂ : R}, IsSumSq s₁ → IsSumSq s₂ → s₁ + s₂ = 0 → s₁ = 0
x b s : R
hb : b ≠ 0
hs : IsSumNonzeroSq s
ih : s ≠ 0
⊢ b * b + s ≠ 0

Tactic:
grind [ha (IsSumSq.mul_self b) hs.isSumSq]

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

Goal state before:
pp: α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
g f₁ f₂ : CentroidHom α
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← comp_apply, h, comp_apply]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Monoid G
inst✝² : Semiring k
inst✝¹ : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst✝ : DecidableEq G
r : k
a : G
⊢ image₂ (fun x1 x2 ↦ x1 * x2) f.support {a} ⊆ image (fun x ↦ x * a) f.support

Tactic:
Finset.image₂_singleton_right

Goal state after:
k : Type u_1
G : Type u_2
inst✝³ : Monoid G
inst✝² : Semiring k
inst✝¹ : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst✝ : DecidableEq G
r : k
a : G
⊢ image (fun a_1 ↦ a_1 * a) f.support ⊆ image (fun x ↦ x * a) f.support
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mk.mk
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
r : R → R → Prop
f : R →+* T
h : ∀ ⦃x y : R⦄, r x y → f x = f y
toQuot✝¹ : Quot (Rel r)
x : R
toQuot✝ : Quot (Rel r)
y : R
⊢ Quot.lift ⇑f ⋯ ({ toQuot := Quot.mk (Rel r) x } + { toQuot := Quot.mk (Rel r) y }).toQuot =
    Quot.lift ⇑f ⋯ { toQuot := Quot.mk (Rel r) x }.toQuot + Quot.lift ⇑f ⋯ { toQuot := Quot.mk (Rel r) y }.toQuot

Tactic:
simp only [add_quot, f.map_add x y]

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
y a b : B
h : r a b
su : a - b = y
⊢ (mkRingHom r) y = 0

Tactic:
← su,

Goal state after:
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
y a b : B
h : r a b
su : a - b = y
⊢ (mkRingHom r) (a - b) = 0
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra S R
inst✝ : Algebra.IsCentral S R
u v : ↥(unitary R)
⊢ (conjStarAlgAut S R) u = (conjStarAlgAut S R) v ↔ ∃ α, ↑u = α • ↑v

Tactic:
by
  conv_lhs => rw [eq_comm]
  simp_rw [StarAlgEquiv.ext_iff, conjStarAlgAut_apply, ← coe_star, star_eq_inv,
    ← val_inv_toUnits_apply, ← val_toUnits_apply, mul_assoc, ← Units.eq_inv_mul_iff_mul_eq,
    ← mul_assoc, Units.eq_mul_inv_iff_mul_eq, mul_assoc, ← mul_assoc (((toUnits v)⁻¹ : Rˣ) : R),
    ← Subalgebra.mem_center_iff (R := S), Algebra.IsCentral.center_eq_bot, Algebra.mem_bot,
    Set.mem_range, Algebra.algebraMap_eq_smul_one, Units.eq_inv_mul_iff_mul_eq, mul_smul_comm,
    mul_one, eq_comm]

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

Goal state before:
pp: R : Type u
inst✝² : LinearOrder R
inst✝¹ : OrderTop R
inst✝ : Zero R
n : ℕ
⊢ untrop (if n + 1 = 0 then 0 else 1) = untrop ((if n = 0 then 0 else 1) + 1)

Tactic:
cases n

Goal state after:
case zero
R : Type u
inst✝² : LinearOrder R
inst✝¹ : OrderTop R
inst✝ : Zero R
⊢ untrop (if 0 + 1 = 0 then 0 else 1) = untrop ((if 0 = 0 then 0 else 1) + 1)

case succ
R : Type u
inst✝² : LinearOrder R
inst✝¹ : OrderTop R
inst✝ : Zero R
n✝ : ℕ
⊢ untrop (if n✝ + 1 + 1 = 0 then 0 else 1) = untrop ((if n✝ + 1 = 0 then 0 else 1) + 1)
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
x : Tropical R
n : ℕ
IH : (n + 1) • x = x
⊢ (n + 1) • x + 1 • x = x

Tactic:
IH,

Goal state after:
case succ
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
x : Tropical R
n : ℕ
IH : (n + 1) • x = x
⊢ x + 1 • x = x
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), a * x = z ↔ a = y
⊢ (f * single x r).coeff z = f.coeff y * y • r

Tactic:
classical
  have A : ∀ a₁ b₁, ((single x r).sum fun a₂ b₂ ↦ ite (a₁ * a₂ = z) (b₁ * a₁ • b₂) 0) =
      ite (a₁ * x = z) (b₁ * a₁ • r) 0 :=
    fun a₁ b₁ ↦ sum_single_index <| by simp
  calc
    (f * (single x r)).coeff z =
        sum f fun a b ↦ if a = y then b * y • r else 0 := by simp [coeff_mul, A, H, sum_ite_eq']
    _ = if y ∈ f.support then f.coeff y * y • r else 0 := (f.support.sum_ite_eq' _ _)
    _ = f.coeff y * y • r := by
      split_ifs with h <;> simp [support] at h <;> simp [h]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
r : k
g : G
x : SkewMonoidAlgebra k G
x✝ : G
a✝ : x✝ ∈ x.coeff.support
h : ∀ (x : G), ¬x✝ * g = x * g
⊢ x.coeff x✝ * x✝ • r = 0

Tactic:
exact False.elim (h _ rfl)

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
U : Opens ↑↑Y
⊢ H.hom.c.app (op U) ≫ (Presheaf.pushforwardToOfIso ((forget C).mapIso H).symm H.inv.c).app (op U) =
    (𝟙 Y.presheaf).app (op U)

Tactic:
simpa using! congr_arg (fun f => f ≫ eqToHom _) (congr_app H.inv_hom_id (op U))

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

Goal state before:
pp: 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
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ limMap (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫
      (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp
            (op
              ((Opens.map
                    (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj
                U))).inv ≫
        (limit.π (pushforwardDiagramToColimit F).leftOp (op j)).app
            (op
              ((Opens.map
                    (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj
                U)) ≫
          (F.obj j).presheaf.map (eqToHom ⋯) ≫
            ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) =
    limit.π (componentwiseDiagram F U) (op j)

Tactic:
limitObjIsoLimitCompEvaluation_inv_π_app_assoc,

Goal state after:
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
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ limMap (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫
      limit.π
          ((pushforwardDiagramToColimit F).leftOp ⋙
            (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj
              (op
                ((Opens.map
                      (colimit.isoColimitCocone
                            { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj
                  U)))
          (op j) ≫
        (F.obj j).presheaf.map (eqToHom ⋯) ≫
          ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) =
    limit.π (componentwiseDiagram F U) (op j)
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
⊢ Function.Bijective
    ((⇑↑(stalkIso (Localization M) x) ∘
        ⇑(Localization.localRingHom (Ideal.comap (algebraMap (↑R) (Localization M)) x.asIdeal) x.asIdeal
            (algebraMap (↑R) (Localization M)) ⋯)) ∘
      ⇑(stalkIso (↑R) (PrimeSpectrum.comap (algebraMap (↑R) (Localization M)) x)).symm)

Tactic:
simp only [EquivLike.bijective_comp]

Goal state after:
R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
⊢ Function.Bijective
    (⇑↑(stalkIso (Localization M) x) ∘
      ⇑(Localization.localRingHom (Ideal.comap (algebraMap (↑R) (Localization M)) x.asIdeal) x.asIdeal
          (algebraMap (↑R) (Localization M)) ⋯))
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 V : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
i : U ⟶ V
⊢ s.snd.c.app (⋯.functor.op.obj U) ≫
      ((TopCat.Presheaf.pushforward C s.snd.base).obj s.pt.presheaf).map (⋯.functor.op.map i) ≫
        s.pt.presheaf.map (eqToHom ⋯) =
    s.snd.c.app (⋯.functor.op.obj U) ≫
      s.pt.presheaf.map (eqToHom ⋯) ≫
        ((TopCat.Presheaf.pushforward C (pullback.lift s.fst.base s.snd.base ⋯)).obj s.pt.presheaf).map i

Tactic:
erw [← s.pt.presheaf.map_comp, ← s.pt.presheaf.map_comp]

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 V : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
i : U ⟶ V
⊢ s.snd.c.app (⋯.functor.op.obj U) ≫
      s.pt.presheaf.map ((Opens.map s.snd.base).op.map (⋯.functor.op.map i) ≫ eqToHom ⋯) =
    s.snd.c.app (⋯.functor.op.obj U) ≫
      s.pt.presheaf.map (eqToHom ⋯ ≫ (Opens.map (pullback.lift s.fst.base s.snd.base ⋯)).op.map i)
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
X : C
R : Presieve X
⊢ R ∈ (Precoverage.comap F Types.jointlySurjectivePrecoverage).coverings X ↔
    ∀ (x : F.obj X), ∃ Y f, R f ∧ x ∈ Set.range ⇑(ConcreteCategory.hom (F.map f))

Tactic:
by
  rw [Precoverage.mem_comap_iff]
  refine ⟨fun h x ↦ ?_, fun h x ↦ ?_⟩
  · obtain ⟨-, -, ⟨hf⟩, hi⟩ := h x
    exact ⟨_, _, hf, hi⟩
  · obtain ⟨Y, g, hg, hi⟩ := h x
    exact ⟨_, _, ⟨hg⟩, hi⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison F f g))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : ∀ (x : (fun X ↦ X) (F.obj S)), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
x : F.obj Y
i : ι
hi : (ConcreteCategory.hom (F.map g)) x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
⊢ ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (p₁ i)))

Tactic:
have : HasPullback g (f i) := (h i).hasPullback

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison F f g))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : ∀ (x : (fun X ↦ X) (F.obj S)), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
x : F.obj Y
i : ι
hi : (ConcreteCategory.hom (F.map g)) x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
this : HasPullback g (f i)
⊢ ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (p₁ i)))
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 ↑↑Y)ᵒᵖ
⊢ s.snd.c.app x ≫
      ((TopCat.Presheaf.pushforward C s.snd.base).obj s.pt.presheaf).map (⋯.adjunction.counit.app (unop x)).op ≫
        s.pt.presheaf.map (eqToHom ⋯) ≫ (Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf).app x =
    s.snd.c.app x

Tactic:
erw [← s.pt.presheaf.map_comp, ← s.pt.presheaf.map_comp]

Goal state after:
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 ↑↑Y)ᵒᵖ
⊢ s.snd.c.app x ≫
      s.pt.presheaf.map
        ((Opens.map s.snd.base).op.map (⋯.adjunction.counit.app (unop x)).op ≫ eqToHom ⋯ ≫ (eqToHom ⋯).app x) =
    s.snd.c.app x
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
as✝ : ι
this✝ :
  colimit.ι (F ⋙ forget C) { as := as✝ } =
    (Discrete.natIsoFunctor.hom.app { as := as✝ } ≫
        colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := as✝ }) ≫
      (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv
this :
  colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := { as := as✝ }.as } =
    TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) { as := as✝ }.as ≫
      (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).inv
⊢ IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        ((((Discrete.natIsoFunctor.hom.app { as := as✝ } ≫ TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) as✝) ≫
              (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).inv) ≫
            (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv) ≫
          (preservesColimitIso (forget C) F).inv))

Tactic:
TopCat.isOpenEmbedding_iff_comp_isIso,

Goal state after:
case mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
as✝ : ι
this✝ :
  colimit.ι (F ⋙ forget C) { as := as✝ } =
    (Discrete.natIsoFunctor.hom.app { as := as✝ } ≫
        colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := as✝ }) ≫
      (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv
this :
  colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := { as := as✝ }.as } =
    TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) { as := as✝ }.as ≫
      (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).inv
⊢ IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (Discrete.natIsoFunctor.hom.app { as := as✝ } ≫ TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) as✝))
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: case h_nhds
X : Scheme
⊢ ∀ (a : ↥X) (u : Set ↥X), a ∈ u → IsOpen u → ∃ v ∈ {x | ∃ a, x = Set.range ⇑(X.affineBasisCover.f a)}, a ∈ v ∧ v ⊆ u

Tactic:
rintro a U haU hU
    rcases X.affineCover.covers a with ⟨x, e⟩
    let U' := (X.affineCover.f (X.affineCover.idx a)) ⁻¹' U
    have hxU' : x ∈ U' := by rw [← e] at haU; exact haU
    rcases PrimeSpectrum.isBasis_basic_opens.exists_subset_of_mem_open hxU'
        ((X.affineCover.f (X.affineCover.idx a)).continuous.isOpen_preimage _
          hU) with
      ⟨_, ⟨_, ⟨s, rfl⟩, rfl⟩, hxV, hVU⟩
    refine ⟨_, ⟨⟨_, s⟩, rfl⟩, ?_, ?_⟩ <;> rw [affineBasisCover_map_range]
    · exact ⟨x, hxV, e⟩
    · rw [Set.image_subset_iff]; exact hVU

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (pullbackRestrictIsoRestrict f U).inv ≫ pullback.fst f U.ι ≫ f = (f ⁻¹ᵁ U).ι ≫ f

Tactic:
pullbackRestrictIsoRestrict_inv_fst_assoc

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (f ⁻¹ᵁ U).ι ≫ f = (f ⁻¹ᵁ U).ι ≫ f
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
n : ↥U → ↥U → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
⊢ ∃ ι x a b,
    ∃ (ibU : ∀ (i : ι), basicOpen (b i) ≤ U),
      U ≤ ⨆ i, basicOpen (b i) ∧
        (∀ (i j : ι), b j • a i = b i • a j) ∧
          ∀ (i : ι),
            (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s =
              const (a i) (b i) (basicOpen (b i)) ⋯

Tactic:
obtain ⟨t, ht⟩ := hU.elim_finite_subcover (fun i ↦ (basicOpen (g i) : Set (PrimeSpectrum R)))
    (fun _ ↦ (basicOpen _).2) (fun x hx ↦ Set.mem_iUnion_of_mem ⟨x, hx⟩ (hxg _))

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
n : ↥U → ↥U → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : ↑U ⊆ ⋃ i ∈ t, ↑(basicOpen (g i))
⊢ ∃ ι x a b,
    ∃ (ibU : ∀ (i : ι), basicOpen (b i) ≤ U),
      U ≤ ⨆ i, basicOpen (b i) ∧
        (∀ (i j : ι), b j • a i = b i • a j) ∧
          ∀ (i : ι),
            (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s =
              const (a i) (b i) (basicOpen (b i)) ⋯
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case e_a
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
⊢ ((f ≫ g) ⁻¹ᵁ U).ι ≫ f = (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.fst f (g ⁻¹ᵁ U).ι ≫ f

Tactic:
pullbackRestrictIsoRestrict_inv_fst_assoc

Goal state after:
case e_a
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
⊢ ((f ≫ g) ⁻¹ᵁ U).ι ≫ f = (f ⁻¹ᵁ g ⁻¹ᵁ U).ι ≫ f
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
W : Opens ↥↑V
⊢ (Scheme.Hom.isoImage U.ι (X.homOfLE e ⁻¹ᵁ W)).inv ≫ X.homOfLE e ∣_ W = X.homOfLE ⋯ ≫ (Scheme.Hom.isoImage V.ι W).inv

Tactic:
simp [← cancel_mono (V.ι.isoImage W).hom, morphismRestrict_homOfLE_isoImage_ι_hom]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
⊢ f ∣_ U.ι ''ᵁ V ≫ (Scheme.Hom.isoImage U.ι V).inv =
    (X.homOfLE ⋯ ≫ (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)).inv) ≫ f ∣_ U ∣_ V

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

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
⊢ f ∣_ U ∣_ V ≫ (Scheme.Hom.isoImage U.ι V).hom =
    ((Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)).hom ≫ X.homOfLE ⋯) ≫ f ∣_ U.ι ''ᵁ V

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

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
⊢ Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V ⋯ = Scheme.Hom.appTop (Scheme.Hom.resLE f U V e) ≫ X.presheaf.map (eqToHom ⋯)

Tactic:
Scheme.Hom.appTop,

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
⊢ Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V ⋯ = Scheme.Hom.app (Scheme.Hom.resLE f U V e) ⊤ ≫ X.presheaf.map (eqToHom ⋯)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U V : X.Opens
h : U ≤ V
⊢ ((↑U).toSpecΓ ≫ Spec.map U.topIso.inv) ≫ Spec.map (X.presheaf.map (homOfLE h).op) =
    X.homOfLE h ≫ (↑V).toSpecΓ ≫ Spec.map V.topIso.inv

Tactic:
simp [← Spec.map_comp, ← X.presheaf.map_comp, toSpecΓ_naturality_assoc]

Goal state after: