mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁸ : CommSemiring k
inst✝⁷ : Monoid G
inst✝⁶ : Monoid H
A : Type u_4
B : Type u_5
inst✝⁵ : Semiring A
inst✝⁴ : Algebra k A
inst✝³ : Semiring B
inst✝² : Algebra k B
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : G →* A
⊢ SkewMonoidAlgebra k G →ₐ[k] A

Tactic:
apply liftNCAlgHom (Algebra.ofId k A) F
    simp_rw [show ∀ (g : G) (r : k), g • r = r by
        exact fun _ _ ↦ smul_algebraMap _ (algebraMap k k _)]
    exact Algebra.commutes _ _

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
a : R
⊢ (⇑φ)^[n] a = ofAdd n • a

Tactic:
induction n with
  | zero => simp
  | succ n hn =>
    simp_all [MulSemiringAction.toRingHom_apply, Function.iterate_succ', -Function.iterate_succ,
      ← mul_smul, mul_comm]

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

Goal state before:
pp: case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ ((single g a).sum fun a₁ b₁ ↦ (single 1 1).sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) = single g a

Tactic:
sum_single_index,

Goal state after:
case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ ((single 1 1).sum fun a₂ b₂ ↦ single (g * a₂) (a * g • b₂)) = single g a

case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ ((single 1 1).sum fun a₂ b₂ ↦ single (g * a₂) (0 * g • b₂)) = 0
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
⊢ a * b = b * a

Tactic:
have hgk (g : G) (r : k) : g • r = r := by
      rw [← Algebra.algebraMap_self_apply r, smul_algebraMap g r]

Goal state after:
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
⊢ a * b = b * a
Module: Mathlib.Algebra.TrivSqZeroExt.Ideal

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ kerIdeal R M ^ 2 = ⊥

Tactic:
simp only [pow_two, eq_bot_iff, mul_le, mem_kerIdeal_iff_inr]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ ∀ (r : TrivSqZeroExt R M), r = inr r.snd → ∀ (s : TrivSqZeroExt R M), s = inr s.snd → r * s ∈ ⊥
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
x y : k
⊢ (↑(singleAddHom 1)).toFun (x * y) = (↑(singleAddHom 1)).toFun x * (↑(singleAddHom 1)).toFun y

Tactic:
simp [ZeroHom.toFun_eq_coe, AddMonoidHom.toZeroHom_coe, singleAddHom_apply,
    single_mul_single, mul_one, one_smul]

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ⅟2 * ⅟2 *
        (unsym a * unsym b * unsym a * unsym a + unsym b * unsym a * unsym a * unsym a +
            unsym a * unsym a * unsym a * unsym b +
          unsym a * unsym a * unsym b * unsym a) -
      ⅟2 * ⅟2 *
        (unsym a * unsym b * unsym a * unsym a + unsym a * unsym a * unsym a * unsym b +
            unsym b * unsym a * unsym a * unsym a +
          unsym a * unsym a * unsym b * unsym a) =
    0

Tactic:
← mul_sub

Goal state after:
case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ⅟2 * ⅟2 *
      (unsym a * unsym b * unsym a * unsym a + unsym b * unsym a * unsym a * unsym a +
            unsym a * unsym a * unsym a * unsym b +
          unsym a * unsym a * unsym b * unsym a -
        (unsym a * unsym b * unsym a * unsym a + unsym a * unsym a * unsym a * unsym b +
            unsym b * unsym a * unsym a * unsym a +
          unsym a * unsym a * unsym b * unsym a)) =
    0
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: case refine_1
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : InvolutiveStar R
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : StarAddMonoid E
inst✝⁴ : StarModule R E
inst✝³ : AddCommMonoid F
inst✝² : Module R F
inst✝¹ : StarAddMonoid F
inst✝ : StarModule R F
f : WithConv (End R E)ˣ
⊢ (star (toConv ↑f.ofConv)).ofConv * (star (toConv ↑f.ofConv⁻¹)).ofConv = 1

