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
hff :
  ∀ {q : R[X]} {r : (i : ι) → Fin (n i) → R[X]},
    ((algebraMap R[X] K) q + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r i j) * gi i ^ (↑j + 1)) *
        ∏ i ∈ s, (algebraMap R[X] K) (g i) ^ n i =
      (algebraMap R[X] K) (q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j.rev * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k)
hf :
  (algebraMap R[X] K) (q₁ * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r₁ i j.rev * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k) =
    ((algebraMap R[X] K) q₂ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₂ i j) * gi i ^ (↑j + 1)) *
      ∏ i ∈ s, (algebraMap R[X] K) (g i) ^ n i
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i

Tactic:
hff,

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
hff :
  ∀ {q : R[X]} {r : (i : ι) → Fin (n i) → R[X]},
    ((algebraMap R[X] K) q + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r i j) * gi i ^ (↑j + 1)) *
        ∏ i ∈ s, (algebraMap R[X] K) (g i) ^ n i =
      (algebraMap R[X] K) (q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j.rev * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k)
hf :
  (algebraMap R[X] K) (q₁ * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r₁ i j.rev * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k) =
    (algebraMap R[X] K) (q₂ * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r₂ i j.rev * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k)
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
f : R[X]
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
this : Nontrivial R
hgi : ∀ i ∈ s, ((algebraMap R[X] K) (g i))⁻¹ * (algebraMap R[X] K) (g i) = 1
⊢ ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ ↑f / ∏ i ∈ s, ↑(g i) = ↑q + ∑ i ∈ s, ↑(r i) / ↑(g i)

Tactic:
obtain ⟨q, r, hr, hf⟩ := mul_prod_pow_inverse_eq_quo_add_sum_rem_mul_pow_inverse
    f hg hcop (fun _ => 1) hgi

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
f : R[X]
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
this : Nontrivial R
hgi : ∀ i ∈ s, ((algebraMap R[X] K) (g i))⁻¹ * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : ι → Fin 1 → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin 1), (r i j).degree < (g i).degree
hf :
  (algebraMap R[X] K) f * ∏ i ∈ s, ((algebraMap R[X] K) (g i))⁻¹ ^ 1 =
    (algebraMap R[X] K) q + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r i j) * ((algebraMap R[X] K) (g i))⁻¹ ^ (↑j + 1)
⊢ ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ ↑f / ∏ i ∈ s, ↑(g i) = ↑q + ∑ i ∈ s, ↑(r i) / ↑(g i)
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: case mpr
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
⊢ R a = L a ∧ L a ∈ (toEndRingHom α).rangeS → a ∈ NonUnitalSubsemiring.center α

Tactic:
rintro ⟨hc, ⟨T, hT⟩⟩
    have e1 (d : α) : T d = a * d := congr($hT d)
    have e2 (d : α) : T d = d * a := congr($(hT.trans hc.symm) d)
    constructor
    case comm => exact (congr($hc.symm ·))
    case left_assoc => simpa [e1] using (map_mul_right T · ·)
    case right_assoc => simpa [e2] using (map_mul_left T · ·)

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

Goal state before:
pp: α : Type u_5
inst✝ : NonUnitalNonAssocCommSemiring α
a : α
⊢ a ∈ NonUnitalSubsemiring.center α ↔ ∀ (b : α), Commute (L b) (L a)

Tactic:
rw [NonUnitalNonAssocSemiring.mem_center_iff, CentroidHom.centroid_eq_centralizer_mulLeftRight,
    Subsemiring.mem_centralizer_iff, AddMonoid.End.mulRight_eq_mulLeft, Set.union_self]

Goal state after:
α : Type u_5
inst✝ : NonUnitalNonAssocCommSemiring α
a : α
⊢ (L a = L a ∧ ∀ g ∈ Set.range ⇑L, g * L a = L a * g) ↔ ∀ (b : α), Commute (L b) (L a)
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
c : R
⊢ (C c * X).support ⊆ {1}

Tactic:
simpa [C_mul_X_eq_monomial] using support_monomial_subset 1

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

