mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Star.CHSH

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : IsOrderedModule ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ √2 ^ 3 • 1

Tactic:
by
  -- abel will create `ℤ` multiplication. We will `simp` them away to `ℝ` multiplication.
  have M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = ((m : ℝ) * a) • x := fun m a x => by
    rw [← Int.cast_smul_eq_zsmul ℝ, ← mul_smul]
  let P := (√2)⁻¹ • (A₁ + A₀) - B₀
  let Q := (√2)⁻¹ • (A₁ - A₀) + B₁
  have w : √2 ^ 3 • (1 : R) - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (√2)⁻¹ • (P ^ 2 + Q ^ 2) := by
    dsimp [P, Q]
    -- distribute out all the powers and products appearing on the RHS
    simp only [sq, sub_mul, mul_sub, add_mul, mul_add, smul_add, smul_sub]
    -- pull all coefficients out to the front, and combine `√2`s where possible
    simp only [Algebra.mul_smul_comm, Algebra.smul_mul_assoc, ← mul_smul, sqrt_two_inv_mul_self]
    -- replace Aᵢ * Aᵢ = 1 and Bᵢ * Bᵢ = 1
    simp only [← sq, T.A₀_inv, T.A₁_inv, T.B₀_inv, T.B₁_inv]
    -- move Aᵢ to the left of Bᵢ
    simp only [← T.A₀B₀_commutes, ← T.A₀B₁_commutes, ← T.A₁B₀_commutes, ← T.A₁B₁_commutes]
    -- collect terms, simplify coefficients, and collect terms again:
    abel_nf
    -- all terms coincide, but the last one. Simplify all other terms
    simp only [M]
    simp only [neg_mul, mul_inv_cancel_of_invertible, add_assoc, add_comm,
      add_left_comm, one_smul, Int.cast_neg, neg_smul, Int.cast_ofNat, ← add_smul]
    grind
  have pos : 0 ≤ (√2)⁻¹ • (P ^ 2 + Q ^ 2) := by
    have P_sa : star P = P := by
      simp only [P, star_smul, star_add, star_sub, star_id_of_comm, T.A₀_sa, T.A₁_sa, T.B₀_sa]
    have Q_sa : star Q = Q := by
      simp only [Q, star_smul, star_add, star_sub, star_id_of_comm, T.A₀_sa, T.A₁_sa, T.B₁_sa]
    have P2_nonneg : 0 ≤ P ^ 2 := by simpa only [P_sa, sq] using star_mul_self_nonneg P
    have Q2_nonneg : 0 ≤ Q ^ 2 := by simpa only [Q_sa, sq] using star_mul_self_nonneg Q
    positivity
  apply le_of_sub_nonneg
  simpa only [sub_add_eq_sub_sub, ← sub_add, w, Nat.cast_zero] using pos

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
a : R
n : ℕ
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ a • X ^ n = (monomial n) a

Tactic:
rw [eq_comm]

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
a : R
n : ℕ
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ (monomial n) a = a • X ^ n
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
f : ℕ → R → S
⊢ sum 0 f = 0

Tactic:
simp [sum_def', zero_def]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : AddMonoid S
inst✝ : StarAddMonoid S
this : Star R := e.star
⊢ StarAddMonoid R

Tactic:
let := e.addMonoid

Goal state after:
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : AddMonoid S
inst✝ : StarAddMonoid S
this✝ : Star R := e.star
this : AddMonoid R := e.addMonoid
⊢ StarAddMonoid R
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra S R
inst✝ : Algebra.IsCentral S R
u v : ↥(unitary R)
| (conjStarAlgAut S R) u = (conjStarAlgAut S R) v

Tactic:
rw [eq_comm]

Goal state after:
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra S R
inst✝ : Algebra.IsCentral S R
u v : ↥(unitary R)
| (conjStarAlgAut S R) v = (conjStarAlgAut S R) u
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)
| (conjStarAlgAut S R) u = (conjStarAlgAut S R) v

Tactic:
rw [eq_comm]