Tactic:
rw [mul_eq_comp, ← toConv_injective.eq_iff, ← LinearMap.intrinsicStar_comp']
      simp [← mul_eq_comp, one_eq_id]

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

Goal state before:
pp: case refine_2
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : InvolutiveStar R
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : StarAddMonoid E
inst✝⁴ : StarModule R E
inst✝³ : AddCommMonoid F
inst✝² : Module R F
inst✝¹ : StarAddMonoid F
inst✝ : StarModule R F
f : WithConv (End R E)ˣ
⊢ (star (toConv ↑f.ofConv⁻¹)).ofConv * (star (toConv ↑f.ofConv)).ofConv = 1

Tactic:
rw [mul_eq_comp, ← toConv_injective.eq_iff, ← LinearMap.intrinsicStar_comp']
      simp [← mul_eq_comp, one_eq_id]

Goal state after:
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✝
Γ : 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
u : U
⊢ (Function.support fun g' ↦ A ((coeff B g') u)).IsPWO

Tactic:
by
    refine Set.IsPWO.mono (((of R).symm (B u)).isPWO_support') ?_
    simp only [coeff_apply_apply, Function.support_subset_iff, ne_eq, Function.mem_support]
    intro g' hg' hAB
    exact hg' (by simp [hAB])

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

Goal state before:
pp: case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
f : X ⟶ Y
x y : ↑↑X
h : x ⤳ y
j : OpenNhds ((TopCat.Hom.hom f.base) y)
⊢ f.c.app ((OpenNhds.inclusion ((ConcreteCategory.hom f.base) x)).op.obj (op ⟨↑j, ⋯⟩)) ≫
      X.presheaf.map (𝟙 ((OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op.obj (op ⟨↑j, ⋯⟩))) ≫
        colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf) ((OpenNhds.map f.base x).op.obj (op ⟨↑j, ⋯⟩)) =
    f.c.app ((OpenNhds.inclusion ((ConcreteCategory.hom f.base) y)).op.obj (op j)) ≫
      X.presheaf.map (𝟙 ((OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op.obj (op j))) ≫
        colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf) (op ⟨↑(unop ((OpenNhds.map f.base y).op.obj (op j))), ⋯⟩)

Tactic:
tauto

Goal state after:
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
hxU : x ∈ U
⊢ ∃ i, x ∈ V i

Tactic:
tauto

Goal state after:
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 ((Opens.inclusionTopIso ↑X).inv ≫ (X.ofRestrict ⋯).base)).obj X.presheaf

Tactic:
tauto

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
U : Opens ↑↑Y
hU : ↑U ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ Y.presheaf.map (homOfLE ⋯).op = Y.presheaf.map (eqToHom ⋯)

Tactic:
tauto

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U V : X.Opens
h : U = V
W : (Spec Γ(X, V)).Opens
⊢ Γ(Spec Γ(X, V), W) = Γ(Spec Γ(X, U), Spec.map (X.presheaf.map (eqToHom h).op) ⁻¹ᵁ W)

Tactic:
cases h

Goal state after:
case refl
X : Scheme
U : X.Opens
W : (Spec Γ(X, U)).Opens
⊢ Γ(Spec Γ(X, U), W) = Γ(Spec Γ(X, U), Spec.map (X.presheaf.map (eqToHom ⋯).op) ⁻¹ᵁ W)
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U V : X.Opens
h : U = V
W : (Spec Γ(X, V)).Opens
this : Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
⊢ Hom.app (Spec.map (X.presheaf.map (eqToHom h).op)) W = eqToHom ⋯

Tactic:
cases h

Goal state after:
case refl
X : Scheme
U : X.Opens
this : Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
W : (Spec Γ(X, U)).Opens
⊢ Hom.app (Spec.map (X.presheaf.map (eqToHom ⋯).op)) W = eqToHom ⋯
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:
by
  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.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
⊢ Types.jointlySurjectivePrecoverage.IsStableUnderBaseChange

Tactic:
rw [← Precoverage.comap_id Types.jointlySurjectivePrecoverage]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
⊢ (Precoverage.comap (𝟭 (Type u_2)) Types.jointlySurjectivePrecoverage).IsStableUnderBaseChange
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case w.none
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
⊢ ((pullbackConeOfLeft f g).fst.base ≫ f.base) ≫ (eqToIso ⋯).hom = pullback.fst f.base g.base ≫ f.base

Tactic:
tauto

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : ↑Γ(X, U)
e :
  f ⁻¹ᵁ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) =
    X.basicOpen ((ConcreteCategory.hom (Hom.app f (f ''ᵁ U))) ((ConcreteCategory.hom (Hom.appIso f U).inv) r))
⊢ f ''ᵁ X.basicOpen r = Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r)

Tactic:
rw [Scheme.Hom.appIso_inv_app_apply, Scheme.basicOpen_res, inf_eq_right.mpr _] at e

Goal state after:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : ↑Γ(X, U)
e : f ⁻¹ᵁ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) = X.basicOpen r
⊢ f ''ᵁ X.basicOpen r = Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r)

X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : ↑Γ(X, U)
e : f ⁻¹ᵁ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) = f ⁻¹ᵁ f ''ᵁ U ⊓ X.basicOpen r
⊢ X.basicOpen r ≤ f ⁻¹ᵁ f ''ᵁ U
Module: Mathlib.AlgebraicGeometry.OpenImmersion

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

Tactic:
by
  ext x
  by_cases hx : x ∈ Set.range f
  · obtain ⟨x, rfl⟩ := hx
    simp [f.isOpenEmbedding.injective.mem_set_image, ← Scheme.image_basicOpen]
  · simp only [Set.mem_inter_iff, hx, and_false, iff_false]
    exact fun H ↦ hx (Set.image_subset_range _ _ H)

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

Goal state before:
pp: X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) f = (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) g
⊢ f = g

Tactic:
fapply TopCat.Sheaf.eq_of_locally_eq' X.sheaf
    (fun i ↦ (𝒰.f (𝒰.idx i)).opensRange ⊓ U) _ (fun _ ↦ homOfLE inf_le_right)
  · intro x hx
    simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_inf, Hom.coe_opensRange, Opens.mem_mk,
      Set.mem_iUnion, Set.mem_inter_iff, Set.mem_range, SetLike.mem_coe, exists_and_right]
    refine ⟨?_, hx⟩
    simpa using ⟨_, 𝒰.covers x⟩
  · intro x
    replace h := h (𝒰.idx x)
    rw [← IsOpenImmersion.map_ΓIso_inv] at h
    exact (IsOpenImmersion.ΓIso (𝒰.f (𝒰.idx x)) U).commRingCatIsoToRingEquiv.symm.injective h

Goal state after:
Module: Mathlib.Topology.Category.TopCommRingCat

Goal state before:
pp: X Y : TopCommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget₂ TopCommRingCat TopCat).map f)
i_Top : (forget₂ TopCommRingCat TopCat).obj X ≅ (forget₂ TopCommRingCat TopCat).obj Y :=
  asIso ((forget₂ TopCommRingCat TopCat).map f)
⊢ IsIso f

Tactic:
let e_Ring : X ≃+* Y := { f.1, ((forget TopCat).mapIso i_Top).toEquiv with }

Goal state after:
X Y : TopCommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget₂ TopCommRingCat TopCat).map f)
i_Top : (forget₂ TopCommRingCat TopCat).obj X ≅ (forget₂ TopCommRingCat TopCat).obj Y :=
  asIso ((forget₂ TopCommRingCat TopCat).map f)
e_Ring : X.α ≃+* Y.α :=
  let __src := ↑f;
  let __src_1 := ((forget TopCat).mapIso i_Top).toEquiv;
  { toFun := (↑↑__src).toFun, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
⊢ IsIso f
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: D : GlueData (Type v)
x : D.glued
⊢ ∃ i y, (ConcreteCategory.hom (D.ι i)) y = x

Tactic:
by
  delta CategoryTheory.GlueData.ι
  simp_rw [← Multicoequalizer.ι_sigmaπ D.diagram]
  rcases D.types_π_surjective x with ⟨x', rfl⟩
  rw [← dsimp% ConcreteCategory.congr_hom
    (colimit.isoColimitCocone (Types.coproductColimitCocone _)).hom_inv_id x']
  rcases (colimit.isoColimitCocone (Types.coproductColimitCocone _)).hom x' with ⟨i, y⟩
  refine ⟨i, y, ?_⟩
  simp
  rfl

Goal state after:
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)
⊢ s ∈ I

Tactic:
have (P : Ideal Γ(X, U)) [hP : P.IsPrime] : IsLocalization.AtPrime _ P :=
      hU.isLocalization_stalk' ⟨P, hP⟩ (hU.isoSpec.inv _).2

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
⊢ s ∈ I
Module: Mathlib.AlgebraicGeometry.AffineScheme

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

Tactic:
hU.ideal_le_iff,

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
I J : Ideal ↑Γ(X, U)
⊢ ((∀ (x : ↥X) (h : x ∈ U),
        Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I ≤
          Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J) ∧
      ∀ (x : ↥X) (h : x ∈ U),
        Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J ≤
          Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I) ↔
    ∀ (x : ↥X) (h : x ∈ U),
      Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I ≤
          Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J ∧
        Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J ≤
          Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
U : Set ↑D.glued
⊢ (∀ (j : Discrete (MultispanShape.prod D.J).R),
      IsOpen
        (⇑(ConcreteCategory.hom (colimit.ι (Discrete.functor D.diagram.right) j)) ⁻¹'
          ⇑(ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) ⁻¹'
            ⇑(homeoOfIso (Multicoequalizer.isoCoequalizer D.diagram).symm) ⁻¹' U)) ↔
    ∀ (i : D.J), IsOpen (⇑(ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) ⁻¹' U)

Tactic:
tauto

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case refine_1
X : Scheme
inst✝ : IsAffine X
s : Set ↥X
hs : IsClosed s
⊢ ∃ I, s = X.zeroLocus ↑I

Tactic:
let Z : Set (Spec Γ(X, ⊤)) := X.toΓSpecFun '' s
    have hZ : IsClosed Z := (X.isoSpec.hom.homeomorph).isClosedMap _ hs
    obtain ⟨I, (hI : Z = _)⟩ := (PrimeSpectrum.isClosed_iff_zeroLocus_ideal _).mp hZ
    use I
    simp only [← Scheme.toSpecΓ_preimage_zeroLocus, ← hI, Z]
    symm
    exact Set.preimage_image_eq _ (bijective_of_isIso X.isoSpec.hom.base).injective

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.t i j)) '' ⇑(ConcreteCategory.hom (D.f i j)) ⁻¹' U =
    ⇑(ConcreteCategory.hom (D.f i j)) ∘ ⇑(ConcreteCategory.hom (D.t j i)) ⁻¹' U

Tactic:
rw [← Set.eq_preimage_iff_image_eq, Set.preimage_preimage]

Goal state after:
D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.f i j)) ⁻¹' U =
    (fun x ↦
        (⇑(ConcreteCategory.hom (D.f i j)) ∘ ⇑(ConcreteCategory.hom (D.t j i)))
          ((ConcreteCategory.hom (D.t i j)) x)) ⁻¹'
      U

case hf
D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ Function.Bijective ⇑(ConcreteCategory.hom (D.t i j))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case right.refine_2
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
x : ↥(∐ f)
y :
  ↥((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).X
      (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
hy :
  ((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
        (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
      y =
    x
⊢ Scheme.Hom.stalkMap (Sigma.desc α)
        (((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
            (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
          y) ≫
      Scheme.Hom.stalkMap
        ((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
          (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
        y =
    (X.presheaf.stalkCongr ⋯).hom ≫
      Scheme.Hom.stalkMap (α (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x).as) y

Tactic:
simp [← Scheme.Hom.stalkMap_comp, Scheme.Hom.stalkMap_congr_hom _ _ (colimit.ι_desc _ _)]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: 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 : 𝒰.I₀
⊢ pullback (p1 𝒰 f g) (𝒰.f i) ≅ pullback (𝒰.f i ≫ f) g

Tactic:
fconstructor
  · exact
      pullback.lift (pullback.snd _ _) (pullback.fst _ _ ≫ p2 𝒰 f g)
        (by rw [← pullback.condition_assoc, Category.assoc, p_comm])
  · exact pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst _ _)
      (by rw [gluing_ι, p1, Multicoequalizer.π_desc])
  · apply pullback.hom_ext
    · simpa using lift_comp_ι 𝒰 f g i
    · simp_rw [Category.assoc, pullback.lift_snd, pullback.lift_fst, Category.id_comp]
  · apply pullback.hom_ext
    · simp_rw [Category.assoc, pullback.lift_fst, pullback.lift_snd, Category.id_comp]
    · simp [p2]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case inr
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
hf : P f
hg : P g
⊢ P (Scheme.Cover.pullbackHom (coprodOpenCover X' Y') (coprod.map f g) (Sum.inr PUnit.unit))

Tactic:
· rw [← MorphismProperty.cancel_left_of_respectsIso P
      (isPullback_inr_inr_coprodMap f g).flip.isoPullback.hom]
    convert! hg
    simp [Scheme.Cover.pullbackHom, coprodOpenCover]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    (D.V (j, k)).presheaf.map (homOfLE ⋯).op ≫
      (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
        (D.V (j, k)).presheaf.map
            ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map
              ((Opens.map (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).map (eqToHom ⋯).unop).op) ≫
          (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
              (D.V (j, k)).presheaf.map ((Opens.map (D.t j k).base).map (eqToHom ⋯).unop).op ≫
                (D.V (j, k)).presheaf.map (eqToHom ⋯)

Tactic:
repeat rw [← (D.V (j, k)).presheaf.map_comp]

Goal state after:
case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ eqToHom ⋯) =
    (D.V (j, k)).presheaf.map
      ((homOfLE ⋯).op ≫
        (opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯) ≫
          (opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map
              ((Opens.map (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).map (eqToHom ⋯).unop).op ≫
            (opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯) ≫
              eqToHom ⋯ ≫ ((Opens.map (D.t j k).base).map (eqToHom ⋯).unop).op ≫ eqToHom ⋯)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case refine_4
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
s : PullbackCone (D.ι i) (D.ι j)
m : s.pt ⟶ (D.vPullbackCone i j).pt
e₁ : m ≫ (D.vPullbackCone i j).fst = s.fst
a✝ : m ≫ (D.vPullbackCone i j).snd = s.snd
⊢ m ≫ D.f i j = s.fst

Tactic:
tauto

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: X✝ Y Z : Scheme
f✝ : X✝ ⟶ Y
g : Y ⟶ Z
P : MorphismProperty Scheme
X S : Scheme
f : X ⟶ S
hf : P f
inst✝ : Surjective f
⊢ Presieve.singleton f ∈ (precoverage P).coverings S

Tactic:
rw [singleton_mem_precoverage_iff]

Goal state after:
X✝ Y Z : Scheme
f✝ : X✝ ⟶ Y
g : Y ⟶ Z
P : MorphismProperty Scheme
X S : Scheme
f : X ⟶ S
hf : P f
inst✝ : Surjective f
⊢ Function.Surjective ⇑f ∧ P f
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: M S T : Scheme
inst✝² : M.Over S
f : T ⟶ S
inst✝¹ : MonObj (M.asOver S)
inst✝ : IsCommMonObj (M.asOver S)
⊢ IsCommMonObj ((pullback (M ↘ S) f).asOver T)

Tactic:
unfold asOver OverClass.asOver at *; exact Over.isCommMonObj_mk_pullbackSnd

Goal state after: