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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddMonoid R
⊢ AddMonoid (QuadraticAlgebra R a b)

Tactic:
refine (equivProd a b).injective.addMonoid _ rfl ?_ ?_ <;> intros <;> rfl

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: S : Type u_1
inst✝ : UnitalShelf S
x y : S
⊢ x ◃ x ◃ y = x ◃ y

Tactic:
have h : x ◃ (x ◃ y) = (x ◃ 1) ◃ (x ◃ y) := by rw [act_one]

Goal state after:
S : Type u_1
inst✝ : UnitalShelf S
x y : S
h : x ◃ x ◃ y = (x ◃ 1) ◃ x ◃ y
⊢ x ◃ x ◃ y = x ◃ y
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₃]
⊢ q.lift (x + y) = q.lift x + q.lift y

Tactic:
by
  simp only [lift, re_add, map_add, imI_add, add_smul, imJ_add, imK_add]
  abel

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toDistrib R)

Tactic:
intro _

Goal state after:
R : Type u
a₁✝ : NonUnitalNonAssocSemiring R
⊢ ∀ ⦃a₂ : NonUnitalNonAssocSemiring R⦄, a₁✝.toDistrib = a₂.toDistrib → a₁✝ = a₂
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case a.inr.inr
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
B : Basis A c₁ c₂ c₃
⊢ B.k ∈ ↑B.liftHom.range

Tactic:
use (Basis.self R).k

Goal state after:
case h
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
B : Basis A c₁ c₂ c₃
⊢ B.liftHom.toRingHom (Basis.self R).k = B.k
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonUnitalNonAssocSemiring R)

Tactic:
intro _

Goal state after:
R : Type u
a₁✝ : NonAssocSemiring R
⊢ ∀ ⦃a₂ : NonAssocSemiring R⦄, a₁✝.toNonUnitalNonAssocSemiring = a₂.toNonUnitalNonAssocSemiring → a₁✝ = a₂
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonUnitalNonAssocSemiring R)

Tactic:
intro _

Goal state after:
R : Type u
a₁✝ : NonUnitalNonAssocRing R
⊢ ∀ ⦃a₂ : NonUnitalNonAssocRing R⦄, a₁✝.toNonUnitalNonAssocSemiring = a₂.toNonUnitalNonAssocSemiring → a₁✝ = a₂
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonUnitalSemiring R)

Tactic:
intro _

Goal state after:
R : Type u
a₁✝ : NonUnitalRing R
⊢ ∀ ⦃a₂ : NonUnitalRing R⦄, a₁✝.toNonUnitalSemiring = a₂.toNonUnitalSemiring → a₁✝ = a₂
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonUnitalNonAssocRing R)

Tactic:
intro _

Goal state after:
R : Type u
a₁✝ : NonUnitalRing R
⊢ ∀ ⦃a₂ : NonUnitalRing R⦄, a₁✝.toNonUnitalNonAssocRing = a₂.toNonUnitalNonAssocRing → a₁✝ = a₂
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonAssocSemiring R)

Tactic:
intro _

Goal state after:
R : Type u
a₁✝ : NonAssocRing R
⊢ ∀ ⦃a₂ : NonAssocRing R⦄, a₁✝.toNonAssocSemiring = a₂.toNonAssocSemiring → a₁✝ = a₂
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonUnitalNonAssocRing R)

Tactic:
intro _

Goal state after:
R : Type u
a₁✝ : NonAssocRing R
⊢ ∀ ⦃a₂ : NonAssocRing R⦄, a₁✝.toNonUnitalNonAssocRing = a₂.toNonUnitalNonAssocRing → a₁✝ = a₂
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonUnitalSemiring R)

Tactic:
intro _

Goal state after:
R : Type u
a₁✝ : Semiring R
⊢ ∀ ⦃a₂ : Semiring R⦄, a₁✝.toNonUnitalSemiring = a₂.toNonUnitalSemiring → a₁✝ = a₂
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonAssocSemiring R)