Goal state after:
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)
| (conjStarAlgAut S R) v = (conjStarAlgAut S R) u
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
M : Type u_6
α : Type u_7
inst✝³ : Monoid G
inst✝² : AddCommMonoid M
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid k
g : G
f f' : SkewMonoidAlgebra k G
⊢ g • (f + f') = g • f + g • f'

Tactic:
by
    ext
    simp [comapSMul_def, map_add]

Goal state after:
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)
i j k : Jᵒᵖ
f : i ⟶ j
g : j ⟶ k
⊢ (F.map (f ≫ g).unop).c.app (op ((Opens.map (colimit.ι F (unop i)).base).obj U)) ≫
      (F.obj (unop k)).presheaf.map (eqToHom ⋯) =
    ((F.map f.unop).c.app (op ((Opens.map (colimit.ι F (unop i)).base).obj U)) ≫
        (F.obj (unop j)).presheaf.map (eqToHom ⋯)) ≫
      (F.map g.unop).c.app (op ((Opens.map (colimit.ι F (unop j)).base).obj U)) ≫
        (F.obj (unop k)).presheaf.map (eqToHom ⋯)

Tactic:
simp only [assoc, CategoryTheory.NatTrans.naturality_assoc]

Goal state after:
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)
i j k : Jᵒᵖ
f : i ⟶ j
g : j ⟶ k
⊢ (F.map (f ≫ g).unop).c.app (op ((Opens.map (colimit.ι F (unop i)).base).obj U)) ≫
      (F.obj (unop k)).presheaf.map (eqToHom ⋯) =
    (F.map f.unop).c.app (op ((Opens.map (colimit.ι F (unop i)).base).obj U)) ≫
      (F.map g.unop).c.app
          ((Opens.map (F.map f.unop).base).op.obj (op ((Opens.map (colimit.ι F (unop i)).base).obj U))) ≫
        ((pushforward C (F.map g.unop).base).obj (F.obj (unop k)).presheaf).map (eqToHom ⋯) ≫
          (F.obj (unop k)).presheaf.map (eqToHom ⋯)
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X✝ X Y : LocallyRingedSpace
f : X.toSheafedSpace ⟶ Y.toSheafedSpace
h : ∀ (x : ↑X.toTopCat), IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap f.hom x))
⊢ ∀ (x : ↑↑X.toPresheafedSpace), IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap f.hom x))

Tactic:
assumption

Goal state after:
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:
by
  rw [← stalkMap_comp, LocallyRingedSpace.stalkMap_congr_hom (e.inv ≫ e.hom) (𝟙 _) (by simp)]
  simp

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

Goal state before:
pp: case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
this :
  X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (i ≫ inv i))) f) =
    unop U ⊓ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)
⊢ X.basicOpen f ≤ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)

Tactic:
IsIso.hom_inv_id,

Goal state after:
case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
this :
  X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (𝟙 U))) f) =
    unop U ⊓ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)
⊢ X.basicOpen f ≤ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T✝ : ↑X → Type u_1
T : Type ?u.10
inst✝ : TopologicalSpace T
U : Opens ↑X
f : ↥U → T
w : ∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (X.continuousPrelocal T).pred fun x ↦ f (i x)
⊢ (X.continuousPrelocal T).pred f

Tactic:
apply continuous_iff_continuousAt.2

Goal state after:
X : TopCat
T✝ : ↑X → Type u_1
T : Type ?u.10
inst✝ : TopologicalSpace T
U : Opens ↑X
f : ↥U → T
w : ∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (X.continuousPrelocal T).pred fun x ↦ f (i x)
⊢ ∀ (x : ↥U), ContinuousAt f x
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : LocallyRingedSpace
f : X ⟶ Y
inst✝ : LocallyRingedSpace.IsOpenImmersion f
⊢ PresheafedSpace.IsOpenImmersion f.toHom

Tactic:
assumption

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case inl
X : Scheme
b : ↥X
hx : IsClosed {b}
a✝ : b ≤ b
⊢ b ≤ b

Tactic:
assumption

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

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

Tactic:
have : IsIso f.c := NatIso.isIso_of_isIso_app _

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
this✝ : ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)
this : IsIso f.c
⊢ IsIso f
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R : CommRingCat
f : ↑R
x : ↥(Spec R)
⊢ x ∈ ↑((Spec R).basicOpen ((ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) f)) ↔ x ∈ ↑(PrimeSpectrum.basicOpen f)

Tactic:
simp only [SetLike.mem_coe, Scheme.mem_basicOpen_top]

