mathlib-initiative/mathlib-tactics huggingface dataset:
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₃
⊢ c₂ • (q.i * c₃ • 1) - (c₁ • q.j * q.j + c₂ • (q.i * q.j) * q.j) = -((c₁ * c₃) • 1)

Tactic:
smul_mul_assoc,

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₃
⊢ c₂ • (q.i * c₃ • 1) - (c₁ • (q.j * q.j) + c₂ • (q.i * q.j) * q.j) = -((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₃
⊢ c₂ • (q.i * c₃ • 1) - ((c₁ * c₃) • 1 + c₂ • (q.i * q.j) * q.j) = -((c₁ * c₃) • 1)

Tactic:
smul_mul_assoc,

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₃
⊢ c₂ • (q.i * c₃ • 1) - ((c₁ * c₃) • 1 + c₂ • (q.i * q.j * q.j)) = -((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₃
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 • 1 * y.re • 1 + x.re • 1 * y.imI • q.i + x.re • 1 * y.imJ • q.j + x.re • 1 * y.imK • q.k +
          (x.imI • q.i * y.re • 1 + x.imI • q.i * y.imI • q.i + x.imI • q.i * y.imJ • q.j + x.imI • q.i * y.imK • q.k) +
        (x.imJ • q.j * y.re • 1 + x.imJ • q.j * y.imI • q.i + x.imJ • q.j * y.imJ • q.j + x.imJ • q.j * y.imK • q.k) +
      (x.imK • q.k * y.re • 1 + x.imK • q.k * y.imI • q.i + x.imK • q.k * y.imJ • q.j + x.imK • q.k * y.imK • q.k)

Tactic:
smul_mul_assoc,

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 • (1 * y.re • 1) + x.re • (1 * y.imI • q.i) + x.re • (1 * y.imJ • q.j) + x.re • (1 * y.imK • q.k) +
          (x.imI • (q.i * y.re • 1) + x.imI • (q.i * y.imI • q.i) + x.imI • (q.i * y.imJ • q.j) +
            x.imI • (q.i * y.imK • q.k)) +
        (x.imJ • (q.j * y.re • 1) + x.imJ • (q.j * y.imI • q.i) + x.imJ • (q.j * y.imJ • q.j) +
          x.imJ • (q.j * y.imK • q.k)) +
      (x.imK • (q.k * y.re • 1) + x.imK • (q.k * y.imI • q.i) + x.imK • (q.k * y.imJ • q.j) +
        x.imK • (q.k * y.imK • q.k))
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case ofNat
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 : ℕ
⊢ ↑n = IntCast.intCast ↑n

Tactic:
inst₂.intCast_ofNat

Goal state after:
case ofNat
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 : ℕ
⊢ ↑n = ↑n
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case rel
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
a b x✝ y✝ : R
hab : Rel r x✝ y✝
c d : R
hcd : Relation.EqvGen (Rel r) c d
⊢ Relation.EqvGen (Rel r) (x✝ * c) (y✝ * d)

Tactic:
| rel _ _ hab =>

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case rel
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
a b x✝ y✝ : R
hab : Rel r x✝ y✝
c d : R
hcd : Relation.EqvGen (Rel r) c d
⊢ Relation.EqvGen (Rel r) (x✝ + c) (y✝ + d)

Tactic:
| rel _ _ hab =>

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

Goal state before:
pp: case pos
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
x : α
hx : x = a
⊢ (f.update a b).coeff x = ((erase a) f + single a b).coeff x

Tactic:
aesop (add norm coeff_single_apply)

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

Goal state before:
pp: case neg
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
x : α
hx : ¬x = a
⊢ (f.update a b).coeff x = ((erase a) f + single a b).coeff x

Tactic:
aesop (add norm coeff_single_apply)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f g : ↥(Subsemiring.center (CentroidHom α))
a : α
⊢ star (g (f (star a))) = star (g (star (star (f (star a)))))

Tactic:
by simp only [star_star]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : SkewPolynomial R
⊢ (-p).support = p.support

Tactic:
simpa [support_eq_skewMonoidAlgebra_support] using SkewMonoidAlgebra.support_neg p

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : AddGroupWithOne k
inst✝ : One G
z : ℤ
⊢ ↑z = single 1 ↑z

Tactic:
cases z

Goal state after:
case ofNat
k : Type u_1
G : Type u_2
inst✝¹ : AddGroupWithOne k
inst✝ : One G
a✝ : ℕ
⊢ ↑(Int.ofNat a✝) = single 1 ↑(Int.ofNat a✝)

case negSucc
k : Type u_1
G : Type u_2
inst✝¹ : AddGroupWithOne k
inst✝ : One G
a✝ : ℕ
⊢ ↑(Int.negSucc a✝) = single 1 ↑(Int.negSucc a✝)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Mul G
inst✝¹ : SMulZeroClass G k
inst✝ : DecidableEq G
f g : SkewMonoidAlgebra k G
x : G
⊢ (f.sum fun a₁ b₁ ↦ g.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)).coeff x =
    f.sum fun a₁ b₁ ↦ g.sum fun a₂ b₂ ↦ if a₁ * a₂ = x then b₁ * a₁ • b₂ else 0

Tactic:
coeff_sum

Goal state after:
k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Mul G
inst✝¹ : SMulZeroClass G k
inst✝ : DecidableEq G
f g : SkewMonoidAlgebra k G
x : G
⊢ (f.sum fun a₁ b ↦ (g.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b * a₁ • b₂)).coeff x) =
    f.sum fun a₁ b₁ ↦ g.sum fun a₂ b₂ ↦ if a₁ * a₂ = x then b₁ * a₁ • b₂ else 0
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case e_g
k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Mul G
inst✝¹ : SMulZeroClass G k
inst✝ : DecidableEq G
f g : SkewMonoidAlgebra k G
x x✝¹ : G
x✝ : k
⊢ (g.sum fun a₂ b₂ ↦ single (x✝¹ * a₂) (x✝ * x✝¹ • b₂)).coeff x =
    g.sum fun a₂ b₂ ↦ if x✝¹ * a₂ = x then x✝ * x✝¹ • b₂ else 0

Tactic:
coeff_sum

Goal state after:
case e_g
k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Mul G
inst✝¹ : SMulZeroClass G k
inst✝ : DecidableEq G
f g : SkewMonoidAlgebra k G
x x✝¹ : G
x✝ : k
⊢ (g.sum fun a₁ b ↦ (single (x✝¹ * a₁) (x✝ * x✝¹ • b)).coeff x) =
    g.sum fun a₂ b₂ ↦ if x✝¹ * a₂ = x then x✝ * x✝¹ • b₂ else 0
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: case inr
R : Type u
inst✝³ : LinearOrder R
inst✝² : AddMonoid R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
x y : Tropical R
n : ℕ
h : y ≤ x
⊢ (x + y) ^ n = x ^ n + y ^ n

Tactic:
add_eq_right h,

Goal state after:
case inr
R : Type u
inst✝³ : LinearOrder R
inst✝² : AddMonoid R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
x y : Tropical R
n : ℕ
h : y ≤ x
⊢ y ^ n = x ^ n + y ^ n
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 : ℤ
x : V
h : n < ((HahnModule.of R).symm (A x)).order
⊢ (coeff A n) x = 0

Tactic:
coeff_eq_ncoeff,

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 : ℤ
x : V
h : n < ((HahnModule.of R).symm (A x)).order
⊢ (ncoeff A (-n - 1)) x = 0
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.Surjective ⇑(ConcreteCategory.hom f.hom.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Mono (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace C
g : ↑Y.toPresheafedSpace ⟶ ↑Z.toPresheafedSpace
gc hc : Z.presheaf ⟶ (pushforward C g).obj Y.presheaf
e : (f ≫ { hom := { base := g, c := gc } }).hom = (f ≫ { hom := { base := g, c := hc } }).hom
y : ↑↑Y.toPresheafedSpace
⊢ PresheafedSpace.Hom.stalkMap { hom := { base := g, c := gc } }.hom y =
    (Z.presheaf.stalkCongr ⋯).hom ≫ PresheafedSpace.Hom.stalkMap { hom := { base := g, c := hc } }.hom y

Tactic:
← (h₁ y).choose_spec,

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.Surjective ⇑(ConcreteCategory.hom f.hom.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Mono (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace C
g : ↑Y.toPresheafedSpace ⟶ ↑Z.toPresheafedSpace
gc hc : Z.presheaf ⟶ (pushforward C g).obj Y.presheaf
e : (f ≫ { hom := { base := g, c := gc } }).hom = (f ≫ { hom := { base := g, c := hc } }).hom
y : ↑↑Y.toPresheafedSpace
⊢ PresheafedSpace.Hom.stalkMap { hom := { base := g, c := gc } }.hom ((ConcreteCategory.hom f.hom.base) ⋯.choose) =
    (Z.presheaf.stalkCongr ⋯).hom ≫
      PresheafedSpace.Hom.stalkMap { hom := { base := g, c := hc } }.hom ((ConcreteCategory.hom f.hom.base) ⋯.choose)
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X✝ X : LocallyRingedSpace
x : ↑↑X.toPresheafedSpace
⊢ IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (𝟙 X.toPresheafedSpace) x))

Tactic:
PresheafedSpace.stalkMap.id

Goal state after:
X✝ X : LocallyRingedSpace
x : ↑↑X.toPresheafedSpace
⊢ IsLocalHom (CommRingCat.Hom.hom (𝟙 (X.presheaf.stalk x)))
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : ↥U → Opens ↑↑X.toPresheafedSpace
iVU : (x : ↥U) → V x ⟶ U
m : ∀ (x : ↥U), ↑x ∈ V x
h_unit : ∀ (x : ↥U), IsUnit ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f)
x : ↑↑X.toPresheafedSpace
⊢ x ∈ U → x ∈ iSup V

Tactic:
hxU

Goal state after:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : ↥U → Opens ↑↑X.toPresheafedSpace
iVU : (x : ↥U) → V x ⟶ U
m : ∀ (x : ↥U), ↑x ∈ V x
h_unit : ∀ (x : ↥U), IsUnit ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f)
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
⊢ x ∈ iSup V
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R : CommRingCat
f : ↑R
x : ↥(Spec R)
⊢ IsUnit ((StructureSheaf.stalkIso (↑R) x).symm ((algebraMap ↑R ↑((structurePresheafInCommRingCat ↑R).stalk x)) f)) ↔
    f ∉ x.asIdeal

Tactic:
AlgEquiv.commutes

Goal state after:
R : CommRingCat
f : ↑R
x : ↥(Spec R)
⊢ IsUnit ((algebraMap (↑R) (Localization.AtPrime x.asIdeal)) f) ↔ f ∉ x.asIdeal
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U U' : X.Opens
h : f ''ᵁ U ≤ f ''ᵁ U'
⊢ U ≤ U'

Tactic:
rw [← preimage_image_eq f U, ← preimage_image_eq f U']

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U U' : X.Opens
h : f ''ᵁ U ≤ f ''ᵁ U'
⊢ f ⁻¹ᵁ f ''ᵁ U ≤ f ⁻¹ᵁ f ''ᵁ U'
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: case h
P : MorphismProperty Scheme
inst✝¹ : IsJointlySurjectivePreserving P
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
hf : P f
x : ↥X
y : ↥Y
h : f x = g y
iso : pullback f g ≅ pullback g f := ⋯
this : HasPullback g f
a : ↥(pullback g f)
ha : (pullback.fst g f) a = y
⊢ (pullback.snd f g) ((pullbackSymmetry f g).inv a) = y

Tactic:
rwa [← Scheme.Hom.comp_apply, pullbackSymmetry_inv_comp_snd]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Function.Surjective ⇑(ConcreteCategory.hom (PreservesPullback.iso Scheme.forgetToTop f g).hom)

Tactic:
← TopCat.epi_iff_surjective

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Epi (PreservesPullback.iso Scheme.forgetToTop f g).hom
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
P Q : MorphismProperty Scheme
inst✝ : JointlySurjective K
𝒰 : Cover K X
h : ∀ (j : 𝒰.I₀), Q (𝒰.f j)
⊢ 𝒰.presieve₀ ∈ (precoverage Q).coverings X

Tactic:
by
    rw [presieve₀_mem_precoverage_iff]
    exact ⟨𝒰.exists_eq, h⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Function.Surjective ⇑(ConcreteCategory.hom (PreservesPullback.iso Scheme.forgetToTop g f).hom)

Tactic:
← TopCat.epi_iff_surjective

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Epi (PreservesPullback.iso Scheme.forgetToTop g f).hom
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasLimits C
inst✝⁴ : HasColimits 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✝² : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : PreservesFilteredColimits (CategoryTheory.forget C)
X Y : SheafedSpace C
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f.hom.base)
U : Opens ↑↑X.toPresheafedSpace
y : ↑↑X.toPresheafedSpace
H :
  IsIso
    ((TopCat.Presheaf.stalkFunctor C ((ConcreteCategory.hom f.hom.base) y)).map f.hom.c ≫
      TopCat.Presheaf.stalkPushforward C f.hom.base X.presheaf y)
hy : y ∈ ↑U
⊢ IsIso
    ((TopCat.Presheaf.stalkFunctor C ↑⟨(ConcreteCategory.hom f.hom.base) y, ⋯⟩).map
      (have this := { hom := f.hom.c };
        this).hom)

Tactic:
have H' := TopCat.Presheaf.stalkPushforward.stalkPushforward_iso_of_isInducing C
        hf.toIsInducing X.presheaf y

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasLimits C
inst✝⁴ : HasColimits 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✝² : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : PreservesFilteredColimits (CategoryTheory.forget C)
X Y : SheafedSpace C
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f.hom.base)
U : Opens ↑↑X.toPresheafedSpace
y : ↑↑X.toPresheafedSpace
H :
  IsIso
    ((TopCat.Presheaf.stalkFunctor C ((ConcreteCategory.hom f.hom.base) y)).map f.hom.c ≫
      TopCat.Presheaf.stalkPushforward C f.hom.base X.presheaf y)
hy : y ∈ ↑U
H' : IsIso (TopCat.Presheaf.stalkPushforward C f.hom.base X.presheaf y)
⊢ IsIso
    ((TopCat.Presheaf.stalkFunctor C ↑⟨(ConcreteCategory.hom f.hom.base) y, ⋯⟩).map
      (have this := { hom := f.hom.c };
        this).hom)
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
ι : Type u_1
s : ι → ↑R
hs : Ideal.span (Set.range s) = ⊤
x : ↥(Spec R)
H : ∃ i, s i ∉ x.asIdeal
i : ι := H.choose
⊢ x ∈
    Set.range
      ⇑(Spec.map
          (CommRingCat.ofHom
            (algebraMap (↑R)
              (Localization.Away
                (s
                  (have this := H;
                  this.choose))))))

Tactic:
have := PrimeSpectrum.localization_away_comap_range (Localization.Away (s i)) (s i)

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
ι : Type u_1
s : ι → ↑R
hs : Ideal.span (Set.range s) = ⊤
x : ↥(Spec R)
H : ∃ i, s i ∉ x.asIdeal
i : ι := H.choose
this : Set.range (PrimeSpectrum.comap (algebraMap (↑R) (Localization.Away (s i)))) = ↑(PrimeSpectrum.basicOpen (s i))
⊢ x ∈
    Set.range
      ⇑(Spec.map
          (CommRingCat.ofHom
            (algebraMap (↑R)
              (Localization.Away
                (s
                  (have this := H;
                  this.choose))))))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this✝ : IsIso (pullback.snd f g)
this :
  (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom ≫
      pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g) =
    (pullback.fst f g).base
⊢ Set.range
      ⇑(ConcreteCategory.hom
          (pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
            ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g))) =
    ⇑(ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom g.base)

pp: X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this✝ : IsIso (pullback.snd f g)
this :
  (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom ≫
      pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g) =
    (pullback.fst f g).base
⊢ Function.Surjective
    ⇑(ConcreteCategory.hom
        ((inv (pullback.snd f g)).base ≫
          (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom))

Tactic:
· rw [TopCat.pullback_fst_range]
    ext
    constructor
    · rintro ⟨y, eq⟩; exact ⟨y, eq.symm⟩
    · rintro ⟨y, eq⟩; exact ⟨y, eq.symm⟩

Goal state after:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this✝ : IsIso (pullback.snd f g)
this :
  (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom ≫
      pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g) =
    (pullback.fst f g).base
⊢ Function.Surjective
    ⇑(ConcreteCategory.hom
        ((inv (pullback.snd f g)).base ≫
          (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom))
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case refine_1
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
s : (structureSheafInType R M).obj.obj (op U)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg : ∀ (x : ↥V), ∃ (hs : g ∉ (↑x).asIdeal), (fun x ↦ ↑s (iVU x)) x = LocalizedModule.mk f ⟨g, hs⟩
g' : R
hxg' : ↑⟨x, hx⟩ ∈ ↑(basicOpen g')
hg'U : ↑(basicOpen g') ⊆ ↑V
⊢ x ∈ basicOpen (g' * g)

Tactic:
simp only [PrimeSpectrum.basicOpen_mul]

Goal state after:
case refine_1
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
s : (structureSheafInType R M).obj.obj (op U)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg : ∀ (x : ↥V), ∃ (hs : g ∉ (↑x).asIdeal), (fun x ↦ ↑s (iVU x)) x = LocalizedModule.mk f ⟨g, hs⟩
g' : R
hxg' : ↑⟨x, hx⟩ ∈ ↑(basicOpen g')
hg'U : ↑(basicOpen g') ⊆ ↑V
⊢ x ∈ basicOpen g' ⊓ basicOpen g
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case refine_2
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
s : (structureSheafInType R M).obj.obj (op U)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg : ∀ (x : ↥V), ∃ (hs : g ∉ (↑x).asIdeal), (fun x ↦ ↑s (iVU x)) x = LocalizedModule.mk f ⟨g, hs⟩
g' : R
hxg' : ↑⟨x, hx⟩ ∈ ↑(basicOpen g')
hg'U : ↑(basicOpen g') ⊆ ↑V
⊢ basicOpen (g' * g) ≤ U

Tactic:
simp only [PrimeSpectrum.basicOpen_mul]

Goal state after:
case refine_2
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
s : (structureSheafInType R M).obj.obj (op U)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg : ∀ (x : ↥V), ∃ (hs : g ∉ (↑x).asIdeal), (fun x ↦ ↑s (iVU x)) x = LocalizedModule.mk f ⟨g, hs⟩
g' : R
hxg' : ↑⟨x, hx⟩ ∈ ↑(basicOpen g')
hg'U : ↑(basicOpen g') ⊆ ↑V
⊢ basicOpen g' ⊓ basicOpen g ≤ U
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case refine_3
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
s : (structureSheafInType R M).obj.obj (op U)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg : ∀ (x : ↥V), ∃ (hs : g ∉ (↑x).asIdeal), (fun x ↦ ↑s (iVU x)) x = LocalizedModule.mk f ⟨g, hs⟩
g' : R
hxg' : ↑⟨x, hx⟩ ∈ ↑(basicOpen g')
hg'U : ↑(basicOpen g') ⊆ ↑V
x✝ : ↥(unop (op (basicOpen (g' * g))))
y : ↑(PrimeSpectrum.Top R)
hy : y ∈ unop (op (basicOpen (g' * g)))
⊢ ↑(const (g' • f) (g' * g) (basicOpen (g' * g)) ⋯) ⟨y, hy⟩ =
    ↑((ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s) ⟨y, hy⟩

Tactic:
simp only [PrimeSpectrum.basicOpen_mul]

Goal state after:
case refine_3
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
s : (structureSheafInType R M).obj.obj (op U)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg : ∀ (x : ↥V), ∃ (hs : g ∉ (↑x).asIdeal), (fun x ↦ ↑s (iVU x)) x = LocalizedModule.mk f ⟨g, hs⟩
g' : R
hxg' : ↑⟨x, hx⟩ ∈ ↑(basicOpen g')
hg'U : ↑(basicOpen g') ⊆ ↑V
x✝ : ↥(unop (op (basicOpen (g' * g))))
y : ↑(PrimeSpectrum.Top R)
hy : y ∈ unop (op (basicOpen (g' * g)))
⊢ ↑(const (g' • f) (g' * g) (basicOpen (g' * g)) ⋯) ⟨y, hy⟩ =
    ↑((ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s) ⟨y, hy⟩
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : M
g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu : U ≤ basicOpen g₁
hf : f₁ = f₂
hg : g₁ = g₂
⊢ const f₁ g₁ U hu = const f₂ g₂ U ⋯

Tactic:
subst hf hg; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
W : (↑(f ⁻¹ᵁ U)).Opens
e : W ≤ (f ∣_ U) ⁻¹ᵁ V
⊢ Scheme.Hom.appLE (f ∣_ U) V W e = Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ W) ⋯

Tactic:
Scheme.Hom.appLE,

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
W : (↑(f ⁻¹ᵁ U)).Opens
e : W ≤ (f ∣_ U) ⁻¹ᵁ V
⊢ Scheme.Hom.app (f ∣_ U) V ≫ (↑(f ⁻¹ᵁ U)).presheaf.map (homOfLE e).op =
    Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ W) ⋯