Tactic:
intro _

Goal state after:
R : Type u
a₁✝ : Semiring R
⊢ ∀ ⦃a₂ : Semiring R⦄, a₁✝.toNonAssocSemiring = a₂.toNonAssocSemiring → a₁✝ = a₂
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonUnitalRing R)

Tactic:
intro _

Goal state after:
R : Type u
a₁✝ : Ring R
⊢ ∀ ⦃a₂ : Ring R⦄, toNonUnitalRing = toNonUnitalRing → a₁✝ = a₂
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonAssocRing R)

Tactic:
intro _

Goal state after:
R : Type u
a₁✝ : Ring R
⊢ ∀ ⦃a₂ : Ring R⦄, toNonAssocRing = toNonAssocRing → a₁✝ = a₂
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toSemiring R)

Tactic:
intro _

Goal state after:
R : Type u
a₁✝ : Ring R
⊢ ∀ ⦃a₂ : Ring R⦄, a₁✝.toSemiring = a₂.toSemiring → a₁✝ = a₂
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mp.refl
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ x✝ : R
⊢ RingConGen.Rel r x✝ x✝

Tactic:
exact RingConGen.Rel.refl _

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: S : Type uS
inst✝⁴ : CommSemiring S
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
f : A →ₐ[S] B
s : A → A → Prop
w : ∀ ⦃x y : A⦄, s x y → f x = f y
x : A
⊢ ((liftAlgHom S) ⟨f, w⟩) ((mkAlgHom S s) x) = f x

Tactic:
simp_rw [liftAlgHom_def, preLiftAlgHom_def, mkAlgHom_def, mkRingHom_def]
  rfl

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

Goal state before:
pp: ⊢ (√2)⁻¹ * (√2)⁻¹ = 2⁻¹

Tactic:
by
  rw [← mul_inv]
  simp

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

Goal state before:

Tactic:
star (f * g) a = star (g * f) a := by rw [CommMonoid.mul_comm f g]
      _ = star (g (f (star a))) := rfl
      _ = star (g (star (star (f (star a))))) := by simp only [star_star]
      _ = (star g * star f) a := rfl

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ X.support = {1}

Tactic:
rw [← pow_one X, support_X_pow 1]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p : SkewPolynomial R
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
s : Finset ℕ
hs : p.support ⊆ s
⊢ ∀ x ∈ s, x ∉ p.support → f x (p.coeff x) = 0