Goal state after:
R : CommRingCat
f : ↑R
x : ↥(Spec R)
⊢ IsUnit
      ((ConcreteCategory.hom ((Spec R).presheaf.germ ⊤ x _root_.trivial))
        ((ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) f)) ↔
    x ∈ PrimeSpectrum.basicOpen f
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ f.toPshHom.c.app (op ((PresheafedSpace.IsOpenImmersion.opensFunctor f.toPshHom).obj U)) ≫ X.presheaf.map (eqToHom ⋯) =
    app f (f ''ᵁ U) ≫ X.presheaf.map (eqToHom ⋯).op

Tactic:
eqToHom_op

Goal state after:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ f.toPshHom.c.app (op ((PresheafedSpace.IsOpenImmersion.opensFunctor f.toPshHom).obj U)) ≫ X.presheaf.map (eqToHom ⋯) =
    app f (f ''ᵁ U) ≫ X.presheaf.map (eqToHom ⋯)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ X.presheaf.map (eqToHom ⋯) = X.presheaf.map (eqToHom ⋯).op

Tactic:
eqToHom_op

Goal state after:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ X.presheaf.map (eqToHom ⋯) = X.presheaf.map (eqToHom ⋯)
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
inst✝ : IsOpenImmersion g
⊢ IsOpenImmersion (limit.π (cospan f g) one)

Tactic:
rw [← limit.w (cospan f g) Hom.inl, cospan_map_inl]
  infer_instance

Goal state after:
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
H' : IsIso (TopCat.Presheaf.stalkPushforward C f.hom.base X.presheaf y)
this :
  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 ≫
        inv (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)

Tactic:
IsIso.hom_inv_id,

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)
this :
  IsIso
    ((TopCat.Presheaf.stalkFunctor C ((ConcreteCategory.hom f.hom.base) y)).map f.hom.c ≫
      𝟙
        ((TopCat.Presheaf.stalkFunctor C ((ConcreteCategory.hom f.hom.base) y)).obj
          ((TopCat.Presheaf.pushforward C f.hom.base).obj X.presheaf)))
⊢ IsIso
    ((TopCat.Presheaf.stalkFunctor C ↑⟨(ConcreteCategory.hom f.hom.base) y, ⋯⟩).map
      (have this := { hom := f.hom.c };
        this).hom)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
inst✝ : Epi f.base
⊢ Epi (forgetToSheafedSpace.map f).hom.base

Tactic:
assumption

Goal state after:
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F✝ : Presheaf CommRingCat X
G : F✝.SubmonoidPresheaf
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ↑(F.presheaf.obj U) := (F.presheaf.submonoidPresheafOfStalk fun x ↦ (↑(F.presheaf.stalk x))⁰).obj U
⊢ m ≤ (↑(F.presheaf.obj U))⁰

Tactic:
rw [← nonZeroDivisorsRight_eq_nonZeroDivisors]

Goal state after:
X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F✝ : Presheaf CommRingCat X
G : F✝.SubmonoidPresheaf
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ↑(F.presheaf.obj U) := (F.presheaf.submonoidPresheafOfStalk fun x ↦ (↑(F.presheaf.stalk x))⁰).obj U
⊢ m ≤ nonZeroDivisorsRight ↑(F.presheaf.obj U)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ IsPullback (X.homOfLE ⋯) (X.homOfLE ⋯) (X.homOfLE hU) (X.homOfLE hV)

Tactic:
refine (isPullback_morphismRestrict (X.homOfLE hV) (W.ι ⁻¹ᵁ U)).of_iso (V.ι.isoImage _ ≪≫
    X.isoOfEq ?_) (W.ι.isoImage _ ≪≫ X.isoOfEq ?_) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_ ?_
  · rw [← TopologicalSpace.Opens.map_comp_obj, ← Scheme.Hom.comp_base, Scheme.homOfLE_ι]
    exact V.functor_map_eq_inf U
  · exact (W.functor_map_eq_inf U).trans (by simpa)
  all_goals { simp [← cancel_mono (Scheme.Opens.ι _)] }

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case e_a
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
⊢ (pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫
      (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f).inv ≫
        pullback.snd f (pullback.fst g (Scheme.Opens.ι U)) ≫ pullback.fst g (Scheme.Opens.ι U) =
    (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫
      pullback.snd f (g ⁻¹ᵁ U).ι ≫ (pullbackRestrictIsoRestrict g U).inv ≫ pullback.fst g (Scheme.Opens.ι U)

Tactic:
pullbackRestrictIsoRestrict_inv_fst,

Goal state after:
case e_a
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
⊢ (pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫
      (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f).inv ≫
        pullback.snd f (pullback.fst g (Scheme.Opens.ι U)) ≫ pullback.fst g (Scheme.Opens.ι U) =
    (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι ≫ (g ⁻¹ᵁ U).ι
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ f ≫ Y.toSpecΓ ≫ inv Y.toSpecΓ = f

Tactic:
IsIso.hom_inv_id,

Goal state after:
X Y : Scheme
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ f ≫ 𝟙 Y = f
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ hU.isoSpec.hom ≫ hU.fromSpec = U.ι

Tactic:
simp [← cancel_epi hU.isoSpec.inv]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
⊢ (equalizerPullbackMapIso hf hg v).hom ≫ pullback.snd (equalizer.ι f g) (pullback.fst s v) =
    equalizer.ι (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯) (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯)

Tactic:
ext <;> simp [equalizerPullbackMapIso]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝² : P.IsLocalAtTarget K
X Y✝ : C
f : X ⟶ Y✝
𝒰 : K.ZeroHypercover Y✝
inst✝¹ : K.HasPullbacks
h : ∀ (i : 𝒰.I₀), P (pullback.snd f (𝒰.f i))
Y : C
i : 𝒰.I₀
inst✝ : HasPullback f (𝒰.f i)
⊢ P (pullback.snd f (𝒰.f i))

Tactic:
exact h _

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝ : P.IsLocalAtSource K
X Y✝ : C
f : X ⟶ Y✝
𝒰 : K.ZeroHypercover X
h : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
Y : C
i : 𝒰.I₀
⊢ P (𝒰.f i ≫ f)

Tactic:
exact h _

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case e_a
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)
r : R
α : stalk (moduleStructurePresheaf R R).presheaf x ≅
  (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).obj ((structurePresheafInCommRingCat R).stalk x) :=
  Limits.colimit.isoColimitCocone
    {
      cocone :=
        (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).mapCocone
          (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInCommRingCat R)),
      isColimit :=
        Limits.isColimitOfPreserves (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat)
          (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙ structurePresheafInCommRingCat R)) }
U : Opens ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
s : ToType ((moduleStructurePresheaf R R).presheaf.obj (op U))
this :
  germ (moduleStructurePresheaf R R).presheaf U x hxU ≫ α.hom =
    (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).map ((structurePresheafInCommRingCat R).germ U x hxU)
⊢ (CommRingCat.Hom.hom ((structurePresheafInCommRingCat R).germ U x hxU)) s =
    (Limits.colimit.isoColimitCocone
            {
              cocone :=
                (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).mapCocone
                  (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInCommRingCat R)),
              isColimit :=
                Limits.isColimitOfPreserves (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat)
                  (Limits.colimit.isColimit
                    ((OpenNhds.inclusion x).op ⋙ structurePresheafInCommRingCat R)) }).addCommGroupIsoToAddEquiv.toFun
      ((ConcreteCategory.hom (germ (moduleStructurePresheaf R R).presheaf U x hxU)) s)

Tactic:
· exact congr($this _).symm

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)
⊢ IsLocalization.AtPrime (↑((structurePresheafInCommRingCat R).stalk x)) x.asIdeal

Tactic:
refine (isLocalizedModule_iff_isLocalization' _ _).mp ?_

Goal state after:
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)
⊢ IsLocalizedModule x.asIdeal.primeCompl (Algebra.linearMap R ↑((structurePresheafInCommRingCat R).stalk x))
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
⊢ (comapFun f y) (LocalizedModule.mk a b) = LocalizedModule.mk (f a) ⟨σ ↑b, ⋯⟩

Tactic:
by
  let := Module.compHom N σ
  let := σ.toAlgebra
  have : IsScalarTower R S N := .of_algebraMap_smul fun _ _ ↦ rfl
  apply ((Module.End.isUnit_iff _).mp (IsLocalizedModule.map_units (S := y.asIdeal.primeCompl)
    (LocalizedModule.mkLinearMap y.asIdeal.primeCompl N) ⟨σ b, b.2⟩)).1
  dsimp
  rw [← (comapFun f y).map_smulₛₗ, LocalizedModule.smul'_mk, ← Submonoid.smul_def,
    LocalizedModule.mk_cancel, ← LocalizedModule.mkLinearMap_apply]
  dsimp [comapFun, Localizations]
  refine (IsLocalizedModule.lift_apply ..).trans ?_
  dsimp
  rw [← LocalizedModule.mk_cancel ⟨σ b.1, b.2⟩, LocalizedModule.smul'_mk]
  rfl

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
a b : (i : D.J) × ↑(D.U i)
x : ↑(D.V (a.fst, b.fst))
e₁ : (ConcreteCategory.hom (D.f a.fst b.fst)) x = a.snd
e₂ : (ConcreteCategory.hom (D.f b.fst a.fst)) ((ConcreteCategory.hom (D.t a.fst b.fst)) x) = b.snd
⊢ (ConcreteCategory.hom (D.f a.fst b.fst))
      ((ConcreteCategory.hom (D.t b.fst a.fst)) ((ConcreteCategory.hom (D.t a.fst b.fst)) x)) =
    (ConcreteCategory.hom (D.f a.fst b.fst)) x

Tactic:
D.t_inv_apply

Goal state after:
D : GlueData
a b : (i : D.J) × ↑(D.U i)
x : ↑(D.V (a.fst, b.fst))
e₁ : (ConcreteCategory.hom (D.f a.fst b.fst)) x = a.snd
e₂ : (ConcreteCategory.hom (D.f b.fst a.fst)) ((ConcreteCategory.hom (D.t a.fst b.fst)) x) = b.snd
⊢ (ConcreteCategory.hom (D.f a.fst b.fst)) x = (ConcreteCategory.hom (D.f a.fst b.fst)) x
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i : D.J
a : ↑(D.U i)
j : D.J
b : ↑(D.U j)
k : D.J
c : ↑(D.U k)
x : ↑(D.V (⟨i, a⟩.fst, ⟨j, b⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, a⟩.fst ⟨j, b⟩.fst)) x = ⟨i, a⟩.snd
e₂ :
  (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨i, a⟩.fst)) ((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x) = ⟨j, b⟩.snd
y : ↑(D.V (⟨j, b⟩.fst, ⟨k, c⟩.fst))
e₃ : (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨k, c⟩.fst)) y = ⟨j, b⟩.snd
e₄ :
  (ConcreteCategory.hom (D.f ⟨k, c⟩.fst ⟨j, b⟩.fst)) ((ConcreteCategory.hom (D.t ⟨j, b⟩.fst ⟨k, c⟩.fst)) y) = ⟨k, c⟩.snd
z : ↑(pullback (D.f j i) (D.f j k)) :=
  (ConcreteCategory.hom (pullbackIsoProdSubtype (D.f j i) (D.f j k)).inv)
    ⟨((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x, y), ⋯⟩
⊢ (ConcreteCategory.hom (D.t j i)) (↑⟨((ConcreteCategory.hom (D.t i j)) x, y), ⋯⟩).1 = x

Tactic:
D.t_inv_apply

Goal state after:
D : GlueData
i : D.J
a : ↑(D.U i)
j : D.J
b : ↑(D.U j)
k : D.J
c : ↑(D.U k)
x : ↑(D.V (⟨i, a⟩.fst, ⟨j, b⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, a⟩.fst ⟨j, b⟩.fst)) x = ⟨i, a⟩.snd
e₂ :
  (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨i, a⟩.fst)) ((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x) = ⟨j, b⟩.snd
y : ↑(D.V (⟨j, b⟩.fst, ⟨k, c⟩.fst))
e₃ : (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨k, c⟩.fst)) y = ⟨j, b⟩.snd
e₄ :
  (ConcreteCategory.hom (D.f ⟨k, c⟩.fst ⟨j, b⟩.fst)) ((ConcreteCategory.hom (D.t ⟨j, b⟩.fst ⟨k, c⟩.fst)) y) = ⟨k, c⟩.snd
z : ↑(pullback (D.f j i) (D.f j k)) :=
  (ConcreteCategory.hom (pullbackIsoProdSubtype (D.f j i) (D.f j k)).inv)
    ⟨((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x, y), ⋯⟩
⊢ x = x