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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : X - C η ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  ((X - C η) * P.eraseLead).coeffList =
    ((X - C η) * P.eraseLead).leadingCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)
⊢ ∃ c₀ cs,
    ((X - C η) * P).coeffList = P.leadingCoeff :: c₀ :: cs ∧ ((X - C η) * P.eraseLead).coeffList = P.nextCoeff :: cs

Tactic:
use nextCoeff ((X - C η) * P), .replicate n 0 ++ coeffList ((X - C η) * P.eraseLead).eraseLead

Goal state after:
case h
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : X - C η ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  ((X - C η) * P.eraseLead).coeffList =
    ((X - C η) * P.eraseLead).leadingCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)
⊢ ((X - C η) * P).coeffList =
      P.leadingCoeff ::
        ((X - C η) * P).nextCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList) ∧
    ((X - C η) * P.eraseLead).coeffList =
      P.nextCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case inr.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this✝ : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
⊢ Disjoint (range q) (Ico q (p.natDegree + 1))

Tactic:
rw [range_eq_Ico, disjoint_iff_inter_eq_empty, eq_empty_iff_forall_notMem]
    intro x hx
    rw [mem_inter, mem_Ico, mem_Ico] at hx
    exact hx.1.2.not_ge hx.2.1

Goal state after:
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
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
a✝ : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₁ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i =
    q₂ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₂ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
i : ι
hi : i ∈ s
⊢ ⊥ < (g i ^ n i).degree

Tactic:
rw [bot_lt_iff_ne_bot, degree_ne_bot]
      exact ((hg i hi).pow (n i)).ne_zero

Goal state after:
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
g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
hcoprime : IsCoprime g₁ g₂
q₁ q₂ r₁₁ r₁₂ r₂₁ r₂₂ : R[X]
hr₁₁ : r₁₁.degree < g₁.degree
hr₁₂ : r₁₂.degree < g₁.degree
hr₂₁ : r₂₁.degree < g₂.degree
hr₂₂ : r₂₂.degree < g₂.degree
hf : ↑q₁ + ↑r₁₁ / ↑g₁ + ↑r₂₁ / ↑g₂ = ↑q₂ + ↑r₁₂ / ↑g₁ + ↑r₂₂ / ↑g₂
g : Bool → R[X] := fun t ↦ Bool.rec g₂ g₁ t
r₁ : Bool → R[X] := fun t ↦ Bool.rec r₂₁ r₁₁ t
⊢ q₁ = q₂ ∧ r₁₁ = r₁₂ ∧ r₂₁ = r₂₂

Tactic:
let r₂ : Bool → R[X] := Bool.rec r₂₂ r₁₂

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
g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
hcoprime : IsCoprime g₁ g₂
q₁ q₂ r₁₁ r₁₂ r₂₁ r₂₂ : R[X]
hr₁₁ : r₁₁.degree < g₁.degree
hr₁₂ : r₁₂.degree < g₁.degree
hr₂₁ : r₂₁.degree < g₂.degree
hr₂₂ : r₂₂.degree < g₂.degree
hf : ↑q₁ + ↑r₁₁ / ↑g₁ + ↑r₂₁ / ↑g₂ = ↑q₂ + ↑r₁₂ / ↑g₁ + ↑r₂₂ / ↑g₂
g : Bool → R[X] := fun t ↦ Bool.rec g₂ g₁ t
r₁ : Bool → R[X] := fun t ↦ Bool.rec r₂₁ r₁₁ t
r₂ : Bool → R[X] := fun t ↦ Bool.rec r₂₂ r₁₂ t
⊢ q₁ = q₂ ∧ r₁₁ = r₁₂ ∧ r₂₁ = r₂₂
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 * 1 = a

Tactic:
rintro ⟨⟨⟩⟩
    simp only [mul_quot, ← one_quot, mul_one]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case refine_1
R : Type uR
inst✝⁵ : Semiring R
S : Type uS
inst✝⁴ : CommSemiring S
T : Type uT
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
r✝ : R → R → Prop
inst✝¹ : Semiring T
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h✝ : x ∈ Ideal.ofRel r
y a b : B
h : r a b
su : a - b = y
⊢ (mkRingHom r) b - (mkRingHom r) b = 0

Tactic:
sub_self

Goal state after:
case refine_1
R : Type uR
inst✝⁵ : Semiring R
S : Type uS
inst✝⁴ : CommSemiring S
T : Type uT
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
r✝ : R → R → Prop
inst✝¹ : Semiring T
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h✝ : x ∈ Ideal.ofRel r
y a b : B
h : r a b
su : a - b = y
⊢ 0 = 0
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a : αˢʸᵐ
⊢ ⅟2 * (2 * (unsym a * unsym a)) = unsym a * unsym a

Tactic:
invOf_mul_cancel_left

Goal state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a : αˢʸᵐ
⊢ unsym a * unsym a = unsym a * unsym a
Module: Mathlib.Algebra.Symmetrized

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

Tactic:
invOf_mul_cancel_left

Goal state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a : α
⊢ sym (a * a) = sym (a * a)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
f g : SkewMonoidAlgebra k G →+* k
h₁ : ∀ (b : k), f (single 1 b) = g (single 1 b)
h_of : ∀ (a : G), f (single a 1) = g (single a 1)
this : ∀ {a : G} {b₁ b₂ : k}, single 1 b₁ * single a b₂ = single a (b₁ * b₂)
a : G
b : k
⊢ ((fun f ↦ ↑f) f) (single a b) = ((fun f ↦ ↑f) g) (single a b)

Tactic:
← mul_one b,

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
f g : SkewMonoidAlgebra k G →+* k
h₁ : ∀ (b : k), f (single 1 b) = g (single 1 b)
h_of : ∀ (a : G), f (single a 1) = g (single a 1)
this : ∀ {a : G} {b₁ b₂ : k}, single 1 b₁ * single a b₂ = single a (b₁ * b₂)
a : G
b : k
⊢ ((fun f ↦ ↑f) f) (single a (b * 1)) = ((fun f ↦ ↑f) g) (single a (b * 1))
Module: Mathlib.Topology.Sheaves.Functors

Goal state before:
pp: case refine_2
C : Type u
inst✝⁸ : Category.{v, u} C
X Y : TopCat
f✝ : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
A : Type u_1
inst✝⁷ : Category.{w, u_1} A
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
FA : A → A → Type u_2
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasColimits A
inst✝³ : HasLimits A
inst✝² : PreservesLimits (CategoryTheory.forget A)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget A)
inst✝ : (CategoryTheory.forget A).ReflectsIsomorphisms
X✝ Y✝ : TopCat.Sheaf A Y
u : X✝ ⟶ Y✝
⊢ ((presheafToSheaf (Opens.grothendieckTopology ↑X) A).map (⋯.pullbackIso.hom.app ((Sheaf.forget A Y).obj X✝))).hom ≫
      ((presheafToSheaf (Opens.grothendieckTopology ↑X) A).map
            (⋯.functor.op.whiskerLeft ((Sheaf.forget A Y).map u))).hom ≫
        (ObjectProperty.homMk
            (sheafifyLift (Opens.grothendieckTopology ↑X) (𝟙 ((sheafPullback A hf).obj Y✝).obj) ⋯)).hom =
    ((presheafToSheaf (Opens.grothendieckTopology ↑X) A).map (⋯.pullbackIso.hom.app ((Sheaf.forget A Y).obj X✝))).hom ≫
      (ObjectProperty.homMk
            (sheafifyLift (Opens.grothendieckTopology ↑X) (𝟙 ((sheafPullback A hf).obj X✝).obj) ⋯)).hom ≫
        ((sheafPullback A hf).map u).hom

Tactic:
dsimp [sheafPullback, Functor.sheafPushforwardContinuous, Sheaf.forget]

Goal state after:
case refine_2
C : Type u
inst✝⁸ : Category.{v, u} C
X Y : TopCat
f✝ : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
A : Type u_1
inst✝⁷ : Category.{w, u_1} A
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
FA : A → A → Type u_2
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasColimits A
inst✝³ : HasLimits A
inst✝² : PreservesLimits (CategoryTheory.forget A)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget A)
inst✝ : (CategoryTheory.forget A).ReflectsIsomorphisms
X✝ Y✝ : TopCat.Sheaf A Y
u : X✝ ⟶ Y✝
⊢ ((presheafToSheaf (Opens.grothendieckTopology ↑X) A).map (⋯.pullbackIso.hom.app X✝.obj)).hom ≫
      ((presheafToSheaf (Opens.grothendieckTopology ↑X) A).map (⋯.functor.op.whiskerLeft u.hom)).hom ≫
        sheafifyLift (Opens.grothendieckTopology ↑X) (𝟙 (hf.functor.op ⋙ Y✝.obj)) ⋯ =
    ((presheafToSheaf (Opens.grothendieckTopology ↑X) A).map (⋯.pullbackIso.hom.app X✝.obj)).hom ≫
      sheafifyLift (Opens.grothendieckTopology ↑X) (𝟙 (hf.functor.op ⋙ X✝.obj)) ⋯ ≫ hf.functor.op.whiskerLeft u.hom
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T₁ : ↑X → Type u_2
T₂ : ↑X → Type u_3
T₃ : ↑X → Type u_4
P₁ : PrelocalPredicate T₁
P₂ : PrelocalPredicate T₂
P₃ : PrelocalPredicate T₃
op : {x : ↑X} → T₁ x → T₂ x → T₃ x
hop :
  ∀ {U V : Opens ↑X} {a : (x : ↥U) → T₁ ↑x} {b : (x : ↥V) → T₂ ↑x},
    P₁.pred a → P₂.pred b → ∀ (p : ↥(U ⊓ V)), ∃ W ia ib, ↑p ∈ W ∧ P₃.pred fun x ↦ op (a (ia x)) (b (ib x))
U : Opens ↑X
a : (x : ↥U) → T₁ ↑x
b : (x : ↥U) → T₂ ↑x
ha : P₁.sheafify.pred a
hb : P₂.sheafify.pred b
⊢ P₃.sheafify.pred fun x ↦ op (a x) (b x)

Tactic:
intro x
  rcases ha x with ⟨Va, ma, ia, ha⟩
  rcases hb x with ⟨Vb, mb, ib, hb⟩
  rcases hop ha hb ⟨x, ma, mb⟩ with ⟨W, sa, sb, hx, hw⟩
  exact ⟨W, hx, sa ≫ ia, hw⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
x✝ : ↑R
x' : ↥(unop (op ⊤))
⊢ ↑((CommRingCat.Hom.hom (toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op)) x✝) x' =
    ↑((CommRingCat.Hom.hom (f ≫ toSpecΓ S)) x✝) x'

Tactic:
erw [comap_apply]

Goal state after:
R S : CommRingCat
f : R ⟶ S
x✝ : ↑R
x' : ↥(unop (op ⊤))
⊢ (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f.op.unop) ↑x').asIdeal (↑x').asIdeal
        (CommRingCat.Hom.hom f.op.unop) ⋯)
      (↑((toSpecΓ R).hom' x✝) ⟨PrimeSpectrum.comap (CommRingCat.Hom.hom f.op.unop) ↑x', ⋯⟩) =
    ↑((CommRingCat.Hom.hom (f ≫ toSpecΓ S)) x✝) x'
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case app.op.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
carrier✝ : Set ↑↑(Y.restrict ⋯)
is_open'✝ : IsOpen carrier✝
⊢ ⇑(ConcreteCategory.hom f.base) ⁻¹' ↑((opensFunctor f).obj { carrier := carrier✝, is_open' := is_open'✝ }) = carrier✝

Tactic:
Set.preimage_image_eq _ H.base_open.injective

Goal state after:
case app.op.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
carrier✝ : Set ↑↑(Y.restrict ⋯)
is_open'✝ : IsOpen carrier✝
⊢ ↑{ carrier := carrier✝, is_open' := is_open'✝ } = carrier✝
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: R : CommRingCat
g : ↑R
⊢ ↑(opensRange (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away g))))) = ↑(PrimeSpectrum.basicOpen g)

Tactic:
exact PrimeSpectrum.localization_away_comap_range _ g

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

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : (Opens ↑↑X)ᵒᵖ
⊢ ((pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst).c ≫ Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf).app
      x =
    s.fst.c.app x

Tactic:
· induction x with | op x => ?_
    change ((_ ≫ _) ≫ _ ≫ _) ≫ _ = _
    simp_rw [Category.assoc]
    erw [← s.pt.presheaf.map_comp]
    erw [s.snd.c.naturality_assoc]
    have := congr_app s.condition (op (opensFunctor f |>.obj x))
    dsimp only [comp_c_app, unop_op] at this
    rw [← IsIso.comp_inv_eq] at this
    replace this := reassoc_of% this
    erw [← this, hf.invApp_app_assoc, s.fst.c.naturality_assoc]
    simp [eqToHom_map]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsOpenImmersion (pullback.fst g f)

Tactic:
by
  rw [← pullbackSymmetry_hom_comp_snd]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ IsOpenImmersion (pullback.fst g f)

Tactic:
by
  rw [← pullbackSymmetry_hom_comp_snd]
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : ↑Γ(X, U)
⊢ f ''ᵁ X.basicOpen r = Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r)

Tactic:
have e := Scheme.preimage_basicOpen f ((f.appIso U).inv r)
  rw [Scheme.Hom.appIso_inv_app_apply, Scheme.basicOpen_res, inf_eq_right.mpr _] at e
  · rw [← e, f.image_preimage_eq_opensRange_inf, inf_eq_right]
    refine Set.Subset.trans (Scheme.basicOpen_le _ _) (Set.image_subset_range _ _)
  · exact (X.basicOpen_le r).trans (f.preimage_image_eq _).ge

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsOpenImmersion (pullback.fst g f)

Tactic:
by
  rw [← pullbackSymmetry_hom_comp_snd]
  infer_instance

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

Goal state before:
pp: X : Scheme
a : ↥X
U : Set ↥X
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
haU : (X.affineCover.f (Cover.idx X.affineCover a)) x ∈ U
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
⊢ x ∈ U'

Tactic:
exact haU

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

Goal state before:
pp: case h_nhds.refine_1
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
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
s : ↑((fun x ↦ Classical.choose ⋯) (Cover.idx X.affineCover a))
hxV : x ∈ ↑(PrimeSpectrum.basicOpen s)
hVU : ↑(PrimeSpectrum.basicOpen s) ⊆ U'
⊢ a ∈ Set.range ⇑(X.affineBasisCover.f ⟨Cover.idx X.affineCover a, s⟩)

Tactic:
affineBasisCover_map_range

Goal state after:
case h_nhds.refine_1
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
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
s : ↑((fun x ↦ Classical.choose ⋯) (Cover.idx X.affineCover a))
hxV : x ∈ ↑(PrimeSpectrum.basicOpen s)
hVU : ↑(PrimeSpectrum.basicOpen s) ⊆ U'
⊢ a ∈ ⇑(X.affineCover.f (Cover.idx X.affineCover a)) '' (PrimeSpectrum.basicOpen s).carrier
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: case h_nhds.refine_2
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
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
s : ↑((fun x ↦ Classical.choose ⋯) (Cover.idx X.affineCover a))
hxV : x ∈ ↑(PrimeSpectrum.basicOpen s)
hVU : ↑(PrimeSpectrum.basicOpen s) ⊆ U'
⊢ Set.range ⇑(X.affineBasisCover.f ⟨Cover.idx X.affineCover a, s⟩) ⊆ U

Tactic:
affineBasisCover_map_range

Goal state after:
case h_nhds.refine_2
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
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
s : ↑((fun x ↦ Classical.choose ⋯) (Cover.idx X.affineCover a))
hxV : x ∈ ↑(PrimeSpectrum.basicOpen s)
hVU : ↑(PrimeSpectrum.basicOpen s) ⊆ U'
⊢ ⇑(X.affineCover.f (Cover.idx X.affineCover a)) '' (PrimeSpectrum.basicOpen s).carrier ⊆ U
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
R : CommRingCat
f g x : ↑R
hx : x = f * g
⊢ IsLocalization.Away (f * g) (Localization.Away x)

Tactic:
rw [hx]; infer_instance

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)) ⋯
⊢ f ∈ (Ideal.span (Set.range b)).radical

Tactic:
have : PrimeSpectrum.zeroLocus (Set.range b) ⊆ PrimeSpectrum.zeroLocus {f} := by
      simpa [← SetLike.coe_subset_coe, ← Set.compl_iInter,
        ← PrimeSpectrum.zeroLocus_iUnion, PrimeSpectrum.Top] using iU

Goal state after:
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)) ⋯
this : PrimeSpectrum.zeroLocus (Set.range b) ⊆ PrimeSpectrum.zeroLocus {f}
⊢ f ∈ (Ideal.span (Set.range b)).radical
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ (ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x ∈ basicOpen 1

Tactic:
rw [basicOpen_one]; trivial

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case e'_2
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
e_1✝ : Spec Γ(X, U) = Spec (CommRingCat.of ↑Γ(X, U))
⊢ PrimeSpectrum.basicOpen f =
    Scheme.Hom.opensRange (Spec.map (CommRingCat.ofHom (algebraMap (↑Γ(X, U)) (Localization.Away f))))

Tactic:
exact Opens.ext (PrimeSpectrum.localization_away_comap_range (Localization.Away f) f).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ (CommRingCat.ofHom (algebraMap R ((structureSheafInType R R).obj.obj (op ⊤))) ≫
        (structurePresheafInCommRingCat R).germ ⊤ y _root_.trivial) ≫
      (structureSheaf R).presheaf.stalkSpecializes h =
    CommRingCat.ofHom (algebraMap R ((structureSheafInType R R).obj.obj (op ⊤))) ≫
      (structurePresheafInCommRingCat R).germ ⊤ x _root_.trivial

Tactic:
simp [structureSheaf]

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ D.f' i j ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f i j hij

Tactic:
delta f'; aesop

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ D.f' i k ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f i k hik

Tactic:
delta f'; aesop

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ D.f j k hjk ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f' j k

Tactic:
delta f'; aesop

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ D.f j i ⋯ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f' j i

Tactic:
delta f'; aesop

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
⊢ D.t'' i j k ≫ pullback.snd (D.f' j k) (D.f' j i) =
    pullback.fst (D.f' i j) (D.f' i k) ≫ if h : i = j then eqToHom ⋯ else eqToHom ⋯ ≫ D.t i j h ≫ eqToHom ⋯

Tactic:
by
    delta GlueData'.t''
    obtain rfl | _ := eq_or_ne i j
    · simp
    obtain rfl | _ := eq_or_ne i k
    · simp [*]
    obtain rfl | _ := eq_or_ne j k
    · simp [*]
    · simp [*, reassoc_of% D.t_fac]

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
    ((ConcreteCategory.hom (sigmaIsoSigma D.U).hom)
      ((ConcreteCategory.hom
          (D.diagram.fstSigmaMapOfIsColimit (colimit.cocone (Discrete.functor D.diagram.right))
            (colimit.isColimit (Discrete.functor D.diagram.left))))
        ((ConcreteCategory.hom (Sigma.ι D.diagram.left (i, j))) y)))
    ((ConcreteCategory.hom (sigmaIsoSigma D.U).hom)
      ((ConcreteCategory.hom
          (D.diagram.sndSigmaMapOfIsColimit (colimit.cocone (Discrete.functor D.diagram.right))
            (colimit.isColimit (Discrete.functor D.diagram.left))))
        ((ConcreteCategory.hom (Sigma.ι D.diagram.left (i, j))) y)))

Tactic:
erw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, colimit.ι_desc_assoc,
      ← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, colimit.ι_desc_assoc]

Goal state after:
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
    ((ConcreteCategory.hom
        ((Cofan.mk (colimit.cocone (Discrete.functor D.diagram.right)).pt fun i ↦
                  D.diagram.fst i ≫
                    Cofan.inj (colimit.cocone (Discrete.functor D.diagram.right))
                      ((MultispanShape.prod D.J).fst i)).ι.app
            { as := (i, j) } ≫
          (sigmaIsoSigma D.U).hom))
      y)
    ((ConcreteCategory.hom
        ((Cofan.mk (colimit.cocone (Discrete.functor D.diagram.right)).pt fun i ↦
                  D.diagram.snd i ≫
                    Cofan.inj (colimit.cocone (Discrete.functor D.diagram.right))
                      ((MultispanShape.prod D.J).snd i)).ι.app
            { as := (i, j) } ≫
          (sigmaIsoSigma D.U).hom))
      y)