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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hgid : g i ∣ r₂ i - r₁ i
hf : g i * ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x = (r₂ i - r₁ i - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
hpgd : ∏ i ∈ s, g i ∣ ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x
hdr : (r₂ i - r₁ i).degree < (g i).degree
hr0 : r₂ i - r₁ i = 0
hpm : (∏ i ∈ s, g i).Monic
j : ι
hj : j ∈ s
dnb : (∏ k ∈ s.erase j, g k).degree ≠ ⊥
⊢ (∏ k ∈ s.erase j, g k).degree + (r₁ j - r₂ j).degree < (∏ x ∈ s.erase j, g x).degree + (g j).degree

Tactic:
WithBot.add_lt_add_iff_left dnb

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hgid : g i ∣ r₂ i - r₁ i
hf : g i * ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x = (r₂ i - r₁ i - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
hpgd : ∏ i ∈ s, g i ∣ ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x
hdr : (r₂ i - r₁ i).degree < (g i).degree
hr0 : r₂ i - r₁ i = 0
hpm : (∏ i ∈ s, g i).Monic
j : ι
hj : j ∈ s
dnb : (∏ k ∈ s.erase j, g k).degree ≠ ⊥
⊢ (r₁ j - r₂ j).degree < (g j).degree
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case succ.inr.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : ∀ m < d + 1, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : SignType.sign P.nextCoeff = 1
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations

Tactic:
have h₁ : nextCoeff P ≠ 0 := by simp [← sign_ne_zero, hs_nC]
    specialize ih _ h_ih (mt nextCoeff_eq_zero_of_eraseLead_eq_zero h₁) rfl
    have : P.signVariations = P.eraseLead.signVariations + ?_ := by
      simp [signVariations_eq_eraseLead_add_ite hP, leadingCoeff_eraseLead_eq_nextCoeff h₁,
        hs_nC, h_lC]
      exact rfl

Goal state after:
case succ.inr.inr.refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : P.eraseLead.signVariations + 1 ≤ ((X - C η) * P.eraseLead).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : SignType.sign P.nextCoeff = 1
h₁ : P.nextCoeff ≠ 0
this : P.signVariations = P.eraseLead.signVariations + 0
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case succ.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : ∀ m < d + 1, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : SignType.sign P.nextCoeff = -1
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations

Tactic:
have h₁ : nextCoeff P ≠ 0 := by simp [← sign_ne_zero, hs_nC]
    specialize ih _ h_ih (mt nextCoeff_eq_zero_of_eraseLead_eq_zero h₁) rfl
    have : P.signVariations = P.eraseLead.signVariations + ?_ := by
      simp [signVariations_eq_eraseLead_add_ite hP, leadingCoeff_eraseLead_eq_nextCoeff h₁,
        hs_nC, h_lC]
      exact rfl

Goal state after:
case succ.inl.refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : P.eraseLead.signVariations + 1 ≤ ((X - C η) * P.eraseLead).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : SignType.sign P.nextCoeff = -1
h₁ : P.nextCoeff ≠ 0
this : P.signVariations = P.eraseLead.signVariations + 1
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
⊢ inst₁ = inst₂

Tactic:
have h_monoid : inst₁.toAddMonoid = inst₂.toAddMonoid := by ext : 1; exact h_add
  have h_zero' : inst₁.toZero = inst₂.toZero := congrArg (·.toZero) h_monoid
  have h_one' : inst₁.toOne = inst₂.toOne :=
    congrArg One.mk h_one
  have h_natCast : inst₁.toNatCast.natCast = inst₂.toNatCast.natCast := by
    funext n; induction n with
    | zero => rewrite [inst₁.natCast_zero, inst₂.natCast_zero]
              exact congrArg (@Zero.zero R) h_zero'
    | succ n h => rw [inst₁.natCast_succ, inst₂.natCast_succ, h_add]
                  exact congrArg₂ _ h h_one
  rcases inst₁ with @⟨⟨⟩⟩; rcases inst₂ with @⟨⟨⟩⟩
  congr

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

Goal state before:
pp: R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne
this : inst₁.toNatCast = inst₂.toNatCast
toAddMonoid_eq✝ : inst₁.toAddMonoid = inst₂.toAddMonoid
toNeg_eq✝ : inst₁.toNeg = inst₂.toNeg
toSub_eq✝ : inst₁.toSub = inst₂.toSub
toZSMul_eq✝ : inst₁.toZSMul = inst₂.toZSMul
n : ℤ
⊢ IntCast.intCast n = IntCast.intCast n

Tactic:
cases n with

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
x a✝ s✝ : R
ha : a✝ ≠ 0
hs : IsSumNonzeroSq s✝
ih : s✝ ∈ closure {x | ∃ x_1, x_1 ≠ 0 ∧ x_1 * x_1 = x}
⊢ a✝ * a✝ + s✝ ∈ closure {x | ∃ x_1, x_1 ≠ 0 ∧ x_1 * x_1 = x}

Tactic:
| sq_add ha hs ih =>

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

Goal state before:
pp: case sq_add
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
h : ∀ {s a : R}, IsSumSq s → a * a + s = 0 → a = 0
x a✝ s✝ : R
ha : a✝ ≠ 0
hs : IsSumNonzeroSq s✝
ih : s✝ ≠ 0
⊢ a✝ * a✝ + s✝ ≠ 0

Tactic:
| sq_add ha hs ih =>

Goal state after:
Module: Mathlib.Algebra.Ring.Semireal.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : IsSemireal R
n : ℕ
hn : ↑n = 0
⊢ n = 0

Tactic:
cases n with

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 → R → Prop
⊢ ∀ (a : RingQuot r), a * 0 = 0

Tactic:
by
    rintro ⟨⟨⟩⟩
    simp only [mul_quot, ← zero_quot, mul_zero]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
⊢ ((monomial n) a).support ⊆ {n}

Tactic:
simp only [monomial_def, support_eq_skewMonoidAlgebra_support]

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
⊢ Finset.map toAdd.toEmbedding (single (ofAdd n) a).support ⊆ {n}
Module: Mathlib.Algebra.Tropical.Basic

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

Tactic:
induction n with
  | zero => simp [one_nsmul]
  | succ n IH => rw [add_nsmul, IH, one_nsmul, add_self]

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a : α
⊢ sym (a * a) = sym a * sym a

Tactic:
by
  rw [sym_mul_sym, ← two_mul, invOf_mul_cancel_left]

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: case calc_1
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ sym
      (⅟2 * ⅟2 *
        (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) +
          (unsym (a * a) * (unsym a * unsym b) + unsym (a * a) * (unsym b * unsym a)))) =
    sym
      (⅟2 * ⅟2 *
        (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
          unsym (a * a) * unsym b * unsym a))

Tactic:
← add_assoc,

Goal state after:
case calc_1
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ sym
      (⅟2 * ⅟2 *
        (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * (unsym a * unsym b) +
          unsym (a * a) * (unsym b * unsym a))) =
    sym
      (⅟2 * ⅟2 *
        (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
          unsym (a * a) * unsym b * unsym a))
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ⅟2 * ⅟2 *
      (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
        unsym (a * a) * unsym b * unsym a) =
    ⅟2 * ⅟2 *
      (unsym a * (unsym b * unsym (a * a)) + unsym a * (unsym (a * a) * unsym b) +
        (unsym b * unsym (a * a) * unsym a + unsym (a * a) * unsym b * unsym a))

Tactic:
← add_assoc,

Goal state after:
case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ⅟2 * ⅟2 *
      (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
        unsym (a * a) * unsym b * unsym a) =
    ⅟2 * ⅟2 *
      (unsym a * (unsym b * unsym (a * a)) + unsym a * (unsym (a * a) * unsym b) + unsym b * unsym (a * a) * unsym a +
        unsym (a * a) * unsym b * unsym a)
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 : ℤ
⊢ coeff A n = coeff A (-(-n - 1) - 1)

Tactic:
neg_sub,

Goal state after:
R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
A : VertexOperator R V
n : ℤ
⊢ coeff A n = coeff A (1 - -n - 1)
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : InvolutiveStar R
inst✝³ : AddCommMonoid E
inst✝² : Module R E
inst✝¹ : StarAddMonoid E
inst✝ : StarModule R E
f : WithConv (End R E)
hf : IsUnit f.ofConv
⊢ IsUnit (star f).ofConv

Tactic:
by
  have ⟨u, hu⟩ := hf
  have : IsUnit (star (toConv (u : End R E))).ofConv := (star (toConv u)).ofConv.isUnit
  simpa [hu] using this

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 ≫ Presheaf.pushforwardToOfIso ((forget C).mapIso H).symm H.inv.c).app (op U) = (𝟙 Y.presheaf).app (op U)

Tactic:
NatTrans.comp_app

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
this✝ : ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)
this : IsIso f.c
x : ↑↑Y
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom f.base)

Tactic:
by rw [Set.range_eq_univ.mpr ((TopCat.epi_iff_surjective _).mp h')]; trivial

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
R : CommRingCat
f : ↑R
⊢ IsOpenImmersion (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away f))))

Tactic:
by
  apply SheafedSpace.IsOpenImmersion.of_stalk_iso (H := ?_)
  · exact (PrimeSpectrum.localization_away_isOpenEmbedding (Localization.Away f) f :)
  · intro x
    exact isIso_SpecMap_stakMap_localization R (Submonoid.powers f) x

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X U Y : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
H : Set.range ⇑f ⊆ Set.range ⇑g
⊢ IsPullback (lift g f H) (𝟙 X) g f

Tactic:
convert! IsPullback.of_id_snd.paste_horiz (IsKernelPair.id_of_mono g)
  · exact (Category.comp_id _).symm
  · simp

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasLimits C
ι✝ : Type v
F✝ : Discrete ι✝ ⥤ SheafedSpace C
inst✝³ : HasColimit F✝
i✝ : Discrete ι✝
ι : Type w
inst✝² : Small.{v, w} ι
F : Discrete ι ⥤ SheafedSpace C
inst✝¹ : HasColimit F
i : Discrete ι
inst✝ : HasStrictTerminalObjects C
ι' : Type v
e : ι ≃ ι'
f : Discrete ι' ≌ Discrete ι := Discrete.equivalence e.symm
⊢ IsOpenImmersion (colimit.ι F i)

Tactic:
have : colimit.ι F i = (colimit.ι F i ≫ (HasColimit.isoOfEquivalence f (Iso.refl _)).inv) ≫
      (HasColimit.isoOfEquivalence f (Iso.refl _)).hom := by
    simp

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasLimits C
ι✝ : Type v
F✝ : Discrete ι✝ ⥤ SheafedSpace C
inst✝³ : HasColimit F✝
i✝ : Discrete ι✝
ι : Type w
inst✝² : Small.{v, w} ι
F : Discrete ι ⥤ SheafedSpace C
inst✝¹ : HasColimit F
i : Discrete ι
inst✝ : HasStrictTerminalObjects C
ι' : Type v
e : ι ≃ ι'
f : Discrete ι' ≌ Discrete ι := Discrete.equivalence e.symm
this :
  colimit.ι F i =
    (colimit.ι F i ≫ (HasColimit.isoOfEquivalence f (Iso.refl (f.functor ⋙ F))).inv) ≫
      (HasColimit.isoOfEquivalence f (Iso.refl (f.functor ⋙ F))).hom
⊢ IsOpenImmersion (colimit.ι F i)
Module: Mathlib.AlgebraicGeometry.Restrict

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

Tactic:
basicOpen_res_eq,

Goal state after:
X : Scheme
U : X.Opens
r : ↑Γ(X, U)
⊢ X.basicOpen ((ConcreteCategory.hom U.topIso.inv) r) = X.basicOpen r
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq : (toBasicOpenₗ R M f) (LocalizedModule.mk a b) = (toBasicOpenₗ R M f) (LocalizedModule.mk c d)
this : f ∈ (⊥.colon {d • a - b • c}).radical
⊢ LocalizedModule.mk a b = LocalizedModule.mk c d

Tactic:
rw [LocalizedModule.mk_eq]

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq : (toBasicOpenₗ R M f) (LocalizedModule.mk a b) = (toBasicOpenₗ R M f) (LocalizedModule.mk c d)
this : f ∈ (⊥.colon {d • a - b • c}).radical
⊢ ∃ u, u • d • a = u • b • c
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case h.h
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq : const a (↑b) (basicOpen f) ⋯ = const c (↑d) (basicOpen f) ⋯
p : PrimeSpectrum R
hfp : f ∉ p.asIdeal
u : ↥(↑⟨p, hfp⟩).asIdeal.primeCompl
hu : u • ⟨↑d, ⋯⟩ • a = u • ⟨↑b, ⋯⟩ • c
⊢ p ∉ PrimeSpectrum.zeroLocus ↑(⊥.colon {d • a - b • c})

Tactic:
PrimeSpectrum.mem_zeroLocus,

Goal state after:
case h.h
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq : const a (↑b) (basicOpen f) ⋯ = const c (↑d) (basicOpen f) ⋯
p : PrimeSpectrum R
hfp : f ∉ p.asIdeal
u : ↥(↑⟨p, hfp⟩).asIdeal.primeCompl
hu : u • ⟨↑d, ⋯⟩ • a = u • ⟨↑b, ⋯⟩ • c
⊢ ¬↑(⊥.colon {d • a - b • c}) ⊆ ↑p.asIdeal
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: ⊢ PreservesLimits forgetToScheme

Tactic:
by
  apply +allowSynthFailures @preservesLimits_of_natIso _ _ _ _ _ _
    (Functor.isoWhiskerRight equivCommRingCat.unitIso forgetToScheme).symm
  change PreservesLimits (equivCommRingCat.functor ⋙ Scheme.Spec)
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
𝒰 : X.OpenCover
U : X.Opens
i : 𝒰.I₀
⊢ 𝒰.f i ∣_ U =
    (IsOpenImmersion.isoOfRangeEq (𝒰.f i ⁻¹ᵁ U).ι (pullback.snd U.ι (𝒰.f ((Equiv.refl 𝒰.I₀) i))) ⋯).hom ≫
      (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).f ((Equiv.refl 𝒰.I₀) i)

Tactic:
rw [← cancel_mono U.ι]

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
𝒰 : X.OpenCover
U : X.Opens
i : 𝒰.I₀
⊢ 𝒰.f i ∣_ U ≫ U.ι =
    ((IsOpenImmersion.isoOfRangeEq (𝒰.f i ⁻¹ᵁ U).ι (pullback.snd U.ι (𝒰.f ((Equiv.refl 𝒰.I₀) i))) ⋯).hom ≫
        (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).f ((Equiv.refl 𝒰.I₀) i)) ≫
      U.ι
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: case w
R : CommRingCat
p : PrimeSpectrum ↑R
⊢ (TopCat.Hom.hom (Spec.topMap (toSpecΓ R))) ((TopCat.Hom.hom (Spec.locallyRingedSpaceObj R).toΓSpecBase) p) = p

Tactic:
refine PrimeSpectrum.ext (Ideal.ext fun x => ?_)

Goal state after:
case w
R : CommRingCat
p : PrimeSpectrum ↑R
x : ↑R
⊢ x ∈
      ((TopCat.Hom.hom (Spec.topMap (toSpecΓ R)))
          ((TopCat.Hom.hom (Spec.locallyRingedSpaceObj R).toΓSpecBase) p)).asIdeal ↔
    x ∈ p.asIdeal
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
y : PrimeSpectrum ↑Γ(X, U)
hy : hU.fromSpec y ∈ U
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk (hU.fromSpec y))) y.asIdeal

Tactic:
apply
    (@IsLocalization.isLocalization_iff_of_ringEquiv (R := Γ(X, U))
      (S := X.presheaf.stalk (hU.fromSpec y)) _ y.asIdeal.primeCompl _
      (TopCat.Presheaf.algebra_section_stalk X.presheaf ⟨hU.fromSpec y, hy⟩) _ _
      (asIso <| hU.fromSpec.stalkMap y).commRingCatIsoToRingEquiv).mpr
  convert StructureSheaf.IsLocalization.to_stalk Γ(X, U) y
  delta IsLocalization.AtPrime StructureSheaf.stalkAlgebra
  congr!
  simp [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp, IsAffineOpen.fromSpec_app_self]
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
x : R
⊢ (comap f (basicOpen x) (basicOpen (f x)) ⋯).comp (algebraMap R ↑((structureSheaf R).obj.obj (op (basicOpen x)))) =
    (IsLocalization.map (↑((structureSheaf S).obj.obj (op (basicOpen (f x))))) f ⋯).comp
      (algebraMap R ↑((structureSheaf R).obj.obj (op (basicOpen x))))

Tactic:
simpa [CommRingCat.hom_ext_iff] using! toOpen_comp_comap f _

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⋃ i, (PrimeSpectrum.basicOpen ↑i).carrier = Set.univ ↔ Ideal.span s = ⊤

Tactic:
· simp only [Opens.carrier_eq_coe, PrimeSpectrum.basicOpen_eq_zeroLocus_compl]
    rw [← Set.compl_iInter, Set.compl_univ_iff, ← PrimeSpectrum.zeroLocus_iUnion, ←
      PrimeSpectrum.zeroLocus_empty_iff_eq_top, PrimeSpectrum.zeroLocus_span]
    simp only [Set.iUnion_singleton_eq_range, Subtype.range_val_subtype, Set.ofPred_mem_eq]

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mp
D : GlueData
i✝ j✝ : D.J
x : ↑(D.U i✝)
y✝ : ↑(D.U j✝)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i✝ ≫ Multicoequalizer.sigmaπ D.diagram)) x =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j✝ ≫ Multicoequalizer.sigmaπ D.diagram)) y✝
i j : D.J
y : ↑(D.diagram.left (i, j))
⊢ D.Rel ⟨(MultispanShape.prod D.J).fst { as := (i, j) }.as, (D.diagram.fst { as := (i, j) }.as).hom' y⟩
    ⟨(MultispanShape.prod D.J).snd { as := (i, j) }.as, (D.diagram.snd { as := (i, j) }.as).hom' y⟩

Tactic:
exact ⟨y, ⟨rfl, rfl⟩⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
r : ↑Γ(X, U)
⊢ U.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = U.ι ⁻¹ᵁ X.basicOpen r

Tactic:
dsimp [toSpecΓ]
  simp only [Scheme.toSpecΓ_preimage_basicOpen, preimage_basicOpen, ι_app, homOfLE_leOfHom]
  rw [← Scheme.basicOpen_res_eq _ _ (eqToHom U.ι_preimage_self.symm).op,
    ← ConcreteCategory.comp_apply]
  congr 3
  simp [← Functor.map_comp]
  rfl

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
h : MkCore
i j k : h.J
x : ↑(h.U i)
hx : x ∈ h.V i j
hx' : x ∈ h.V i k
⊢ ↑((ConcreteCategory.hom (h.t k i))
          ⟨↑((ConcreteCategory.hom (h.t j k)) ⟨↑((ConcreteCategory.hom (h.t i j)) ⟨x, hx⟩), ⋯⟩), ⋯⟩) =
      x ∧
    ↑((ConcreteCategory.hom (h.t k i))
          ⟨↑((ConcreteCategory.hom (h.t j k)) ⟨↑((ConcreteCategory.hom (h.t i j)) ⟨x, hx⟩), ⋯⟩), ⋯⟩) =
      ↑⟨x, hx'⟩

Tactic:
and_self_iff

Goal state after:
D : GlueData
h : MkCore
i j k : h.J
x : ↑(h.U i)
hx : x ∈ h.V i j
hx' : x ∈ h.V i k
⊢ ↑((ConcreteCategory.hom (h.t k i))
        ⟨↑((ConcreteCategory.hom (h.t j k)) ⟨↑((ConcreteCategory.hom (h.t i j)) ⟨x, hx⟩), ⋯⟩), ⋯⟩) =
    x