Goal state before:
pp: case mk.mk
R✝ : Type u
inst✝³ : Semiring R✝
r✝ : R✝ → R✝ → Prop
inst✝² : StarRing R✝
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
r : R → R → Prop
hr : ∀ (a b : R), r a b → r (star a) (star b)
toQuot✝¹ : Quot (Rel r)
a✝¹ : R
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ star' r hr ({ toQuot := Quot.mk (Rel r) a✝¹ } * { toQuot := Quot.mk (Rel r) a✝ }) =
    star' r hr { toQuot := Quot.mk (Rel r) a✝ } * star' r hr { toQuot := Quot.mk (Rel r) a✝¹ }

Tactic:
simp [star'_quot, mul_quot, star_mul]

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

Goal state before:
pp: X✝ X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
⊢ homOfSheafedSpaceHomOfIsIso f.inv ≫ homOfSheafedSpaceHomOfIsIso f.hom = 𝟙 Y

Tactic:
by
    ext : 1
    dsimp
    rw [← InducedCategory.comp_hom, f.inv_hom_id, SheafedSpace.id_hom]

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

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
⊢ g₁.c ≫ whiskerRight (eqToHom ⋯) Z.presheaf = g₂.c

Tactic:
· 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.AlgebraicGeometry.Spec

Goal state before:
pp: R : CommRingCatᵒᵖ
⊢ locallyRingedSpaceMap (𝟙 R).unop = 𝟙 (locallyRingedSpaceObj (unop R))

Tactic:
by dsimp; rw [Spec.locallyRingedSpaceMap_id]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsOpenImmersion g
⊢ opensRange (f ≫ g) = opensRange g

Tactic:
opensRange_comp,

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsOpenImmersion g
⊢ g ''ᵁ opensRange f = opensRange g
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : Y.Opens
hU : U ≤ opensRange f
⊢ ↑(f ''ᵁ f ⁻¹ᵁ U) = ↑U

Tactic:
simpa [Set.image_preimage_eq_inter_range]

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

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

Tactic:
exact ⟨_, _, hf, hi⟩

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

Goal state before:
pp: X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) f = (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) g
⊢ f = g

Tactic:
fapply TopCat.Sheaf.eq_of_locally_eq' X.sheaf
    (fun i ↦ (𝒰.f (𝒰.idx i)).opensRange ⊓ U) _ (fun _ ↦ homOfLE inf_le_right)

Goal state after:
case hcover
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) f = (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) g
⊢ U ≤ ⨆ i, Hom.opensRange (𝒰.f (Cover.idx 𝒰 i)) ⊓ U

case h
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) f = (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) g
⊢ ∀ (i : ↥X),
    (ConcreteCategory.hom (X.sheaf.obj.map (homOfLE ⋯).op)) f =
      (ConcreteCategory.hom (X.sheaf.obj.map (homOfLE ⋯).op)) g
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
r : ↑Γ(↑U, ⊤)
⊢ X.basicOpen ((ConcreteCategory.hom (Hom.appIso (X.ofRestrict ⋯) ⊤).inv) r) =
    X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op)) r)

Tactic:
rw [← Scheme.basicOpen_res_eq _ _ (eqToHom U.isOpenEmbedding_obj_top).op]

Goal state after:
X : Scheme
U : X.Opens
r : ↑Γ(↑U, ⊤)
⊢ X.basicOpen ((ConcreteCategory.hom (Hom.appIso (X.ofRestrict ⋯) ⊤).inv) r) =
    X.basicOpen
      ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op))
        ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op)) r))
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
⊢ app (resLE f U V e) ⊤ = U.topIso.hom ≫ appLE f U V e ≫ V.topIso.inv

Tactic:
simp [Scheme.Hom.resLE]

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
⊢ ∃ ι 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:
choose g hxg igU f H using fun x : U ↦ exists_const U s x.1 x.2
  have (i j : _) : LocalizedModule.mk (g i • f j) ⟨g i * g j, Submonoid.mem_powers _⟩ =
      LocalizedModule.mk (g j • f i) ⟨g i * g j, Submonoid.mem_powers _⟩ := by
    refine toBasicOpenₗ_injective (g i * g j) ?_
    simp only [toBasicOpenₗ_mk]
    have := H i
    trans (structureSheafInType R M).obj.map (homOfLE ?_).op s
    · refine .trans (Subtype.ext <| funext fun a ↦ ?_) congr((structureSheafInType R M).obj.map
        (homOfLE ((PrimeSpectrum.basicOpen_mul (g i) (g j)).trans_le inf_le_right)).op $(H j))
      exact LocalizedModule.mk_eq.mpr ⟨1, by simp [Submonoid.smul_def, ← smul_assoc]; ring_nf⟩
    · refine congr((structureSheafInType R M).obj.map (homOfLE ((PrimeSpectrum.basicOpen_mul (g i)
        (g j)).trans_le inf_le_left)).op $(H i)).symm.trans (Subtype.ext <| funext fun a ↦ ?_)
      exact LocalizedModule.mk_eq.mpr ⟨1, by simp [Submonoid.smul_def, ← smul_assoc]⟩
    · exact ((PrimeSpectrum.basicOpen_mul (g i) (g j)).trans_le inf_le_right).trans (igU _)
  simp only [LocalizedModule.mk_eq, Submonoid.smul_def, Subtype.exists, Submonoid.mem_powers_iff,
    exists_prop, exists_exists_eq_and, ← mul_smul, ← pow_succ, ← mul_assoc _ (_ * _)] at this
  choose n hn using this
  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 _))
  let N := (t ×ˢ t).sup fun x ↦ n x.1 x.2 + 1
  refine ⟨t, inferInstance, fun i ↦ g i ^ N • f i, fun i ↦ (g i) ^ (N + 1),
    fun x ↦ by simpa using igU x.1, fun x hx ↦ by simpa using ht hx, fun i j ↦ ?_, fun i ↦ ?_⟩
  · dsimp
    convert_to (g i * g ↑j) ^ N • g j • f i = (g i * g ↑j) ^ N • g i • f j
    · module
    · module
    have : n i j + 1 ≤ N := (t ×ˢ t).le_sup (f := fun x ↦ n x.1 x.2 + 1) (b := ⟨_, _⟩) (by simp)
    rw [← Nat.sub_add_cancel this, pow_add, mul_smul, mul_smul]
    congr 1
    convert! (hn i j).symm using 1 <;> module
  · convert! congr((structureSheafInType R M).presheaf.map (homOfLE ?_).op $((H i).symm)) using 1
    · refine Subtype.ext <| funext fun x ↦ LocalizedModule.mk_eq.mpr ⟨1, ?_⟩
      simp [Submonoid.smul_def, pow_succ', mul_smul]
    · simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
s : (structureSheafInType R M).obj.obj (op (basicOpen f))
ι : Type u
w✝ : Fintype ι
a : ι → M
b : ι → R
ibU : ∀ (i : ι), basicOpen (b i) ≤ basicOpen f
iU : basicOpen f ≤ ⨆ i, basicOpen (b i)
hab : ∀ (i j : ι), b j • a i = b i • a j
H :
  ∀ (i : ι),
    (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s = const (a i) (b i) (basicOpen (b i)) ⋯
n : ℕ
c : ι →₀ R
hc : ∑ i, c i • b i = f ^ (n + 1)
i : ι
x : ↥(unop (op (basicOpen (b i))))
⊢ (∑ i, c i • b i) • a i = f ^ (n + 1) • a i

Tactic:
hc

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
inst✝ : IsAffine X
s : Set ↥X
⊢ IsClosed s ↔ ∃ I, s = X.zeroLocus ↑I

Tactic:
refine ⟨fun hs ↦ ?_, ?_⟩
  · let Z : Set (Spec Γ(X, ⊤)) := X.toΓSpecFun '' s
    have hZ : IsClosed Z := (X.isoSpec.hom.homeomorph).isClosedMap _ hs
    obtain ⟨I, (hI : Z = _)⟩ := (PrimeSpectrum.isClosed_iff_zeroLocus_ideal _).mp hZ
    use I
    simp only [← Scheme.toSpecΓ_preimage_zeroLocus, ← hI, Z]
    symm
    exact Set.preimage_image_eq _ (bijective_of_isIso X.isoSpec.hom.base).injective
  · rintro ⟨I, rfl⟩
    exact zeroLocus_isClosed X I.carrier

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
U : Set ↑(D.U i)
x : ↑(D.V (j, i))
| x ∈ ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U

Tactic:
rw [← Set.preimage_image_eq U (D.ι_injective _)]

Goal state after:
D : GlueData
i j : D.J
U : Set ↑(D.U i)
x : ↑(D.V (j, i))
| x ∈
    ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹'
      ⇑(ConcreteCategory.hom (D.ι i)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' U
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' U =
    ⇑(ConcreteCategory.hom (D.f j i)) '' ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U

Tactic:
have : D.f _ _ ⁻¹' 𝖣.ι j ⁻¹' 𝖣.ι i '' U = (D.t j i ≫ D.f _ _) ⁻¹' U := by
    ext x
    conv_rhs => rw [← Set.preimage_image_eq U (D.ι_injective _)]
    simp

Goal state after:
D : GlueData
i j : D.J
U : Set ↑(D.U i)
this :
  ⇑(ConcreteCategory.hom (D.f j i)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' U =
    ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' U =
    ⇑(ConcreteCategory.hom (D.f j i)) '' ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X R✝ : C
f : R✝ ⟶ X
R S : Over X
⊢ Hom.left (LaxMonoidal.μ (pullback f) R S) ≫ pullback.snd (R ⊗ S).hom f =
    pullback.snd ((pullback f).obj R).hom ((pullback f).obj S).hom ≫ pullback.snd S.hom f

Tactic:
rw [Monoidal.μ_of_cartesianMonoidalCategory,
    ← cancel_epi (prodComparisonIso (Over.pullback f) R S).hom.left,
    ← Over.comp_left_assoc, Iso.hom_inv_id]
  simp [CartesianMonoidalCategory.prodComparison]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
S : Set ↑↑(D.V (i, j))
eq₁ :
  (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫
      pullback.fst ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) =
    (pullback.fst (D.f i j) (D.f i k)).base
eq₂ :
  (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫
      pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) =
    (pullback.snd (D.f i j) (D.f i k)).base
⊢ ⇑(ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k)).base) ''
      ⇑(ConcreteCategory.hom
            ((PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫
              pullback.fst ((forget C).map (D.f i j)) ((forget C).map (D.f i k)))) ⁻¹'
        S =
    ⇑(ConcreteCategory.hom (D.f i k).base) ⁻¹' ⇑(ConcreteCategory.hom (D.f i j).base) '' S

Tactic:
← eq₂,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
S : Set ↑↑(D.V (i, j))
eq₁ :
  (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫
      pullback.fst ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) =
    (pullback.fst (D.f i j) (D.f i k)).base
eq₂ :
  (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫
      pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) =
    (pullback.snd (D.f i j) (D.f i k)).base
⊢ ⇑(ConcreteCategory.hom
          ((PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫
            pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k)))) ''
      ⇑(ConcreteCategory.hom
            ((PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫
              pullback.fst ((forget C).map (D.f i j)) ((forget C).map (D.f i k)))) ⁻¹'
        S =
    ⇑(ConcreteCategory.hom (D.f i k).base) ⁻¹' ⇑(ConcreteCategory.hom (D.f i j).base) '' S
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↥Y
⊢ IsIso f

Tactic:
have : IsEmpty X := f.base.hom.1.isEmpty

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↥Y
this : IsEmpty ↥X
⊢ IsIso f
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
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
k₁ : (k : J) × (k ⟶ i) × (k ⟶ j)
k₂ : (k_1 : J) × (k_1 ⟶ i) × (k_1 ⟶ k)
l : J
hli : l ⟶ k₁.fst
hlk : l ⟶ k₂.fst
z : (F ⋙ forget).obj l
hy₁ : (F.map k₁.snd.1) ((ConcreteCategory.hom ((F ⋙ forget).map hli)) z) = ↑((pullback.fst (V F i j).ι (V F i k).ι) x)
hy₂ : (F.map k₂.snd.1) ((ConcreteCategory.hom ((F ⋙ forget).map hlk)) z) = ↑((pullback.snd (V F i j).ι (V F i k).ι) x)
α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι :=
  pullback.lift ((Hom.isoOpensRange (F.map (hli ≫ k₁.snd.1))).hom ≫ (F.obj i).homOfLE ⋯)
    ((Hom.isoOpensRange (F.map (hli ≫ k₁.snd.1))).hom ≫ (F.obj i).homOfLE ⋯) ⋯
this : IsOpenImmersion α
⊢ (((Hom.isoOpensRange (F.map (hli ≫ k₁.snd.1))).hom ≫ (F.obj i).homOfLE ⋯) ≫ (V F i j).ι) z =
    (V F i j).ι ((pullback.fst (V F i j).ι (V F i k).ι) x)

Tactic:
simpa using hy₁

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

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

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

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
        pullback.snd (𝒰.f i ≫ f) g =
    pullbackFstιToV 𝒰 f g i j ≫
      t 𝒰 f g j i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ pullback.snd (𝒰.f i ≫ f) g

Tactic:
simp_rw [t_fst_snd, pullback.lift_snd, pullbackFstιToV_fst_assoc, pullback.condition_assoc,
        GlueData.openCover_f, p2]
      simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case inv_hom_id.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i : 𝒰.I₀
⊢ (pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯ ≫
        pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯) ≫
      pullback.fst (𝒰.f i ≫ f) g =
    𝟙 (pullback (𝒰.f i ≫ f) g) ≫ pullback.fst (𝒰.f i ≫ f) g

Tactic:
simp_rw [Category.assoc, pullback.lift_fst, pullback.lift_snd, Category.id_comp]

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✝
A B C : CommRingCat
f : Spec A ⟶ Spec C
g : Spec B ⟶ Spec C
⊢ HasPullback f g

Tactic:
rw [← Scheme.Spec.map_preimage f, ← Scheme.Spec.map_preimage g]
  exact ⟨⟨⟨_, isLimitOfHasPullbackOfPreservesLimit
    Scheme.Spec (Scheme.Spec.preimage f) (Scheme.Spec.preimage g)⟩⟩⟩

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → X.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P ((U i).ι ≫ f)
⊢ P f

Tactic:
refine (P.iff_of_zeroHypercover_source
    (X.openCoverOfIsOpenCover (s := Set.range U) Subtype.val (by ext; simp [← hU]))).mpr fun i ↦ ?_

Goal state after:
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → X.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P ((U i).ι ≫ f)
i : (X.openCoverOfIsOpenCover Subtype.val ⋯).I₀
⊢ P ((X.openCoverOfIsOpenCover Subtype.val ⋯).f i ≫ f)
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
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
i j : (glueData F).toLocallyRingedSpaceGlueData.J
x✝ :
  (MultispanShape.prod
      (Cover.ulift
              (Opens.iSupOpenCover fun i_1 ↦
                Hom.opensRange (F.map i_1.snd.1))).gluedCover.toLocallyRingedSpaceGlueData.J).R
k : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hk : k ∈ ⨆ i_1, Hom.opensRange (F.map i_1.snd.1)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp +instances only [Opens.iSupOpenCover, Cover.ulift, V, ← Hom.comp_toLRSHom_assoc,
        Cover.ι_fromGlued_assoc, homOfLE_ι, Hom.isoOpensRange_hom_ι, Cover.idx]

Goal state after:
J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
i j : (glueData F).toLocallyRingedSpaceGlueData.J
x✝ :
  (MultispanShape.prod
      (Cover.ulift
              (Opens.iSupOpenCover fun i_1 ↦
                Hom.opensRange (F.map i_1.snd.1))).gluedCover.toLocallyRingedSpaceGlueData.J).R
k : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hk : k ∈ ⨆ i_1, Hom.opensRange (F.map i_1.snd.1)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: ⊢ @Surjective = topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective

Tactic:
by ext; exact surjective_iff _

Goal state after: