mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: K : Type u_1
R : Type u_2
a b : R
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
f : QuadraticAlgebra R a b →ₐ[R] A
⊢ f ω * f ω = a • 1 + b • f ω

Tactic:
simp [← map_mul, omega_mul_omega_eq_add]

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

Goal state before:
pp: K : Type u_1
R : Type u_2
a b : R
inst✝ : CommRing R
x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (star (x✝¹ + x✝)).re = (star x✝¹ + star x✝).re

Tactic:
simp only [re_star, re_add, im_add]; ring

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 = a

Tactic:
by
    rintro ⟨⟨⟩⟩
    simp only [add_quot, ← zero_quot, add_zero]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case add_left
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 : RingQuot r
a✝² b✝¹ a✝¹ b✝ c✝ : R
a✝ : Rel r a✝¹ b✝
r' : f a✝¹ = f b✝
⊢ f (a✝¹ + c✝) = f (b✝ + c✝)

Tactic:
rw [map_add, map_add, r']

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

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
a : α
⊢ a * ↑(star z) = ↑(star z) * a

Tactic:
by rw [(star z).property.comm]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
a b : FreeAlgebra R X
⊢ (MulOpposite.unop ∘ ⇑((lift R) (MulOpposite.op ∘ ι R))) (a + b) =
    (MulOpposite.unop ∘ ⇑((lift R) (MulOpposite.op ∘ ι R))) a +
      (MulOpposite.unop ∘ ⇑((lift R) (MulOpposite.op ∘ ι R))) b

Tactic:
simp only [Function.comp_apply, map_add, MulOpposite.unop_add]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddMonoid k
p : G →₀ k
⊢ { coeff := p }.support = p.support

Tactic:
by
  rw [support]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddMonoid k
p : SkewMonoidAlgebra k G
⊢ p.coeff.support = p.support

Tactic:
by
  rw [support]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : CommMonoid G
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
a b : SkewMonoidAlgebra k G
hgk : ∀ (g : G) (r : k), g • r = r
x : G
x✝¹ : x ∈ b.coeff.support
y : G
x✝ : y ∈ a.coeff.support
⊢ single (y * x) (a.coeff y * b.coeff x) = single (x * y) (b.coeff x * a.coeff y)

Tactic:
rw [mul_comm, mul_comm (a.coeff y) _]

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

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

Tactic:
induction s using Multiset.induction with

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

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

Tactic:
induction s using Multiset.induction with

Goal state after:
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
⊢ g (single 1 b) * f (single a 1) = g (single 1 b) * g (single a 1)

Tactic:
h_of

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
⊢ g (single 1 b) * g (single a 1) = g (single 1 b) * g (single a 1)
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
r : R
u : U
⊢ A.compHahnSeries B (r • u) = r • A.compHahnSeries B u

Tactic:
ext
  simp only [compHahnSeries_coeff, map_smul, coeff_apply_apply, HahnSeries.coeff_smul]
  rw [← HahnSeries.coeff_smul]

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : X ⟶ Y
h₁ : Function.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 : Z.presheaf ⟶ (pushforward C g).obj Y.presheaf
h : ↑Y.toPresheafedSpace ⟶ ↑Z.toPresheafedSpace
hc : Z.presheaf ⟶ (pushforward C h).obj Y.presheaf
e : f ≫ { hom := { base := g, c := gc } } = f ≫ { hom := { base := h, c := hc } }
⊢ { hom := { base := g, c := gc } } = { hom := { base := h, c := hc } }

Tactic:
apply_fun InducedCategory.Hom.hom at e

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 : Z.presheaf ⟶ (pushforward C g).obj Y.presheaf
h : ↑Y.toPresheafedSpace ⟶ ↑Z.toPresheafedSpace
hc : Z.presheaf ⟶ (pushforward C h).obj Y.presheaf
e : (f ≫ { hom := { base := g, c := gc } }).hom = (f ≫ { hom := { base := h, c := hc } }).hom
⊢ { hom := { base := g, c := gc } } = { hom := { base := h, c := hc } }
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X Y : LocallyRingedSpace
e : X ≅ Y
y : ↑Y.toTopCat
⊢ Hom.stalkMap e.hom ((ConcreteCategory.hom e.inv.base) y) ≫ Hom.stalkMap e.inv y = Y.presheaf.stalkSpecializes ⋯

Tactic:
← stalkMap_comp,

Goal state after:
X Y : LocallyRingedSpace
e : X ≅ Y
y : ↑Y.toTopCat
⊢ Hom.stalkMap (e.inv ≫ e.hom) y = Y.presheaf.stalkSpecializes ⋯
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X Y : LocallyRingedSpace
e : X ≅ Y
x : ↑X.toTopCat
⊢ Hom.stalkMap e.inv ((ConcreteCategory.hom e.hom.base) x) ≫ Hom.stalkMap e.hom x = X.presheaf.stalkSpecializes ⋯

Tactic:
← stalkMap_comp,

Goal state after:
X Y : LocallyRingedSpace
e : X ≅ Y
x : ↑X.toTopCat
⊢ Hom.stalkMap (e.hom ≫ e.inv) x = X.presheaf.stalkSpecializes ⋯
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
⊢ X.presheaf = (Presheaf.pushforward C (X.ofRestrict ⋯).base).obj (X.restrict ⋯).presheaf

Tactic:
restrict_top_presheaf,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
⊢ X.presheaf =
    (Presheaf.pushforward C (X.ofRestrict ⋯).base).obj
      ((Presheaf.pushforward C (Opens.inclusionTopIso ↑X).inv).obj X.presheaf)
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
s : Set ↑(X.presheaf.obj (op U))
i : ↑(X.presheaf.obj (op U))
a✝ : i ∈ s
⊢ IsClosed (↑(X.basicOpen i))ᶜ

Tactic:
simp only [isClosed_compl_iff]

Goal state after:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
s : Set ↑(X.presheaf.obj (op U))
i : ↑(X.presheaf.obj (op U))
a✝ : i ∈ s
⊢ IsOpen ↑(X.basicOpen i)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : LocallyRingedSpace
h : ∀ (x : ↑X.toTopCat), ∃ R f, x ∈ Set.range ⇑(ConcreteCategory.hom f.base) ∧ IsOpenImmersion f
⊢ ∀ (x : ↑X.toTopCat), ∃ U R, Nonempty (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))

Tactic:
by
    intro x
    obtain ⟨R, f, h₁, h₂⟩ := h x
    refine ⟨⟨⟨_, h₂.base_open.isOpen_range⟩, h₁⟩, R, ⟨?_⟩⟩
    apply LocallyRingedSpace.isoOfSheafedSpaceIso
    refine SheafedSpace.forgetToPresheafedSpace.preimageIso ?_
    apply PresheafedSpace.IsOpenImmersion.isoOfRangeEq (PresheafedSpace.ofRestrict _ _) f.1
    exact Subtype.range_coe_subtype

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

Goal state before:
pp: K : Precoverage Scheme
inst✝ : JointlySurjective K
X : Scheme
𝒰 : Cover K X
⊢ ⋃ i, Set.range ⇑(𝒰.f i) = Set.univ

Tactic:
rw [Set.eq_univ_iff_forall]

Goal state after:
K : Precoverage Scheme
inst✝ : JointlySurjective K
X : Scheme
𝒰 : Cover K X
⊢ ∀ (x : ↥X), x ∈ ⋃ i, Set.range ⇑(𝒰.f i)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range ⇑(pullback.fst g f ≫ g) = Set.range ⇑g ∩ Set.range ⇑f

Tactic:
rw [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp, range_pullbackFst,
    Opens.map_obj, Opens.coe_mk, Set.image_preimage_eq_inter_range,
    Set.inter_comm, Opens.carrier_eq_coe, Scheme.Hom.coe_opensRange]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this : (preservesLimitIso forget (cospan g f)).hom ≫ limit.π (cospan g f ⋙ forget) left = (pullback.fst g f).hom
⊢ PresheafedSpace.IsOpenImmersion ((preservesLimitIso forget (cospan g f)).hom ≫ limit.π (cospan g f ⋙ forget) left)

Tactic:
have := HasLimit.isoOfNatIso_hom_π (diagramIsoCospan (cospan g f ⋙ forget)) left

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this✝ : (preservesLimitIso forget (cospan g f)).hom ≫ limit.π (cospan g f ⋙ forget) left = (pullback.fst g f).hom
this :
  (HasLimit.isoOfNatIso (diagramIsoCospan (cospan g f ⋙ forget))).hom ≫
      limit.π (cospan ((cospan g f ⋙ forget).map Hom.inl) ((cospan g f ⋙ forget).map Hom.inr)) left =
    limit.π (cospan g f ⋙ forget) left ≫ (diagramIsoCospan (cospan g f ⋙ forget)).hom.app left
⊢ PresheafedSpace.IsOpenImmersion ((preservesLimitIso forget (cospan g f)).hom ≫ limit.π (cospan g f ⋙ forget) left)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
W : (↑U).Opens
⊢ U.ι ''ᵁ W ≤ U

Tactic:
by
  simp_rw [← U.ι_image_top]
  exact U.ι.image_mono le_top

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
f g : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : U ≤ basicOpen g
hu₂ : U ≤ basicOpen f
⊢ const f g U hu₁ * const g f U hu₂ = 1

Tactic:
const_mul,

Goal state after:
R : Type u
inst✝ : CommRing R
f g : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : U ≤ basicOpen g
hu₂ : U ≤ basicOpen f
⊢ const (f * g) (g * f) U ⋯ = 1
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
f g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
⊢ const f g₁ U hu₁ * const g₁ g₂ U hu₂ = const f g₂ U hu₂

Tactic:
const_mul,

Goal state after:
R : Type u
inst✝ : CommRing R
f g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
⊢ const (f * g₁) (g₁ * g₂) U ⋯ = const f g₂ U hu₂
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
X : Scheme
U V : X.Opens
e : U = V
⊢ Set.range ⇑U.ι = Set.range ⇑V.ι

Tactic:
by rw [e]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ ↑V := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
t : pullback f g ⟶ pullback f V.ι := pullback.map f g f V.ι (𝟙 X) e.hom (𝟙 Y) ⋯ ⋯
⊢ t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ (f ⁻¹ᵁ Scheme.Hom.opensRange g).ι ≫ f = pullback.fst f g ≫ f

Tactic:
pullbackRestrictIsoRestrict_hom_ι_assoc,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ ↑V := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
t : pullback f g ⟶ pullback f V.ι := pullback.map f g f V.ι (𝟙 X) e.hom (𝟙 Y) ⋯ ⋯
⊢ t ≫ pullback.fst f V.ι ≫ f = pullback.fst f g ≫ f
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
x : ↥V
⊢ (Y.presheaf.stalkSpecializes ⋯ ≫ stalkMap f ↑x) ≫ stalkMap V.ι x =
    stalkMap U.ι ((resLE f U V e) x) ≫ stalkMap (resLE f U V e) x

Tactic:
← stalkMap_comp,

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
x : ↥V
⊢ (Y.presheaf.stalkSpecializes ⋯ ≫ stalkMap f ↑x) ≫ stalkMap V.ι x = stalkMap (resLE f U V e ≫ U.ι) x
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
f : R
hf : x ∈ basicOpen f
⊢ IsUnit ((algebraMap R (Module.End R ↑((structurePresheafInModuleCat R M).stalk x))) f)

Tactic:
have := (isUnit_toStalk x f hf).map (algebraMap _
    (Module.End ((structurePresheafInCommRingCat R).stalk x)
      ((structurePresheafInModuleCat R M).stalk x)))
  rw [Module.End.isUnit_iff] at this ⊢
  convert! this
  ext a
  simp only [Module.algebraMap_end_apply]
  rw [toStalk_smul]

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
⊢ stalkToLocalizationₗ R M x ≫ localizationtoStalkₗ R M x = 𝟙 ((structurePresheafInModuleCat R M).stalk x)

Tactic:
apply stalk_hom_ext
    intro U hxU
    ext s
    obtain ⟨g, hxg, igU, f, hs⟩ :=
      exists_const _ s x hxU
    rw [germ_stalkToLocalizationₗ_assoc, Category.comp_id, ← germ_res_apply _ igU.hom _ hxg]
    refine congr(localizationtoStalkₗ R M x (openToLocalizationₗ R M _ x hxg $hs)).symm.trans ?_
    refine (localizationtoStalkₗ_mk ..).trans
      congr((structurePresheafInModuleCat R M).germ _ x hxg $hs)

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
⊢ Scheme.Hom.app f (Y.basicOpen r) =
    CommRingCat.ofHom
        (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r))
          (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)))
          (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
      X.presheaf.map (eqToHom ⋯).op

Tactic:
have := hU.isLocalization_basicOpen r

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
this : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
⊢ Scheme.Hom.app f (Y.basicOpen r) =
    CommRingCat.ofHom
        (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r))
          (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)))
          (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
      X.presheaf.map (eqToHom ⋯).op
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

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

Tactic:
by
  rw [← basicOpen_eq_of_affine, Scheme.preimage_basicOpen, ← Scheme.Hom.appTop]
  congr
  rw [Scheme.toSpecΓ_appTop]
  exact Iso.inv_hom_id_apply (C := CommRingCat) _ _

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
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : ↑(PrimeSpectrum.Top S)
a : M
b : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
this✝ : Module R N := Module.compHom N σ
this : Algebra R S := σ.toAlgebra
⊢ (comapFun f y) (LocalizedModule.mk a b) = LocalizedModule.mk (f a) ⟨σ ↑b, ⋯⟩

Tactic:
have : IsScalarTower R S N := .of_algebraMap_smul fun _ _ ↦ rfl

Goal state after:
R M : Type u
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : ↑(PrimeSpectrum.Top S)
a : M
b : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
this✝¹ : Module R N := Module.compHom N σ
this✝ : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
⊢ (comapFun f y) (LocalizedModule.mk a b) = LocalizedModule.mk (f a) ⟨σ ↑b, ⋯⟩
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
s : (x : ↥U) → Localizations M ↑x
hs : (isLocallyFraction R M).pred s
this✝ : Module R N := Module.compHom N σ
this : Algebra R S := σ.toAlgebra
⊢ (isLocallyFraction S N).pred (comapFun f U V hUV s)

Tactic:
have : IsScalarTower R S N := .of_algebraMap_smul fun _ _ ↦ rfl

Goal state after:
R M : Type u
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
s : (x : ↥U) → Localizations M ↑x
hs : (isLocallyFraction R M).pred s
this✝¹ : Module R N := Module.compHom N σ
this✝ : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
⊢ (isLocallyFraction S N).pred (comapFun f U V hUV s)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
s : (x : ↥U) → Localizations M ↑x
hs : (isLocallyFraction R M).pred s
⊢ (isLocallyFraction S N).pred (comapFun f U V hUV s)

Tactic:
by
  let := Module.compHom N σ
  let := σ.toAlgebra
  have : IsScalarTower R S N := .of_algebraMap_smul fun _ _ ↦ rfl
  rintro ⟨p, hpV⟩
  obtain ⟨W, m, iWU, a, b, h_frac⟩ := hs ⟨PrimeSpectrum.comap σ p, hUV hpV⟩
  refine ⟨⟨_, (PrimeSpectrum.continuous_comap σ).isOpen_preimage _ W.2⟩ ⊓ V,
    ⟨m, hpV⟩, Opens.infLERight _ _, f a, σ b, ?_⟩
  rintro ⟨q, ⟨hqW, hqV⟩⟩
  obtain ⟨hs, H⟩ := h_frac ⟨PrimeSpectrum.comap σ q, hqW⟩
  refine ⟨hs, ?_⟩
  dsimp [comapFun] at H ⊢
  rw [H]
  simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
this : Hom.stalkMap ((gluedCover 𝒰).ι i ≫ fromGlued 𝒰) x = (X.presheaf.stalkCongr ⋯).hom ≫ Hom.stalkMap (𝒰.f i) x
⊢ IsIso (Hom.stalkMap (fromGlued 𝒰) (((gluedCover 𝒰).ι i) x))

Tactic:
Hom.stalkMap_comp,

Goal state after:
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
this :
  Hom.stalkMap (fromGlued 𝒰) (((gluedCover 𝒰).ι i) x) ≫ Hom.stalkMap ((gluedCover 𝒰).ι i) x =
    (X.presheaf.stalkCongr ⋯).hom ≫ Hom.stalkMap (𝒰.f i) x
⊢ IsIso (Hom.stalkMap (fromGlued 𝒰) (((gluedCover 𝒰).ι i) x))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
this : Topology.IsOpenEmbedding (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f))
⊢ Topology.IsOpenEmbedding ⇑(Sigma.desc α)

Tactic:
convert! this.comp (sigmaMk f).symm.isOpenEmbedding; ext; simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case e_a
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ (pullbackSymmetry s.fst (𝒰.f j)).inv ≫ pullback.snd s.fst (𝒰.f j) =
    pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯ ≫ pullback.fst (𝒰.f j ≫ f) g

Tactic:
pullbackSymmetry_inv_comp_snd,

Goal state after:
case e_a
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ pullback.fst (𝒰.f j) s.fst =
    pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯ ≫ pullback.fst (𝒰.f j ≫ f) g
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ pullback.fst ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      (pullbackSymmetry s.fst (𝒰.f i)).hom ≫
        pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯ ≫ pullback.snd (𝒰.f i ≫ f) g =
    pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      (pullbackSymmetry s.fst (𝒰.f j)).hom ≫
        pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯ ≫ pullback.snd (𝒰.f j ≫ f) g

Tactic:
pullback.lift_snd,

Goal state after:
case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ pullback.fst ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      (pullbackSymmetry s.fst (𝒰.f i)).hom ≫ pullback.snd (𝒰.f i) s.fst ≫ s.snd =
    pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      (pullbackSymmetry s.fst (𝒰.f j)).hom ≫
        pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯ ≫ pullback.snd (𝒰.f j ≫ f) g