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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
hf :
  (algebraMap R[X] K) q₁ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₁ i j) * gi i ^ (↑j + 1) =
    (algebraMap R[X] K) q₂ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₂ i j) * gi i ^ (↑j + 1)
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ gi i ^ n i * (algebraMap R[X] K) (g i) ^ n i * (algebraMap R[X] K) (g i) ^ ↑j = (algebraMap R[X] K) (g i) ^ ↑j

Tactic:
← mul_pow,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
hf :
  (algebraMap R[X] K) q₁ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₁ i j) * gi i ^ (↑j + 1) =
    (algebraMap R[X] K) q₂ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₂ i j) * gi i ^ (↑j + 1)
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ (gi i * (algebraMap R[X] K) (g i)) ^ n i * (algebraMap R[X] K) (g i) ^ ↑j = (algebraMap R[X] K) (g i) ^ ↑j
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: case sq
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
s₁ s₂ : R
h₂ : IsSumNonzeroSq s₂
a✝ : R
ha✝ : a✝ ≠ 0
⊢ IsSumNonzeroSq (a✝ * a✝ + s₂)

Tactic:
simp_all [sq_add, add_assoc]

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

Goal state before:
pp: case sq_add
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
s₁ s₂ : R
h₂ : IsSumNonzeroSq s₂
a✝ s✝ : R
ha✝ : a✝ ≠ 0
hs✝ : IsSumNonzeroSq s✝
hs_ih✝ : IsSumNonzeroSq (s✝ + s₂)
⊢ IsSumNonzeroSq (a✝ * a✝ + s✝ + s₂)

Tactic:
simp_all [sq_add, add_assoc]

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
f g : CentroidHom α
h : (fun f ↦ (↑f.toAddMonoidHom).toFun) f = (fun f ↦ (↑f.toAddMonoidHom).toFun) g
⊢ f = g

Tactic:
cases f
    cases g
    congr with x
    exact congrFun h x

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R✝ : Type u_4
α : Type u_5
inst✝¹⁶ : NonUnitalNonAssocSemiring α
inst✝¹⁵ : Monoid M
inst✝¹⁴ : Monoid N
inst✝¹³ : Semiring R✝
inst✝¹² : DistribMulAction M α
inst✝¹¹ : SMulCommClass M α α
inst✝¹⁰ : IsScalarTower M α α
inst✝⁹ : DistribMulAction N α
inst✝⁸ : SMulCommClass N α α
inst✝⁷ : IsScalarTower N α α
inst✝⁶ : Module R✝ α
inst✝⁵ : SMulCommClass R✝ α α
inst✝⁴ : IsScalarTower R✝ α α
R : Type u_6
inst✝³ : CommSemiring «R»
inst✝² : Module «R» α
inst✝¹ : SMulCommClass «R» α α
inst✝ : IsScalarTower «R» α α
f g : ↥(Subsemiring.center (CentroidHom α))
h : (fun f ↦ (↑(↑f).toAddMonoidHom).toFun) f = (fun f ↦ (↑(↑f).toAddMonoidHom).toFun) g
⊢ f = g

Tactic:
cases f
    cases g
    congr with x
    exact congrFun h x

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
A : Type u_4
inst✝³ : Semiring A
inst✝² : Algebra k A
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : G →* A
a : G
b : k
⊢ (liftNC ↑(algebraMap k A) ⇑F) (single a b) = b • F a

Tactic:
liftNC_single,

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
A : Type u_4
inst✝³ : Semiring A
inst✝² : Algebra k A
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : G →* A
a : G
b : k
⊢ ↑(algebraMap k A) b * F a = b • F a
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
x✝ : RingQuot r
n : ℕ
a✝ : Quot (Rel r)
a b : R
h : Rel r a b
⊢ Quot.mk (Rel r) (a ^ n) = Quot.mk (Rel r) (b ^ n)

Tactic:
by
      -- note we can't define a `Rel.pow` as `Rel` isn't reflexive so `Rel r 1 1` isn't true
      induction n with
      | zero => rw [pow_zero, pow_zero]
      | succ n ih =>
        simpa +instances [pow_succ, (· * ·), instMul, Quot.map₂_mk, mk.injEq] using
          congr_arg₂ (fun x y ↦ (⟨x⟩ : RingQuot r) * ⟨y⟩) ih (Quot.sound h)

Goal state after:
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✝ : Semiring T
r : R → R → Prop
F : RingQuot r →+* T
⊢ (fun f ↦ preLift ⋯) ((fun F ↦ ⟨F.comp (mkRingHom r), ⋯⟩) F) = F

Tactic:
simp only [preLift_def]
      ext
      simp only [mkRingHom_def, RingHom.coe_comp, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
        Function.comp_apply]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
⊢ (ringQuotToIdealQuotient r) ((mkRingHom r) x) = (Ideal.Quotient.mk (Ideal.ofRel r)) x

Tactic:
simp_rw [ringQuotToIdealQuotient, lift_def, preLift_def, mkRingHom_def]
  rfl

Goal state after:
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✝ : Semiring T
s : A → A → Prop
x✝ : S
⊢ (↑↑(mkRingHom s)).toFun ((algebraMap S A) x✝) = (algebraMap S (RingQuot s)) x✝

Tactic:
simp [mkRingHom_def]; rfl

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ (((monomial 1) 1).sum fun a₁ b₁ ↦ p.sum fun a₂ b₂ ↦ (monomial (a₁ + a₂)) (b₁ * (⇑φ)^[a₁] b₂)) =
    (p.sum fun a b ↦ (monomial a) (φ b)).sum fun a₁ b₁ ↦
      ((monomial 1) 1).sum fun a₂ b₂ ↦ (monomial (a₁ + a₂)) (b₁ * (⇑φ)^[a₁] b₂)

Tactic:
sum_monomial_index (by simp),

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ (p.sum fun a₂ b₂ ↦ (monomial (1 + a₂)) (1 * (⇑φ)^[1] b₂)) =
    (p.sum fun a b ↦ (monomial a) (φ b)).sum fun a₁ b₁ ↦
      ((monomial 1) 1).sum fun a₂ b₂ ↦ (monomial (a₁ + a₂)) (b₁ * (⇑φ)^[a₁] b₂)
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
n : ℕ
a : R
inst✝ : DecidableEq R
⊢ Finset.map toAdd.toEmbedding
      (if a = 0 then (SkewMonoidAlgebra.support p).erase (ofAdd n)
      else insert (ofAdd n) (SkewMonoidAlgebra.support p)) =
    if a = 0 then (Finset.map toAdd.toEmbedding (SkewMonoidAlgebra.support p)).erase n
    else insert n (Finset.map toAdd.toEmbedding (SkewMonoidAlgebra.support p))

Tactic:
split_ifs <;> simp

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddMonoid k
p q : SkewMonoidAlgebra k G
⊢ p = q ↔ ∀ (n : G), p.coeff n = q.coeff n

Tactic:
by
  rcases p with ⟨f : G →₀ k⟩
  rcases q with ⟨g : G →₀ k⟩
  simpa [coeff] using DFunLike.ext_iff (f := f) (g := g)

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : Mul G
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : NonAssocSemiring k
inst✝² : SMul G k
g_hom : Type u_4
inst✝¹ : FunLike g_hom G R
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : SkewMonoidAlgebra k G
h_comm : ∀ {x y : G}, y ∈ a.support → f (y • b.coeff x) * g y = g y * f (b.coeff x)
⊢ (a.sum fun a b_1 ↦ b.sum fun a_1 b ↦ (liftNC ↑f ⇑g) (single (a * a_1) (b_1 * a • b))) =
    (a.sum fun a b ↦ (liftNC ↑f ⇑g) (single a b)) * b.sum fun a b ↦ (liftNC ↑f ⇑g) (single a b)

Tactic:
liftNC_single,

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁵ : Mul G
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : NonAssocSemiring k
inst✝² : SMul G k
g_hom : Type u_4
inst✝¹ : FunLike g_hom G R
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : SkewMonoidAlgebra k G
h_comm : ∀ {x y : G}, y ∈ a.support → f (y • b.coeff x) * g y = g y * f (b.coeff x)
⊢ (a.sum fun a b_1 ↦ b.sum fun a_1 b ↦ ↑f (b_1 * a • b) * g (a * a_1)) =
    (a.sum fun a b ↦ ↑f b * g a) * b.sum fun a b ↦ ↑f b * g a
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ 1 * single g a = single g a

Tactic:
| single g a =>

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

Goal state before:
pp: case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ single g a * 1 = single g a

Tactic:
| single g a =>

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

Goal state before:
pp: k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
inst✝³ : AddMonoid k
inst✝² : SMulZeroClass S k
inst✝¹ : FaithfulSMul S k
inst✝ : Nonempty G
_s₁ _s₂ : S
h : ∀ (a : SkewMonoidAlgebra k G), _s₁ • a = _s₂ • a
⊢ _s₁ = _s₂

Tactic:
by
    apply eq_of_smul_eq_smul fun a : G →₀ k ↦ congr_arg coeff _
    intro a
    simp_rw [ofCoeff_smul, h]

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

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
a b : Tropical R
⊢ (if a ≤ b then untrop a else untrop b) = untrop (if a ≤ b then a else b)

Tactic:
split_ifs <;> simp

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

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
a b : Tropical R
⊢ (if a ≤ b then untrop b else untrop a) = untrop (if a ≤ b then b else a)

Tactic:
split_ifs <;> simp

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

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
A : VertexOperator R V
n : ℤ
x : V
h : -n - 1 < ((HahnModule.of R).symm (A x)).order
⊢ (ncoeff A n) x = 0

Tactic:
simp only [ncoeff, HVertexOperator.coeff, LinearMap.coe_mk, AddHom.coe_mk]
  exact HahnSeries.coeff_eq_zero_of_lt_order h

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

