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)
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)
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i

Tactic:
by
    apply_fun (· * ∏ i ∈ s, algebraMap R[X] K (g i) ^ n i) at hf
    rw [hff, hff, (FaithfulSMul.algebraMap_injective R[X] K).eq_iff] at hf
    obtain ⟨hq, hr⟩ := quo_mul_prod_pow_add_sum_rem_mul_prod_pow_unique hg hgg
      (fun i hi j => hr₁ i hi j.rev) (fun i hi j => hr₂ i hi j.rev) hf
    exact ⟨hq, fun i hi => funext fun j => j.rev_rev ▸ congrFun (hr i hi) j.rev⟩

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k +
          ((x.imI * y.re) • q.i + (x.imI * y.imI) • (q.i * q.i) + (x.imI * y.imJ) • (q.i * q.j) +
            (x.imI * y.imK) • (q.i * q.k)) +
        ((x.imJ * y.re) • q.j + (x.imJ * y.imI) • (q.j * q.i) + (x.imJ * y.imJ) • (q.j * q.j) +
          (x.imJ * y.imK) • (q.j * q.k)) +
      ((x.imK * y.re) • q.k + (x.imK * y.imI) • (q.k * q.i) + (x.imK * y.imJ) • (q.k * q.j) +
        (x.imK * y.imK) • (q.k * q.k))

Tactic:
simp only [i_mul_i, j_mul_j, i_mul_j, j_mul_i, i_mul_k, k_mul_i, k_mul_j, j_mul_k, k_mul_k]

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k +
          ((x.imI * y.re) • q.i + (x.imI * y.imI) • (c₁ • 1 + c₂ • q.i) + (x.imI * y.imJ) • q.k +
            (x.imI * y.imK) • (c₁ • q.j + c₂ • q.k)) +
        ((x.imJ * y.re) • q.j + (x.imJ * y.imI) • (c₂ • q.j - q.k) + (x.imJ * y.imJ) • c₃ • 1 +
          (x.imJ * y.imK) • ((c₂ * c₃) • 1 - c₃ • q.i)) +
      ((x.imK * y.re) • q.k + (x.imK * y.imI) • -c₁ • q.j + (x.imK * y.imJ) • c₃ • q.i +
        (x.imK * y.imK) • -((c₁ * c₃) • 1))
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
r : R
x : ℍ[R,c₁,c₂,c₃]
⊢ q.lift (r • x) = r • q.lift x

Tactic:
simp [lift, mul_smul, ← Algebra.smul_def]

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case a
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
B : Basis A c₁ c₂ c₃
⊢ B.liftHom.range ≤ R[B.i, B.j, B.k]

Tactic:
rintro x ⟨y, rfl⟩
    refine add_mem (add_mem (add_mem ?_ ?_) ?_) ?_
    · exact algebraMap_mem _ _
    all_goals
      exact Subalgebra.smul_mem _ (Algebra.subset_adjoin <| by simp) _

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : IsFormallyReal R
s₁ s₂ : R
hs₁ : IsSumSq s₁
hs₂ : IsSumSq s₂
h : s₁ + s₂ = 0
⊢ s₁ = 0

Tactic:
by_contra! h₁

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : IsFormallyReal R
s₁ s₂ : R
hs₁ : IsSumSq s₁
hs₂ : IsSumSq s₂
h : s₁ + s₂ = 0
h₁ : s₁ ≠ 0
⊢ False
Module: Mathlib.Algebra.Ring.Semireal.Defs

Goal state before:
pp: R : Type u_1
inst✝² : AddGroup R
inst✝¹ : One R
inst✝ : Mul R
h : ¬IsSumSq (-1)
⊢ ∀ {s : R}, IsSumSq s → 1 + s ≠ 0

Tactic:
by aesop (add simp add_eq_zero_iff_neg_eq)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p q : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
h : p ≠ q
h01 : 0 = 1
⊢ p = q

Tactic:
rw [← mul_one p, ← mul_one q, ← C_1, ← h01, C_0, mul_zero, mul_zero]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : CommMonoid G
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
a b : SkewMonoidAlgebra k G
g : G
r : k
⊢ g • r = r

Tactic:
rw [← Algebra.algebraMap_self_apply r, smul_algebraMap g r]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Multiset R
⊢ trop s.inf = (map trop s).sum

Tactic:
by
  induction s using Multiset.induction with
  | empty => simp
  | cons s x IH => simp [← IH]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
hs : ¬BddAbove s
this : Set.range untrop = Set.univ
⊢ sSup (untrop '' s) = sSup ∅

Tactic:
apply csSup_of_not_bddAbove

Goal state after:
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
hs : ¬BddAbove s
this : Set.range untrop = Set.univ
⊢ ¬BddAbove (untrop '' s)
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ✝ : Type u_1
inst✝¹⁴ : PartialOrder Γ✝
R✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
inst✝¹³ : CommRing R✝
inst✝¹² : AddCommGroup V✝
inst✝¹¹ : Module R✝ V✝
inst✝¹⁰ : AddCommGroup W✝
inst✝⁹ : Module R✝ W✝
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u : U
g' : Γ'
hg' : ¬A (((of R).symm (B u)).coeff g') = 0
hAB : ((of R).symm (B u)).coeff g' = 0
⊢ A (((of R).symm (B u)).coeff g') = 0

Tactic:
simp [hAB]

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 Z : PresheafedSpace C
α : X ⟶ Y
β : Y ⟶ Z
x : ↑↑X
⊢ Hom.stalkMap (α ≫ β) x = Hom.stalkMap β ((ConcreteCategory.hom α.base) x) ≫ Hom.stalkMap α x

Tactic:
dsimp [Hom.stalkMap, stalkFunctor, stalkPushforward]
  -- We can't use `ext` here due to https://github.com/leanprover/std4/pull/159
  apply colimit.hom_ext
  rintro ⟨U, hU⟩
  simp

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : X ⟶ Y
h₁ : Function.Injective ⇑(ConcreteCategory.hom f.hom.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Epi (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace C
g : ↑Z.toPresheafedSpace ⟶ ↑X.toPresheafedSpace
gc hc : X.presheaf ⟶ (pushforward C g).obj Z.presheaf
e : { hom := { base := g, c := gc } } ≫ f = { hom := { base := g, c := hc } } ≫ f
⊢ { hom := { base := g, c := gc } } = { hom := { base := g, c := hc } }

Tactic:
refine SheafedSpace.hom_stalk_ext ⟨g, gc⟩ ⟨g, hc⟩ rfl fun x ↦ ?_

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : X ⟶ Y
h₁ : Function.Injective ⇑(ConcreteCategory.hom f.hom.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Epi (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace C
g : ↑Z.toPresheafedSpace ⟶ ↑X.toPresheafedSpace
gc hc : X.presheaf ⟶ (pushforward C g).obj Z.presheaf
e : { hom := { base := g, c := gc } } ≫ f = { hom := { base := g, c := hc } } ≫ f
x : ↑↑Z.toPresheafedSpace
⊢ PresheafedSpace.Hom.stalkMap { hom := { base := g, c := gc } }.hom x =
    (X.presheaf.stalkCongr ⋯).hom ≫ PresheafedSpace.Hom.stalkMap { hom := { base := g, c := hc } }.hom x
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: case mp
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : (ConcreteCategory.hom f.base) x ∈ U
hx : IsUnit ((ConcreteCategory.hom (Y.toRingedSpace.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s)
⊢ IsUnit
    ((ConcreteCategory.hom (X.presheaf.germ ((Opens.map f.base).obj U) x hxU))
      ((ConcreteCategory.hom (f.c.app (op U))) s))

Tactic:
← stalkMap_germ_apply

Goal state after:
case mp
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : (ConcreteCategory.hom f.base) x ∈ U
hx : IsUnit ((ConcreteCategory.hom (Y.toRingedSpace.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s)
⊢ IsUnit
    ((ConcreteCategory.hom (Hom.stalkMap f x))
      ((ConcreteCategory.hom (Y.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s))
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: case mpr
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ (Opens.map f.base).obj U
hx :
  IsUnit
    ((ConcreteCategory.hom (X.presheaf.germ ((Opens.map f.base).obj U) x hxU))
      ((ConcreteCategory.hom (f.c.app (op U))) s))
⊢ IsUnit ((ConcreteCategory.hom (Y.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s)

Tactic:
← stalkMap_germ_apply

Goal state after:
case mpr
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ (Opens.map f.base).obj U
hx :
  IsUnit
    ((ConcreteCategory.hom (Hom.stalkMap f x))
      ((ConcreteCategory.hom (Y.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s))
⊢ IsUnit ((ConcreteCategory.hom (Y.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s)
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
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
j : J
x✝ : ↑((F ⋙ forget C).obj j)
⊢ (ConcreteCategory.hom (colimit.ι (F ⋙ forget C) j ≫ m.base)) x✝ =
    (ConcreteCategory.hom (colimit.ι (F ⋙ forget C) j ≫ colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))) x✝

Tactic:
colimit.ι_desc,

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
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
j : J
x✝ : ↑((F ⋙ forget C).obj j)
⊢ (ConcreteCategory.hom (colimit.ι (F ⋙ forget C) j ≫ m.base)) x✝ =
    (ConcreteCategory.hom (((forget C).mapCocone s).ι.app j)) x✝
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T✝ : ↑X → Type u_1
T : Type ?u.10
inst✝ : TopologicalSpace T
U : Opens ↑X
f : ↥U → T
w : ∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (X.continuousPrelocal T).pred fun x ↦ f (i x)
⊢ (X.continuousPrelocal T).pred f

Tactic:
apply continuous_iff_continuousAt.2
      intro x
      specialize w x
      rcases w with ⟨V, m, i, w⟩
      dsimp at w
      rw [continuous_iff_continuousAt] at w
      specialize w ⟨x, m⟩
      simpa using (Opens.isOpenEmbedding_of_le i.le).continuousAt_iff.1 w

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
e : X ≅ Y
x : ↥X
⊢ e.inv (e.hom x) = x

Tactic:
change (e.hom ≫ e.inv) x = 𝟙 X.toPresheafedSpace x

Goal state after:
X Y : Scheme
e : X ≅ Y
x : ↥X
⊢ (e.hom ≫ e.inv) x = (ConcreteCategory.hom (𝟙 X.toPresheafedSpace).base) x
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: U V X Y : Scheme
g : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
f : X ⟶ Y
inst✝¹ : IsOpenImmersion iU
inst✝ : IsOpenImmersion iV
H : iU ≫ f = g ≫ iV
H' : f ⁻¹ᵁ Scheme.Hom.opensRange iV = Scheme.Hom.opensRange iU
e : pullback iV f ≅ U := isoOfRangeEq (pullback.snd iV f) iU ⋯
⊢ e.inv ≫ pullback.snd iV f = iU ≫ 𝟙 X

Tactic:
by simp [e]

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

Goal state before:
pp: case intro
X : Scheme
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
H : ∀ (i : 𝒰.I₀), CompactSpace ↥(𝒰.X i)
val✝ : Fintype 𝒰.I₀
i : 𝒰.I₀
⊢ IsCompact (Set.range ⇑(𝒰.f i))

Tactic:
isCompact_iff_compactSpace

Goal state after:
case intro
X : Scheme
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
H : ∀ (i : 𝒰.I₀), CompactSpace ↥(𝒰.X i)
val✝ : Fintype 𝒰.I₀
i : 𝒰.I₀
⊢ CompactSpace ↑(Set.range ⇑(𝒰.f i))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
s : PullbackCone f g
⊢ ∀ {m : s.pt ⟶ (pullbackConeOfLeft f g).pt},
    m ≫ (pullbackConeOfLeft f g).fst = s.fst →
      m ≫ (pullbackConeOfLeft f g).snd = s.snd →
        m =
          {
            toHom :=
              PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
                (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯),
            prop := ⋯ }

Tactic:
intro m _ h₂
      rw [← cancel_mono (pullbackConeOfLeft f g).snd]
      exact h₂.trans <| LocallyRingedSpace.Hom.ext'
        (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_snd f.1 g.1 <|
          PullbackCone.mk s.fst.1 s.snd.1 <| congr_arg
            LocallyRingedSpace.Hom.toHom s.condition).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)), Ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
f : ↥↑V → ↑Γ(X, ↑V)
hf₁ : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥↑V), P (X.affineBasicOpen (f x))
this : Ideal.span (Set.range f) = ⊤
⊢ P V

Tactic:
by
    obtain ⟨t, ht₁, ht₂⟩ := (Ideal.span_eq_top_iff_finite _).mp this
    apply openCover V t ht₂
    rintro ⟨i, hi⟩
    obtain ⟨x, rfl⟩ := ht₁ hi
    exact hf₂ x

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf : ∀ (x y : 𝒰.I₀), pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x = pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y
x : 𝒰.I₀
i : (Precoverage.ZeroHypercover.pullback₁ (𝒰.f x) (ulift 𝒰)).I₀
⊢ pullback.snd (𝒰.f x) (𝒰.f (idx 𝒰 i)) ≫ 𝒰.f (idx 𝒰 i) ≫ glueMorphisms 𝒰 f hf =
    pullback.fst (𝒰.f x) (𝒰.f (idx 𝒰 i)) ≫ f x

Tactic:
← ulift_f,

Goal state after:
X : Scheme
𝒰 : X.OpenCover
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf : ∀ (x y : 𝒰.I₀), pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x = pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y
x : 𝒰.I₀
i : (Precoverage.ZeroHypercover.pullback₁ (𝒰.f x) (ulift 𝒰)).I₀
⊢ pullback.snd (𝒰.f x) ((ulift 𝒰).f i) ≫ (ulift 𝒰).f i ≫ glueMorphisms 𝒰 f hf =
    pullback.fst (𝒰.f x) ((ulift 𝒰).f i) ≫ f x
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Function.Injective ⇑(ConcreteCategory.hom (D.gluedIso (forget C)).inv)

Tactic:
rw [← TopCat.mono_iff_injective]
    infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
⊢ Nonempty (IsColimit (BinaryCofan.mk f g))

Tactic:
let c' : Cofan fun j ↦ (WalkingPair.casesOn j X Y : Scheme.{u}) :=
    .mk S fun j ↦ WalkingPair.casesOn j f g
  let i : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl _) (by rintro (b | b) <;> rfl)
  refine ⟨IsColimit.ofIsoColimit (Nonempty.some ?_) i.symm⟩
  let fi (j : WalkingPair) : WalkingPair.casesOn j X Y ⟶ S := WalkingPair.casesOn j f g
  convert! nonempty_isColimit_cofanMk_of fi _ _
  · intro i
    cases i <;> (simp [fi]; infer_instance)
  · simpa [← WalkingPair.equivBool.symm.iSup_comp, iSup_bool_eq, ← codisjoint_iff] using hf.2
  · intro i j hij
    match i, j with
    | .left, .right => simpa [fi] using hf.1
    | .right, .left => simpa [fi] using hf.1.symm

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
i : ι
⊢ P (f ∣_ Scheme.Hom.opensRange ((Y.openCoverOfIsOpenCover Subtype.val ⋯).f ⟨U i, ⋯⟩))

Tactic:
change P (f ∣_ (U i).ι.opensRange)

Goal state after:
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
i : ι
⊢ P (f ∣_ Scheme.Hom.opensRange (U i).ι)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
⊢ PresheafedSpace.IsOpenImmersion (D.ι i).hom

Tactic:
← D.ι_isoPresheafedSpace_inv

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
⊢ PresheafedSpace.IsOpenImmersion (D.toPresheafedSpaceGlueData.ι i ≫ D.isoPresheafedSpace.inv)
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: X : Scheme
U V : X.Opens
hU : Dense ↑U
hU' : U ≤ V
⊢ IsDominant (X.homOfLE hU' ≫ V.ι)

Tactic:
by simpa using Opens.isDominant_ι hU

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Lemmas

Goal state before:
pp: case h
R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
h₁ : Ideal.span (p ⟨a, ha⟩) ≤ Ideal.span (⇑(algebraMap R (Rₜ ⟨a, ha⟩)) '' Set.range (mulNumerator s p))
y : R
hy : y ∈ Ideal.span (Set.range (mulNumerator s p))
m n : ℕ
hc : a ^ n * a ^ m = a ^ n * y
⊢ a ^ (n + m) ∈ Ideal.span (Set.range (mulNumerator s p))

Tactic:
simpa [pow_add, hc] using Ideal.mul_mem_left _ _ hy

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Lemmas

Goal state before:
pp: case succ
R : Type u_2
S : Type u_3
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : IsLocalization.Away x S
I J : Ideal R
hle : map (algebraMap R S) I ≤ map (algebraMap R S) J
hxJ : ∀ (y : R), x * y ∈ J → y ∈ J
y : R
hy : y ∈ I
n : ℕ
ih : x ^ n * y ∈ J → y ∈ J
h : x * (x ^ n * y) ∈ J
⊢ y ∈ J

Tactic:
exact ih <| hxJ _ h

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

Goal state before:
pp: ⊢ IsZariskiLocalAtTarget (topologically @SpecializingMap)

Tactic:
by
  apply topologically_isZariskiLocalAtTarget
  · introv _ _ hf
    rw [specializingMap_iff_closure_singleton_subset] at hf ⊢
    intro ⟨x, hx⟩ ⟨y, hy⟩ hcl
    simp only [closure_subtype, Set.restrictPreimage_mk, Set.image_singleton] at hcl
    obtain ⟨a, ha, hay⟩ := hf x hcl
    rw [← specializes_iff_mem_closure] at hcl
    exact ⟨⟨a, by simp [hay, hy]⟩, by simpa [closure_subtype], by simpa⟩
  · introv hU _ hsp
    simp_rw [specializingMap_iff_closure_singleton_subset] at hsp ⊢
    intro x y hy
    have : ∃ i, y ∈ U i := Opens.mem_iSup.mp (hU ▸ Opens.mem_top _)
    obtain ⟨i, hi⟩ := this
    rw [← specializes_iff_mem_closure] at hy
    have hfx : f x ∈ U i := (U i).2.stableUnderGeneralization hy hi
    have hy : (⟨y, hi⟩ : U i) ∈ closure {⟨f x, hfx⟩} := by
      simp only [closure_subtype, Set.image_singleton]
      rwa [← specializes_iff_mem_closure]
    obtain ⟨a, ha, hay⟩ := hsp i ⟨x, hfx⟩ hy
    rw [closure_subtype] at ha
    simp only [Opens.carrier_eq_coe, Set.image_singleton] at ha
    apply_fun Subtype.val at hay
    simp only [Opens.carrier_eq_coe, Set.restrictPreimage_coe] at hay
    use a.val, ha, hay

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

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
⊢ Q.diagonal f

Tactic:
rw [HasAffineProperty.diagonal_iff (targetAffineLocally Q)]
  let 𝒱 := Scheme.Pullback.openCoverOfLeftRight.{u} 𝒰 𝒰 f f
  have i1 : ∀ i, IsAffine (𝒱.X i) := fun i => by dsimp [𝒱]; infer_instance
  refine HasAffineProperty.of_openCover (P := targetAffineLocally Q) 𝒱 fun i ↦ ?_
  dsimp [𝒱, Scheme.Cover.pullbackHom]
  have : IsPullback (pullback.fst _ _ ≫ 𝒰.f _) (pullback.mapDesc (𝒰.f i.1) (𝒰.f i.2) f)
      (pullback.diagonal f) (pullback.map _ _ _ _ (𝒰.f _) (𝒰.f _) (𝟙 Y) (by simp) (by simp)) :=
    .of_iso (pullback_fst_map_snd_isPullback f (𝟙 _) (𝒰.f i.1 ≫ pullback.lift (𝟙 _) f)
      (𝒰.f i.2 ≫ pullback.lift (𝟙 _) f)) (asIso (pullback.map _ _ _ _ (𝟙 _) (𝟙 _)
      (pullback.fst _ _) (by simp) (by simp))) (.refl _) (pullback.congrHom (by simp) (by simp))
      (.refl _) (by simp) (by cat_disch) (by simp) (by cat_disch)
  rw [← Q.cancel_left_of_respectsIso this.isoPullback.hom, IsPullback.isoPullback_hom_snd]
  exact h𝒰 _ _

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

Goal state before:
pp: case e'_2
X : Scheme
U : X.Opens
s : Set ↑X.affineOpens
⊢ U = ⨆ i ∈ s, ↑i ↔ U.carrier = ⋃ i ∈ s, ↑↑i

Tactic:
· convert! SetLike.coe_injective.eq_iff.symm; simp

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

Goal state before:
pp: case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂],
    (fun X x x_1 x_2 ↦ CompactSpace ↥X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯
U V : ↑X.affineOpens
g : pullback (↑U).ι (↑V).ι ⟶ X := pullback.fst (↑U).ι (↑V).ι ≫ (↑U).ι
e : ↥(pullback (↑U).ι (↑V).ι) ≃ₜ ↑(↑↑U ∩ ↑↑V)
⊢ IsCompact (↑↑U ∩ ↑↑V)

Tactic:
isCompact_iff_compactSpace

Goal state after:
case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂],
    (fun X x x_1 x_2 ↦ CompactSpace ↥X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯
U V : ↑X.affineOpens
g : pullback (↑U).ι (↑V).ι ⟶ X := pullback.fst (↑U).ι (↑V).ι ≫ (↑U).ι
e : ↥(pullback (↑U).ι (↑V).ι) ≃ₜ ↑(↑↑U ∩ ↑↑V)
⊢ CompactSpace ↑(↑↑U ∩ ↑↑V)