Tactic:
intro _

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p : SkewPolynomial R
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
s : Finset ℕ
hs : p.support ⊆ s
x✝ : ℕ
⊢ x✝ ∈ s → x✝ ∉ p.support → f x✝ (p.coeff x✝) = 0
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:
by
  simp [sum_def', zero_def]

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

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

Tactic:
by
  rcases le_total x y with h | h
  · rw [add_eq_left h, add_eq_left (pow_le_pow_left' h _)]
  · rw [add_eq_right h, add_eq_right (pow_le_pow_left' h _)]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
⊢ untrop (∑ i ∈ s, f i) = ⨅ i, untrop (f ↑i)

Tactic:
simpa [← _root_.untrop_sum] using (sum_attach _ _).symm

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

Goal state before:
pp: R : Type u_4
V : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : InvolutiveStar R
inst✝³ : AddCommGroup V
inst✝² : StarAddMonoid V
inst✝¹ : Module R V
inst✝ : StarModule R V
f : WithConv (End R V)
x : R
⊢ x ∈ spectrum R (star f).ofConv ↔ star x ∈ spectrum R f.ofConv

Tactic:
spectrum.mem_iff,

Goal state after:
R : Type u_4
V : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : InvolutiveStar R
inst✝³ : AddCommGroup V
inst✝² : StarAddMonoid V
inst✝¹ : Module R V
inst✝ : StarModule R V
f : WithConv (End R V)
x : R
⊢ ¬IsUnit ((algebraMap R (End R V)) x - (star f).ofConv) ↔ ¬IsUnit ((algebraMap R (End R V)) (star x) - f.ofConv)
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
⊢ Function.Injective ⇑coeff

Tactic:
intro _

Goal state after:
Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
a₁✝ : HVertexOperator Γ R V W
⊢ ∀ ⦃a₂ : HVertexOperator Γ R V W⦄, coeff a₁✝ = coeff a₂ → a₁✝ = a₂
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
h : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : x ∈ V
g : ToType (X.presheaf.obj (op V))
W : Opens ↑↑X.toPresheafedSpace := ⋯
hxW : x ∈ W
heq :
  (ConcreteCategory.hom (X.presheaf.germ W x hxW))
      ((ConcreteCategory.hom (X.presheaf.map (U.infLELeft V).op)) f *
        (ConcreteCategory.hom (X.presheaf.map (U.infLERight V).op)) g) =
    (ConcreteCategory.hom (X.presheaf.germ W x hxW)) 1
W' : Opens ↑↑X.toPresheafedSpace
hxW' : x ∈ W'
i₁ i₂ : W' ⟶ W
heq' :
  (ConcreteCategory.hom (X.presheaf.map i₁.op))
      ((ConcreteCategory.hom (X.presheaf.map (U.infLELeft V).op)) f *
        (ConcreteCategory.hom (X.presheaf.map (U.infLERight V).op)) g) =
    (ConcreteCategory.hom (X.presheaf.map i₂.op)) 1
⊢ IsUnit ((ConcreteCategory.hom (X.presheaf.map (i₁ ≫ U.infLELeft V).op)) f)

Tactic:
simp only [map_mul, map_one] at heq'

Goal state after:
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
h : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : x ∈ V
g : ToType (X.presheaf.obj (op V))
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : x ∈ W
heq :
  (ConcreteCategory.hom (X.presheaf.germ W x hxW))
      ((ConcreteCategory.hom (X.presheaf.map (U.infLELeft V).op)) f *
        (ConcreteCategory.hom (X.presheaf.map (U.infLERight V).op)) g) =
    (ConcreteCategory.hom (X.presheaf.germ W x hxW)) 1
W' : Opens ↑↑X.toPresheafedSpace
hxW' : x ∈ W'
i₁ i₂ : W' ⟶ W
heq' :
  (ConcreteCategory.hom (X.presheaf.map i₁.op)) ((ConcreteCategory.hom (X.presheaf.map (U.infLELeft V).op)) f) *
      (ConcreteCategory.hom (X.presheaf.map i₁.op)) ((ConcreteCategory.hom (X.presheaf.map (U.infLERight V).op)) g) =
    1
⊢ IsUnit ((ConcreteCategory.hom (X.presheaf.map (i₁ ≫ U.infLELeft V).op)) f)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
Z : PresheafedSpace C
g₁ : Z ⟶ X.restrict hf
⊢ ∀ (h : Z ⟶ X.restrict hf), g₁ ≫ X.ofRestrict hf = h ≫ X.ofRestrict hf → g₁ = h

Tactic:
g₂

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ X.restrict hf
⊢ g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf → g₁ = g₂
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R : CommRingCat
⊢ (locallyRingedSpaceMap (𝟙 R)).toHom = (𝟙 (locallyRingedSpaceObj R)).toHom

Tactic:
rw [Spec.locallyRingedSpaceMap_toHom, Spec.sheafedSpaceMap_id]; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case refine_2
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
x : ↥X
H : ∀ f ∈ s, x ∉ X.basicOpen f
f : ↑Γ(X, U)
⊢ ∀ (x_1 y : ↑Γ(X, U)),
    x_1 ∈ Submodule.span (↑Γ(X, U)) s →
      y ∈ Submodule.span (↑Γ(X, U)) s → x ∉ X.basicOpen x_1 → x ∉ X.basicOpen y → x ∉ X.basicOpen (x_1 + y)

pp: case refine_3
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
x : ↥X
H : ∀ f ∈ s, x ∉ X.basicOpen f
f : ↑Γ(X, U)
⊢ ∀ (a x_1 : ↑Γ(X, U)), x_1 ∈ Submodule.span (↑Γ(X, U)) s → x ∉ X.basicOpen x_1 → x ∉ X.basicOpen (a • x_1)

Tactic:
· exact fun a b _ _ ha hb H ↦ (X.basicOpen_add_le a b H).elim ha hb

Goal state after:
case refine_3
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
x : ↥X
H : ∀ f ∈ s, x ∉ X.basicOpen f
f : ↑Γ(X, U)
⊢ ∀ (a x_1 : ↑Γ(X, U)), x_1 ∈ Submodule.span (↑Γ(X, U)) s → x ∉ X.basicOpen x_1 → x ∉ X.basicOpen (a • x_1)
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R : CommRingCat
s : Set ↑Γ(Spec R, ⊤)
⊢ (Spec R).zeroLocus s = PrimeSpectrum.zeroLocus (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) ⁻¹' s)

Tactic:
convert! Spec_zeroLocus_eq_zeroLocus ((Scheme.ΓSpecIso R).inv ⁻¹' s)
  rw [Set.image_preimage_eq]
  exact (ConcreteCategory.bijective_of_isIso (C := CommRingCat) _).2

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ (appIso f U).inv ≫ app f (f ''ᵁ U) ≫ X.presheaf.map (eqToHom ⋯).op = 𝟙 Γ(X, U)

Tactic:
by
  rw [Scheme.Hom.appIso_inv_app_assoc, ← Functor.map_comp, ← X.presheaf.map_id]; rfl

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

Goal state before:
pp: P✝ P : MorphismProperty Scheme
inst✝ : P.IsStableUnderComposition
⊢ (precoverage P).IsStableUnderComposition

Tactic:
dsimp only [precoverage]

Goal state after:
P✝ P : MorphismProperty Scheme
inst✝ : P.IsStableUnderComposition
⊢ (jointlySurjectivePrecoverage ⊓ P.precoverage).IsStableUnderComposition
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: P✝ P : MorphismProperty Scheme
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
⊢ (precoverage P).HasIsos

Tactic:
dsimp only [precoverage]

Goal state after:
P✝ P : MorphismProperty Scheme
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
⊢ (jointlySurjectivePrecoverage ⊓ P.precoverage).HasIsos
Module: Mathlib.AlgebraicGeometry.OpenImmersion

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

Tactic:
by
  rw [hasLimit_iff_of_iso (diagramIsoCospan _)]
  exact inferInstanceAs (HasLimit (cospan ((forget).map g) ((forget).map f)))

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

Goal state before:
pp: case right
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✝ s : PullbackCone f g
⊢ pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd = s.snd ∧
    ∀ {m : s.pt ⟶ (pullbackConeOfLeft f g).pt},
      m ≫ (pullbackConeOfLeft f g).fst = s.fst →
        m ≫ (pullbackConeOfLeft f g).snd = s.snd → m = pullbackConeOfLeftLift f g s

Tactic:
use pullbackConeOfLeftLift_snd f g s

Goal state after:
case right
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✝ s : PullbackCone f g
⊢ ∀ {m : s.pt ⟶ (pullbackConeOfLeft f g).pt},
    m ≫ (pullbackConeOfLeft f g).fst = s.fst →
      m ≫ (pullbackConeOfLeft f g).snd = s.snd → m = pullbackConeOfLeftLift f g s
Module: Mathlib.AlgebraicGeometry.OpenImmersion

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

Tactic:
rw [← pullbackSymmetry_hom_comp_snd]
  infer_instance

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

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

Tactic:
rw [← pullbackSymmetry_hom_comp_snd]
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ MorphismProperty.isomorphisms Scheme ≤ IsOpenImmersion

Tactic:
intro _

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ : Scheme
⊢ ∀ ⦃Y : Scheme⦄ (f : X✝ ⟶ Y), MorphismProperty.isomorphisms Scheme f → IsOpenImmersion f
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ (X Y S : Scheme) (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    IsOpenImmersion g → IsOpenImmersion (pullback.fst f g)

Tactic:
intro X Y Z f g _ H

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
H : IsOpenImmersion g
⊢ IsOpenImmersion (pullback.fst f g)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

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

Tactic:
refine PullbackCone.mk ?_
      (Y.ofRestrict (TopCat.snd_isOpenEmbedding_of_left H.base_open g.base)) ?_

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Y.restrict ⋯ ⟶ X

case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ?refine_1 ≫ f = Y.ofRestrict ⋯ ≫ g
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

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

Tactic:
rw [← pullbackSymmetry_hom_comp_snd]
  infer_instance

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
S : (x : ↑X) → Submonoid ↑(F.stalk x)
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
⊢ ⨅ x, Submonoid.comap (CommRingCat.Hom.hom (F.germ (unop U) ↑x ⋯)) (S ↑x) ≤
    Submonoid.comap (CommRingCat.Hom.hom (F.map i))
      (⨅ x, Submonoid.comap (CommRingCat.Hom.hom (F.germ (unop V) ↑x ⋯)) (S ↑x))

Tactic:
by
    intro s hs
    simp only [Submonoid.mem_comap, Submonoid.mem_iInf] at hs ⊢
    intro x
    change (F.map i.unop.op ≫ F.germ V.unop x.1 x.2) s ∈ _
    rw [F.germ_res]
    exact hs ⟨_, i.unop.le x.2⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ (Spec.map (X.presheaf.map (eqToHom ⋯).op ≫ X.presheaf.germ (U.ι ''ᵁ ⊤) ↑x ⋯ ≫ (U.stalkIso x).inv))
      (closedPoint ↑((↑U).presheaf.stalk x)) =
    (Spec.map (X.presheaf.germ U ↑x ⋯)) (closedPoint ↑(X.presheaf.stalk ↑x))

Tactic:
X.presheaf.germ_res_assoc,

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ (Spec.map (X.presheaf.germ U ↑x ⋯ ≫ (U.stalkIso x).inv)) (closedPoint ↑((↑U).presheaf.stalk x)) =
    (Spec.map (X.presheaf.germ U ↑x ⋯)) (closedPoint ↑(X.presheaf.stalk ↑x))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Set.range ⇑hU.fromSpec = ↑U

Tactic:
delta IsAffineOpen.fromSpec; dsimp [IsAffineOpen.isoSpec_inv]
  rw [Set.range_comp, Set.range_eq_univ.mpr, Set.image_univ]
  · exact Subtype.range_coe
  rw [← TopCat.coe_comp, ← TopCat.epi_iff_surjective]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
⊢ coprod.desc f g ≫ coequalizer.π f g = coprod.desc (𝟙 X) (𝟙 X) ≫ f ≫ coequalizer.π f g

Tactic:
by ext <;> simp [coequalizer.condition f g]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
⊢ f ≫ s.inl = s.inr

Tactic:
simpa using congr(coprod.inl ≫ $s.condition)

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
⊢ (f ≫ coequalizer.π f g) ≫ coequalizer.desc s.inl ⋯ = s.inr

Tactic:
simpa using congr(coprod.inl ≫ $s.condition)

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case e'_3
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
e_1✝ :
  ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) = ↑((structureSheaf ↑Γ(X, U)).obj.obj (op (PrimeSpectrum.basicOpen f)))
e_2✝ : CommRing.toCommSemiring ≍ CommRing.toCommSemiring
⊢ ∀ (r : ↑Γ(X, U)),
    (algebraMap ↑Γ(X, U) ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f)) r =
      (algebraMap ↑Γ(X, U) ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f)) r

Tactic:
intro _

Goal state after:
case e'_3
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
e_1✝ :
  ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) = ↑((structureSheaf ↑Γ(X, U)).obj.obj (op (PrimeSpectrum.basicOpen f)))
e_2✝ : CommRing.toCommSemiring ≍ CommRing.toCommSemiring
r✝ : ↑Γ(X, U)
⊢ (algebraMap ↑Γ(X, U) ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f)) r✝ =
    (algebraMap ↑Γ(X, U) ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f)) r✝
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : ↑Γ(X, U)
I : Ideal ↑Γ(X, U)
H :
  ∀ (x : ↥X) (h : x ∈ U),
    (ConcreteCategory.hom (X.presheaf.germ U x h)) s ∈ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I
this✝ : (x : ↥(Spec Γ(X, U))) → Algebra ↑Γ(X, U) ↑(X.presheaf.stalk (hU.fromSpec x)) :=
  fun x ↦ X.presheaf.algebra_section_stalk ((Scheme.Hom.toLRSHom hU.isoSpec.inv).base.hom' x)
this :
  ∀ (P : Ideal ↑Γ(X, U)) [hP : P.IsPrime],
    IsLocalization.AtPrime (↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := hP }))) P
P : Ideal ↑Γ(X, U)
⊢ ∀ [inst : P.IsMaximal],
    (Algebra.linearMap ↑Γ(X, U) ↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := ⋯ }))) s ∈
      Submodule.localized₀ P.primeCompl
        (Algebra.linearMap ↑Γ(X, U) ↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := ⋯ }))) I

Tactic:
hP

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : ↑Γ(X, U)
I : Ideal ↑Γ(X, U)
H :
  ∀ (x : ↥X) (h : x ∈ U),
    (ConcreteCategory.hom (X.presheaf.germ U x h)) s ∈ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I
this✝ : (x : ↥(Spec Γ(X, U))) → Algebra ↑Γ(X, U) ↑(X.presheaf.stalk (hU.fromSpec x)) :=
  fun x ↦ X.presheaf.algebra_section_stalk ((Scheme.Hom.toLRSHom hU.isoSpec.inv).base.hom' x)
this :
  ∀ (P : Ideal ↑Γ(X, U)) [hP : P.IsPrime],
    IsLocalization.AtPrime (↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := hP }))) P
P : Ideal ↑Γ(X, U)
hP : P.IsMaximal
⊢ (Algebra.linearMap ↑Γ(X, U) ↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := ⋯ }))) s ∈
    Submodule.localized₀ P.primeCompl
      (Algebra.linearMap ↑Γ(X, U) ↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := ⋯ }))) I
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : ↑Γ(X, U)
I : Ideal ↑Γ(X, U)
⊢ s ∈ I ↔
    ∀ (x : ↥X) (h : x ∈ U),
      (ConcreteCategory.hom (X.presheaf.germ U x h)) s ∈ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I

Tactic:
refine ⟨fun hs x hxU ↦ Ideal.mem_map_of_mem _ hs, fun H ↦ ?_⟩
  let (x : _) : Algebra Γ(X, U) (X.presheaf.stalk (hU.fromSpec x)) :=
    TopCat.Presheaf.algebra_section_stalk X.presheaf _
  have (P : Ideal Γ(X, U)) [hP : P.IsPrime] : IsLocalization.AtPrime _ P :=
      hU.isLocalization_stalk' ⟨P, hP⟩ (hU.isoSpec.inv _).2
  refine Submodule.mem_of_localization_maximal
      (fun P hP ↦ X.presheaf.stalk (hU.fromSpec ⟨P, hP.isPrime⟩))
      (fun P hP ↦ Algebra.linearMap _ _) _ _ ?_
  intro P hP
  rw [Ideal.localized₀_eq_restrictScalars_map]
  exact H _ _

Goal state after: