mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.Subgroup

Goal state before:
pp: R : Type u_1
M✝ : Type u_2
inst✝ : NonUnitalNonAssocRing R
M N : AddSubgroup R
x✝ : R
h : x✝ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
r₁ r₂ : R
h₁ : -r₁ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
h₂ : -r₂ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
⊢ -(r₁ + r₂) ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier

Tactic:
rw [neg_add]

Goal state after:
R : Type u_1
M✝ : Type u_2
inst✝ : NonUnitalNonAssocRing R
M N : AddSubgroup R
x✝ : R
h : x✝ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
r₁ r₂ : R
h₁ : -r₁ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
h₂ : -r₂ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
⊢ -r₁ + -r₂ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝ : Semiring R
r : R → R → Prop
a b c : R
h : Rel r b c
⊢ Rel r (a + b) (a + c)

Tactic:
rw [add_comm a b, add_comm a c]

Goal state after:
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
a b c : R
h : Rel r b c
⊢ Rel r (b + a) (c + a)
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝⁴ : Semiring R
S : Type uS
inst✝³ : CommSemiring S
T : Type uT
A : Type uA
inst✝² : Semiring A
inst✝¹ : Algebra S A
r✝ : R → R → Prop
inst✝ : Semiring T
r : R → R → Prop
f : R →+* T
h : ∀ ⦃x y : R⦄, r x y → f x = f y
⊢ ∀ (x y : RingQuot r), Quot.lift ⇑f ⋯ (x * y).toQuot = Quot.lift ⇑f ⋯ x.toQuot * Quot.lift ⇑f ⋯ y.toQuot

Tactic:
rintro ⟨⟨x⟩⟩ ⟨⟨y⟩⟩

Goal state after:
case mk.mk
R : Type uR
inst✝⁴ : Semiring R
S : Type uS
inst✝³ : CommSemiring S
T : Type uT
A : Type uA
inst✝² : Semiring A
inst✝¹ : Algebra S A
r✝ : R → R → Prop
inst✝ : Semiring T
r : R → R → Prop
f : R →+* T
h : ∀ ⦃x y : R⦄, r x y → f x = f y
toQuot✝¹ : Quot (Rel r)
x : R
toQuot✝ : Quot (Rel r)
y : R
⊢ Quot.lift ⇑f ⋯ ({ toQuot := Quot.mk (Rel r) x } * { toQuot := Quot.mk (Rel r) y }).toQuot =
    Quot.lift ⇑f ⋯ { toQuot := Quot.mk (Rel r) x }.toQuot * Quot.lift ⇑f ⋯ { toQuot := Quot.mk (Rel r) y }.toQuot
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝⁴ : Semiring R
S : Type uS
inst✝³ : CommSemiring S
T : Type uT
A : Type uA
inst✝² : Semiring A
inst✝¹ : Algebra S A
r✝ : R → R → Prop
inst✝ : Semiring T
r : R → R → Prop
f : R →+* T
h : ∀ ⦃x y : R⦄, r x y → f x = f y
⊢ ∀ (x y : RingQuot r), Quot.lift ⇑f ⋯ (x + y).toQuot = Quot.lift ⇑f ⋯ x.toQuot + Quot.lift ⇑f ⋯ y.toQuot

Tactic:
rintro ⟨⟨x⟩⟩ ⟨⟨y⟩⟩

Goal state after:
case mk.mk
R : Type uR
inst✝⁴ : Semiring R
S : Type uS
inst✝³ : CommSemiring S
T : Type uT
A : Type uA
inst✝² : Semiring A
inst✝¹ : Algebra S A
r✝ : R → R → Prop
inst✝ : Semiring T
r : R → R → Prop
f : R →+* T
h : ∀ ⦃x y : R⦄, r x y → f x = f y
toQuot✝¹ : Quot (Rel r)
x : R
toQuot✝ : Quot (Rel r)
y : R
⊢ Quot.lift ⇑f ⋯ ({ toQuot := Quot.mk (Rel r) x } + { toQuot := Quot.mk (Rel r) y }).toQuot =
    Quot.lift ⇑f ⋯ { toQuot := Quot.mk (Rel r) x }.toQuot + Quot.lift ⇑f ⋯ { toQuot := Quot.mk (Rel r) y }.toQuot
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝¹ : Semiring R
T : Type uT
inst✝ : Semiring T
f : R →+* T
r : R → R → Prop
w : ∀ ⦃x y : R⦄, r x y → f x = f y
x : R
⊢ (lift ⟨f, w⟩) ((mkRingHom r) x) = f x

Tactic:
simp_rw [lift_def, preLift_def, mkRingHom_def]
  rfl

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝⁶ : Semiring R
S : Type uS
inst✝⁵ : CommSemiring S
T : Type uT
A : Type uA
inst✝⁴ : Semiring A
inst✝³ : Algebra S A
r : R → R → Prop
inst✝² : Semiring T
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f : A →ₐ[S] B
h : ∀ ⦃x y : A⦄, s x y → f x = f y
⊢ ∀ (x y : RingQuot s), Quot.lift ⇑f ⋯ (x * y).toQuot = Quot.lift ⇑f ⋯ x.toQuot * Quot.lift ⇑f ⋯ y.toQuot

Tactic:
rintro ⟨⟨x⟩⟩ ⟨⟨y⟩⟩

Goal state after:
case mk.mk
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 u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f : A →ₐ[S] B
h : ∀ ⦃x y : A⦄, s x y → f x = f y
toQuot✝¹ : Quot (Rel s)
x : A
toQuot✝ : Quot (Rel s)
y : A
⊢ Quot.lift ⇑f ⋯ ({ toQuot := Quot.mk (Rel s) x } * { toQuot := Quot.mk (Rel s) y }).toQuot =
    Quot.lift ⇑f ⋯ { toQuot := Quot.mk (Rel s) x }.toQuot * Quot.lift ⇑f ⋯ { toQuot := Quot.mk (Rel s) y }.toQuot
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝⁶ : Semiring R
S : Type uS
inst✝⁵ : CommSemiring S
T : Type uT
A : Type uA
inst✝⁴ : Semiring A
inst✝³ : Algebra S A
r : R → R → Prop
inst✝² : Semiring T
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f : A →ₐ[S] B
h : ∀ ⦃x y : A⦄, s x y → f x = f y
⊢ ∀ (x y : RingQuot s), Quot.lift ⇑f ⋯ (x + y).toQuot = Quot.lift ⇑f ⋯ x.toQuot + Quot.lift ⇑f ⋯ y.toQuot

Tactic:
rintro ⟨⟨x⟩⟩ ⟨⟨y⟩⟩

Goal state after:
case mk.mk
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 u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f : A →ₐ[S] B
h : ∀ ⦃x y : A⦄, s x y → f x = f y
toQuot✝¹ : Quot (Rel s)
x : A
toQuot✝ : Quot (Rel s)
y : A
⊢ Quot.lift ⇑f ⋯ ({ toQuot := Quot.mk (Rel s) x } + { toQuot := Quot.mk (Rel s) y }).toQuot =
    Quot.lift ⇑f ⋯ { toQuot := Quot.mk (Rel s) x }.toQuot + Quot.lift ⇑f ⋯ { toQuot := Quot.mk (Rel s) y }.toQuot
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
n : ℕ
⊢ p.update n 0 = erase n p

Tactic:
by
  ext; simp [Function.update_apply]

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

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
x✝ : ∃ y, y • 1 = star ↑v * ↑u
y : S
h : y • 1 = star ↑v * ↑u
huv : ↑u = y • ↑v
hvu : ↑v = star y • ↑u
this : ↑v = 0
⊢ u = 1 • v

Tactic:
ext; simp [this, huv] at huv ⊢

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : AddMonoidWithOne α
inst✝¹ : Invertible 2
a : α
inst✝ : Invertible a
⊢ sym (⅟2 * (⅟a * a + a * ⅟a)) = 1

Tactic:
mul_invOf_self,

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : AddMonoidWithOne α
inst✝¹ : Invertible 2
a : α
inst✝ : Invertible a
⊢ sym (⅟2 * (⅟a * a + 1)) = 1
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : AddMonoidWithOne α
inst✝¹ : Invertible 2
a : α
inst✝ : Invertible a
⊢ sym (⅟2 * (a * ⅟a + ⅟a * a)) = 1

Tactic:
mul_invOf_self,

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : AddMonoidWithOne α
inst✝¹ : Invertible 2
a : α
inst✝ : Invertible a
⊢ sym (⅟2 * (1 + ⅟a * a)) = 1
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Group G
inst✝ : MulSemiringAction G k
f g : SkewMonoidAlgebra k G
x : G
⊢ (f * g).coeff x = f.sum fun a b ↦ (single a b * g).coeff x

Tactic:
rw [← coeff_sum, ← sum_mul g f, f.sum_single]

Goal state after:
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:
unsym_mul_self

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 * unsym a) + unsym b * unsym a * (unsym a * unsym a) +
          unsym a * unsym a * unsym a * unsym b +
        unsym a * unsym a * unsym b * unsym a) =
    ⅟2 * ⅟2 *
      (unsym a * unsym b * (unsym a * unsym a) + unsym a * (unsym a * unsym a) * unsym b +
          unsym b * (unsym a * unsym a) * unsym a +
        unsym a * unsym a * unsym b * unsym a)
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
F : J ⥤ PresheafedSpace C
inst✝ : HasColimit F
U : Opens ↑↑(colimit F)
j k : Jᵒᵖ
f : j ⟶ k
⊢ (Opens.map (F.map f.unop).base).op.obj (op ((Opens.map (colimit.ι F (unop j)).base).obj U)) =
    op ((Opens.map (colimit.ι F (unop k)).base).obj U)

Tactic:
rw [← colimit.w F f.unop, comp_base]; rfl

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

Goal state before:
pp: X Y : LocallyRingedSpace
e : X ≅ Y
x : ↑X.toTopCat
⊢ (ConcreteCategory.hom e.inv.base) ((ConcreteCategory.hom e.hom.base) x) = x

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

Goal state after:
X Y : LocallyRingedSpace
e : X ≅ Y
x : ↑X.toTopCat
⊢ (ConcreteCategory.hom (e.hom.base ≫ e.inv.base)) x = (ConcreteCategory.hom (𝟙 X.toPresheafedSpace).base) x
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.hom.base = β.hom.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ α.hom.c.app (op U)) ≫
        X.presheaf.map (eqToHom ⋯) =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ β.hom.c.app (op U)
r : ↑R
⊢ (α.hom.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf).app (op (PrimeSpectrum.basicOpen r)) =
    β.hom.c.app (op (PrimeSpectrum.basicOpen r))

Tactic:
apply (StructureSheaf.to_basicOpen_epi R r).1

Goal state after:
case h
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.hom.base = β.hom.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ α.hom.c.app (op U)) ≫
        X.presheaf.map (eqToHom ⋯) =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ β.hom.c.app (op U)
r : ↑R
⊢ CommRingCat.ofHom (algebraMap ↑R ↑((structureSheaf ↑R).obj.obj (op (PrimeSpectrum.basicOpen r)))) ≫
      (α.hom.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf).app (op (PrimeSpectrum.basicOpen r)) =
    CommRingCat.ofHom (algebraMap ↑R ↑((structureSheaf ↑R).obj.obj (op (PrimeSpectrum.basicOpen r)))) ≫
      β.hom.c.app (op (PrimeSpectrum.basicOpen r))
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 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s : PullbackCone f g
U : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
s' : PullbackCone f.base g.base := PullbackCone.mk s.fst.base s.snd.base ⋯
this : limit.lift (cospan f.base g.base) s' ≫ limit.π (cospan f.base g.base) WalkingCospan.right = s.snd.base
| ⇑(ConcreteCategory.hom s.snd.base) ⁻¹' ↑(⋯.functor.obj (unop U))

Tactic:
rw [← this]
                  dsimp [s']
                  rw [Function.comp_def, ← Set.preimage_preimage]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s : PullbackCone f g
U : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
s' : PullbackCone f.base g.base := PullbackCone.mk s.fst.base s.snd.base ⋯
this : limit.lift (cospan f.base g.base) s' ≫ limit.π (cospan f.base g.base) WalkingCospan.right = s.snd.base
| ⇑(TopCat.Hom.hom (limit.lift (cospan f.base g.base) (PullbackCone.mk s.fst.base s.snd.base ⋯))) ⁻¹'
    ⇑(TopCat.Hom.hom (limit.π (cospan f.base g.base) WalkingCospan.right)) ⁻¹'
      ⇑(ConcreteCategory.hom (pullback.snd f.base g.base)) '' ↑(unop U)
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: case refine_1
X : Type u
ι : Type u_1
Y✝ : ι → Type u
f : (i : ι) → Y✝ i ⟶ X
h : Presieve.ofArrows Y✝ f ∈ jointlySurjectivePrecoverage.coverings X
x : (fun X ↦ X) X
Y : Type u
i : ι
hx : x ∈ Set.range ⇑(ConcreteCategory.hom (f i))
⊢ ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (f i))

Tactic:
use i

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison F f g))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : ∀ (x : (fun X ↦ X) (F.obj S)), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
x : F.obj Y
i : ι
hi : (ConcreteCategory.hom (F.map g)) x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
this : HasPullback g (f i)
⊢ ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (p₁ i)))

Tactic:
use i

Goal state after:
case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison F f g))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : ∀ (x : (fun X ↦ X) (F.obj S)), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
x : F.obj Y
i : ι
hi : (ConcreteCategory.hom (F.map g)) x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
this : HasPullback g (f i)
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (p₁ i)))
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: K : Precoverage Scheme
X Y Z : Scheme
𝒰✝ : Cover K X
f : X ⟶ Z
g : Y ⟶ Z
inst✝² : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
inst✝¹ : JointlySurjective K
inst✝ : Nonempty ↥X
𝒰 : Cover K X
i : 𝒰.I₀
h✝ : ∃ y, (𝒰.f i) y = inst✝.some
⊢ Nonempty 𝒰.I₀

Tactic:
use i

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ IsOpenImmersion.RespectsIso

Tactic:
apply MorphismProperty.respectsIso_of_isStableUnderComposition
  intro _ _ f (hf : IsIso f)
  have : IsIso f := hf
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: case pos
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
s : Set ↑Γ(X, U)
x : ↥Y
hx : x ∈ Set.range ⇑f
⊢ x ∈ ⇑f '' X.zeroLocus s ↔ x ∈ Y.zeroLocus (⇑(CommRingCat.Hom.hom (Hom.appIso f U).inv) '' s) ∩ Set.range ⇑f

Tactic:
obtain ⟨x, rfl⟩ := hx
    simp [f.isOpenEmbedding.injective.mem_set_image, ← Scheme.image_basicOpen]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
s : Type u_1
X : Scheme
U : s → X.Opens
hU : IsOpenCover U
x : ↥X
i : s
hi : x ∈ U i
⊢ ∃ i, x ∈ Set.range ⇑({ I₀ := s, X := fun i ↦ ↑(U i), f := fun i ↦ (U i).ι }.f i)

Tactic:
use i

Goal state after:
case h
C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
s : Type u_1
X : Scheme
U : s → X.Opens
hU : IsOpenCover U
x : ↥X
i : s
hi : x ∈ U i
⊢ x ∈ Set.range ⇑({ I₀ := s, X := fun i ↦ ↑(U i), f := fun i ↦ (U i).ι }.f i)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
e₁ : Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U).presheaf.map (eqToHom ⋯).op
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
e₂ :
  (↑V).presheaf.map (eqToIso this).hom.op ≫ Hom.app (X.homOfLE e) (V.ι ⁻¹ᵁ V.ι ''ᵁ W) =
    Hom.app (X.homOfLE e) W ≫ (↑U).presheaf.map ((Opens.map (X.homOfLE e).base).map (eqToIso this).hom.op.unop).op
e₃ :
  Hom.app (X.homOfLE e) W ≫
      X.presheaf.map ((Hom.opensFunctor U.ι).map ((Opens.map (X.homOfLE e).base).map (eqToHom this))).op =
    X.presheaf.map (homOfLE ⋯).op ≫ X.presheaf.map ((Hom.opensFunctor U.ι).map (eqToHom ⋯)).op
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op

Tactic:
← IsIso.eq_comp_inv,

Goal state after:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
e₁ : Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U).presheaf.map (eqToHom ⋯).op
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
e₂ :
  (↑V).presheaf.map (eqToIso this).hom.op ≫ Hom.app (X.homOfLE e) (V.ι ⁻¹ᵁ V.ι ''ᵁ W) =
    Hom.app (X.homOfLE e) W ≫ (↑U).presheaf.map ((Opens.map (X.homOfLE e).base).map (eqToIso this).hom.op.unop).op
e₃ :
  Hom.app (X.homOfLE e) W =
    (X.presheaf.map (homOfLE ⋯).op ≫ X.presheaf.map ((Hom.opensFunctor U.ι).map (eqToHom ⋯)).op) ≫
      inv (X.presheaf.map ((Hom.opensFunctor U.ι).map ((Opens.map (X.homOfLE e).base).map (eqToHom this))).op)
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: R : CommRingCat
this : (Spec R).toSpecΓ ≫ Spec.map (Scheme.ΓSpecIso R).inv = 𝟙 (Spec R)
⊢ Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ

Tactic:
← IsIso.eq_comp_inv,

Goal state after:
R : CommRingCat
this : (Spec R).toSpecΓ = 𝟙 (Spec R) ≫ inv (Spec.map (Scheme.ΓSpecIso R).inv)
⊢ Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ
Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers

Goal state before:
pp: case mp
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : ⇑(hom f) ⁻¹' U = ⇑(hom g) ⁻¹' U
lem : ∀ (x y : (fun X ↦ X) Y), Function.Coequalizer.Rel (⇑(hom f)) (⇑(hom g)) x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y ↦ x ∈ U ↔ y ∈ U
x✝ : (fun X ↦ X) Y
⊢ x✝ ∈
      ⇑(hom
            ((coequalizerColimit f g).cocone.ι.app WalkingParallelPair.one ≫
              (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv)) ⁻¹'
        ⇑(hom
              ((coequalizerColimit f g).cocone.ι.app WalkingParallelPair.one ≫
                (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv)) ''
          U →
    x✝ ∈ U

Tactic:
rintro ⟨y, hy, e'⟩

Goal state after:
case mp
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : ⇑(hom f) ⁻¹' U = ⇑(hom g) ⁻¹' U
lem : ∀ (x y : (fun X ↦ X) Y), Function.Coequalizer.Rel (⇑(hom f)) (⇑(hom g)) x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y ↦ x ∈ U ↔ y ∈ U
x✝ : (fun X ↦ X) Y
y : Y
hy : y ∈ U
e' :
  (hom
        ((coequalizerColimit f g).cocone.ι.app WalkingParallelPair.one ≫
          (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv))
      y =
    (hom
        ((coequalizerColimit f g).cocone.ι.app WalkingParallelPair.one ≫
          (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv))
      x✝
⊢ x✝ ∈ U
Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers

Goal state before:
pp: case mp
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : ⇑(hom f) ⁻¹' U = ⇑(hom g) ⁻¹' U
lem : ∀ (x y : (fun X ↦ X) Y), Function.Coequalizer.Rel (⇑(hom f)) (⇑(hom g)) x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y ↦ x ∈ U ↔ y ∈ U
x✝ : (fun X ↦ X) Y
⊢ x✝ ∈ ⇑(hom π) ⁻¹' ⇑(hom π) '' U → x✝ ∈ U

pp: case mpr
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : ⇑(hom f) ⁻¹' U = ⇑(hom g) ⁻¹' U
lem : ∀ (x y : (fun X ↦ X) Y), Function.Coequalizer.Rel (⇑(hom f)) (⇑(hom g)) x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y ↦ x ∈ U ↔ y ∈ U
x✝ : (fun X ↦ X) Y
⊢ x✝ ∈ U → x✝ ∈ ⇑(hom π) ⁻¹' ⇑(hom π) '' U

Tactic:
· rw [←
      show _ = π from
        h.comp_coconePointUniqueUpToIso_inv (coequalizerColimit f g).2
          WalkingParallelPair.one]
    rintro ⟨y, hy, e'⟩
    dsimp at e'
    have e'' :=
      (mono_iff_injective
            (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv).mp
        inferInstance
    refine (eqv.eqvGen_iff.mp (Relation.EqvGen.mono lem y _ (Quot.eqvGen_exact ?_))).mp hy
    apply e''
    convert! e'

Goal state after:
case mpr
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : ⇑(hom f) ⁻¹' U = ⇑(hom g) ⁻¹' U
lem : ∀ (x y : (fun X ↦ X) Y), Function.Coequalizer.Rel (⇑(hom f)) (⇑(hom g)) x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y ↦ x ∈ U ↔ y ∈ U
x✝ : (fun X ↦ X) Y
⊢ x✝ ∈ U → x✝ ∈ ⇑(hom π) ⁻¹' ⇑(hom π) '' U
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
y : PrimeSpectrum ↑Γ(X, U) := hU.primeIdealOf ⟨x, hx⟩
hy : y = hU.primeIdealOf ⟨x, hx⟩
this : hU.fromSpec y = x
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hx⟩)) y.asIdeal

Tactic:
clear_value y

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
y : PrimeSpectrum ↑Γ(X, U)
hy : y = hU.primeIdealOf ⟨x, hx⟩
this : hU.fromSpec y = x
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hx⟩)) y.asIdeal
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case a
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
x : ↥X
hx : x ∈ U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑U
⊢ ↑V ⊆ ↑(⨆ i ∈ s, X.basicOpen i)

Tactic:
← (hV.iSup_basicOpen_eq_self_iff (s := X.presheaf.map (homOfLE hVU).op '' s)).mpr
      (by rw [← Ideal.map_span, hs, Ideal.map_top])

Goal state after:
case a
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
x : ↥X
hx : x ∈ U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑U
⊢ ↑(⨆ f, X.basicOpen ↑f) ⊆ ↑(⨆ i ∈ s, X.basicOpen i)