Goal state before:
pp: case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
V : OpenNhds ((ConcreteCategory.hom f) x)
i : (h.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE ⋯
⊢ colimit.ι
      (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
            (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
        X.presheaf)
      (op V) =
    (colimit.ι
          (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
                (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
            X.presheaf)
          (op V) ≫
        Hom.stalkMap (X.ofRestrict h) x) ≫
      (X.restrictStalkIso h x).hom

Tactic:
colimit.ι_map_assoc,

Goal state after:
case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
V : OpenNhds ((ConcreteCategory.hom f) x)
i : (h.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE ⋯
⊢ colimit.ι
      (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
            (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
        X.presheaf)
      (op V) =
    ((((whiskeringLeft (OpenNhds ((ConcreteCategory.hom (X.ofRestrict h).base) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
                  (OpenNhds.inclusion ((ConcreteCategory.hom (X.ofRestrict h).base) x)).op).map
              (X.ofRestrict h).c).app
          (op V) ≫
        colimit.ι
            (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom (X.ofRestrict h).base) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
                  (OpenNhds.inclusion ((ConcreteCategory.hom (X.ofRestrict h).base) x)).op).obj
              ((pushforward C (X.ofRestrict h).base).obj (X.restrict h).presheaf))
            (op V) ≫
          stalkPushforward C (X.ofRestrict h).base (X.restrict h).presheaf x) ≫
      (X.restrictStalkIso h x).hom
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
V : OpenNhds ((ConcreteCategory.hom f) x)
i : (h.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE ⋯
⊢ colimit.ι
      (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
            (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
        X.presheaf)
      (op V) =
    ((((whiskeringLeft (OpenNhds ((ConcreteCategory.hom (X.ofRestrict h).base) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
                  (OpenNhds.inclusion ((ConcreteCategory.hom (X.ofRestrict h).base) x)).op).map
              (X.ofRestrict h).c).app
          (op V) ≫
        colimit.ι
            (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom (X.ofRestrict h).base) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
                  (OpenNhds.inclusion ((ConcreteCategory.hom (X.ofRestrict h).base) x)).op).obj
              ((pushforward C (X.ofRestrict h).base).obj (X.restrict h).presheaf))
            (op V) ≫
          stalkPushforward C (X.ofRestrict h).base (X.restrict h).presheaf x) ≫
      (X.restrictStalkIso h x).hom

Tactic:
colimit.ι_map_assoc,

Goal state after:
case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
V : OpenNhds ((ConcreteCategory.hom f) x)
i : (h.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE ⋯
⊢ colimit.ι
      (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
            (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
        X.presheaf)
      (op V) =
    ((((whiskeringLeft (OpenNhds ((ConcreteCategory.hom (X.ofRestrict h).base) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
                  (OpenNhds.inclusion ((ConcreteCategory.hom (X.ofRestrict h).base) x)).op).map
              (X.ofRestrict h).c).app
          (op V) ≫
        (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso (X.ofRestrict h).base x).inv) (X.restrict h).presheaf).app
            (op V) ≫
          colimit.ι
              ((OpenNhds.map (X.ofRestrict h).base x).op ⋙
                ((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑↑(X.restrict h))ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj
                  (X.restrict h).presheaf)
              (op V) ≫
            colimit.pre
              (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑↑(X.restrict h))ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj
                (X.restrict h).presheaf)
              (OpenNhds.map (X.ofRestrict h).base x).op) ≫
      (X.restrictStalkIso h x).hom
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
⊢ Mono (X.ofRestrict hf)

Tactic:
by
  have : Mono f := (TopCat.mono_iff_injective _).mpr hf.injective
  constructor
  intro Z g₁ g₂ eq
  ext1
  · have := congr_arg PresheafedSpace.Hom.base eq
    simp only [PresheafedSpace.comp_base, PresheafedSpace.ofRestrict_base] at this
    rw [cancel_mono] at this
    exact this
  · ext V
    have hV : (Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V) = V := by
      ext1
      exact Set.preimage_image_eq _ hf.injective
    have :
      IsIso (hf.isOpenMap.adjunction.counit.app (unop (op (hf.functor.obj V)))) :=
        NatIso.isIso_app_of_isIso
          (whiskerLeft hf.functor hf.isOpenMap.adjunction.counit) V
    have := PresheafedSpace.congr_app eq (op (hf.functor.obj V))
    rw [PresheafedSpace.comp_c_app, PresheafedSpace.comp_c_app,
      PresheafedSpace.ofRestrict_c_app, Category.assoc, cancel_epi] at this
    have h : _ ≫ _ = _ ≫ _ ≫ _ :=
      congr_arg (fun f => (X.restrict hf).presheaf.map (eqToHom hV).op ≫ f) this
    simp only [g₁.c.naturality, g₂.c.naturality_assoc] at h
    simp only [eqToHom_op, eqToHom_map, eqToHom_trans,
      ← IsIso.comp_inv_eq, inv_eqToHom, Category.assoc] at h
    simpa using h

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

Goal state before:
pp: X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens ↑X
sf : (i : ι) → ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : (subpresheafToTypes P.toPrelocalPredicate).IsCompatible U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) := fun i ↦ ↑(sf i)
sf'_comp : (X.presheafToTypes T).IsCompatible U sf'
⊢ IsCompatible (X.sheafToTypes T).obj U sf'

Tactic:
by exact sf'_comp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case mk.mk.w
X Y : Scheme
toLRSHom'✝¹ toLRSHom'✝ : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom'✝¹ }.base = { toLRSHom' := toLRSHom'✝ }.base
h_app :
  ∀ (U : Y.Opens),
    { toLRSHom' := toLRSHom'✝¹ }.app U ≫ X.presheaf.map (eqToHom ⋯).op = { toLRSHom' := toLRSHom'✝ }.app U
⊢ toLRSHom'✝¹.base = toLRSHom'✝.base

Tactic:
exact h_base

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h₃
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx :
  (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          ⊤ p trivial).hom'
      ((CommRingCat.ofHom
            (algebraMap (↑S)
              ((structureSheafInType ↑S ↑S).obj.obj
                (op ((TopologicalSpace.Opens.map (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj ⊤))))).hom'
        x) =
    (CommRingCat.Hom.hom
        (CommRingCat.ofHom
            (algebraMap (↑(CommRingCat.of ↑S))
              ((structureSheafInType ↑(CommRingCat.of ↑S) ↑(CommRingCat.of ↑S)).obj.obj
                ((TopologicalSpace.Opens.map (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).op.obj (op ⊤)))) ≫
          ((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                (structureSheaf ↑(CommRingCat.of ↑S)).obj).germ
            ⊤ p trivial))
      0
⊢ ∃ m, m • x = 0

Tactic:
rw [CommRingCat.comp_apply, map_zero] at hx

Goal state after:
case h₃
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx :
  (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          ⊤ p trivial).hom'
      ((CommRingCat.ofHom
            (algebraMap (↑S)
              ((structureSheafInType ↑S ↑S).obj.obj
                (op ((TopologicalSpace.Opens.map (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj ⊤))))).hom'
        x) =
    (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑(CommRingCat.of ↑S)).obj).germ
          ⊤ p trivial))
      0
⊢ ∃ m, m • x = 0
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
⊢ HasLimit (cospan f g ⋙ forget)

Tactic:
have : HasLimit (cospan ((cospan f g ⋙ forget).map Hom.inl)
      ((cospan f g ⋙ forget).map Hom.inr)) := by
    change HasLimit (cospan ((forget).map f) ((forget).map g))
    infer_instance

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 : HasLimit (cospan ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr))
⊢ HasLimit (cospan f g ⋙ forget)
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)
⊢ x ∈
    Set.range
      ⇑(Spec.map
          (CommRingCat.ofHom
            (algebraMap (↑R)
              (Localization.Away
                (s
                  (have this := ⋯;
                  this.choose))))))

Tactic:
by
    generalize_proofs H
    let i := H.choose
    have := PrimeSpectrum.localization_away_comap_range (Localization.Away (s i)) (s i)
    exact (eq_iff_iff.mp congr(x ∈ $this)).mpr H.choose_spec

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

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

Tactic:
rcases X.affineCover.covers a with ⟨x, e⟩

Goal state after:
case h_nhds
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
⊢ ∃ v ∈ {x | ∃ a, x = Set.range ⇑(X.affineBasisCover.f a)}, a ∈ v ∧ v ⊆ U
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
X : Scheme
U V : X.Opens
h : U ≤ V
W : (↑U).Opens
⊢ ⋯.functor.obj (unop (op (X.homOfLE h ''ᵁ W))) ≤ ⋯.functor.obj (unop (op W))

Tactic:
by
        suffices V.ι ''ᵁ _ ≤ U.ι ''ᵁ W by simpa
        simp [← Scheme.Hom.comp_image]

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
⊢ Set.range ⇑(pullback.fst f U.ι) = Set.range ⇑(f ⁻¹ᵁ U).ι

Tactic:
simp [IsOpenImmersion.range_pullbackFst]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ resLE f U (f ⁻¹ᵁ U) ⋯ = f ∣_ U

Tactic:
simp [resLE]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
⊢ resLE f U V e ≫ U.ι = V.ι ≫ f

Tactic:
simp [resLE]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
V : X.Opens
U : Y.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
i : V ≤ f ⁻¹ᵁ U
this : IsAffine ↑U
⊢ Spec.map (Scheme.Hom.appLE f U V i) ≫ Spec.map (Y.presheaf.map (eqToHom ⋯).op) ≫ (↑U).isoSpec.inv ≫ U.ι =
    Spec.map (X.presheaf.map (eqToHom ⋯).op) ≫ (↑V).isoSpec.inv ≫ (X.homOfLE i ≫ (f ⁻¹ᵁ U).ι) ≫ f

Tactic:
rw [Category.assoc, ← morphismRestrict_ι,
    ← Category.assoc _ (f ∣_ U) U.ι, ← @Scheme.isoSpec_inv_naturality_assoc,
    ← Spec.map_comp_assoc, ← Spec.map_comp_assoc, Scheme.Hom.comp_appTop, morphismRestrict_appTop,
    Scheme.homOfLE_appTop, Scheme.Hom.app_eq_appLE, Scheme.Hom.appLE_map,
    Scheme.Hom.appLE_map, Scheme.Hom.appLE_map, Scheme.Hom.map_appLE]

Goal state after: