mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RingHom.Integral

Goal state before:
pp: ⊢ RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ f.IsIntegral

Tactic:
by
  apply isIntegral_stableUnderComposition.respectsIso
  introv x
  rw [← e.apply_symm_apply x]
  apply RingHom.isIntegralElem_map

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

Goal state before:
pp: ⊢ HasAffineProperty (@IsFinite) (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ RingHom.Finite)

Tactic:
rw [HasAffineProperty.affineAnd_iff _ RingHom.finite_respectsIso
    RingHom.finite_localizationPreserves.away RingHom.finite_ofLocalizationSpan]

Goal state after:
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y),
    IsFinite f ↔ IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → (CommRingCat.Hom.hom (Scheme.Hom.app f U)).Finite
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S X : Scheme
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : n
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ConcreteCategory.hom_ofHom,

Goal state after:
n : Type u
S X : Scheme
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : n
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected

Goal state before:
pp: I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cone F
cG : Cone G
f : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
j : I
⊢ ⋯.lift (s.π.app (Classical.arbitrary I)) (hcG.lift ((Cone.postcompose α).obj s)) ⋯ ≫ cF.π.app j = s.π.app j

Tactic:
by
    let f (i : _) : s.pt ⟶ cF.pt :=
      (hf i).lift (s.π.app i) (hcG.lift ((Cone.postcompose α).obj s)) (by simp)
    have (i j : _) : f i = f j := by
      refine constant_of_preserves_morphisms f (fun j₁ j₂ g ↦ ?_) i j
      refine (hf j₂).hom_ext ?_ (by simp [f])
      rw [IsPullback.lift_fst, ← cF.w g, IsPullback.lift_fst_assoc, Cone.w]
    change f _ ≫ _ = _
    rw [this _ j]
    simp [f]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case hX
n : Type u
S : Scheme
inst✝ : IsAffine S
i : n
⊢ (ConcreteCategory.hom
        (Scheme.Hom.app
          (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
            (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X))
          ⊤))
      ((ConcreteCategory.hom
          (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S))))
        (X i)) =
    (CommRingCat.Hom.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) (X i)

Tactic:
ConcreteCategory.hom_ofHom,

Goal state after:
case hX
n : Type u
S : Scheme
inst✝ : IsAffine S
i : n
⊢ (ConcreteCategory.hom
        (Scheme.Hom.app
          (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
            (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X))
          ⊤))
      ((eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S)) (X i)) =
    (CommRingCat.Hom.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) (X i)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₂
n : Type u
R S : CommRingCat
φ : R ⟶ S
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑S))).inv) (X i✝) =
    (ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑S))).inv)
      ((ConcreteCategory.hom (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ)))) (X i✝))

Tactic:
ConcreteCategory.hom_ofHom,

Goal state after:
case h₂
n : Type u
R S : CommRingCat
φ : R ⟶ S
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑S))).inv) (X i✝) =
    (ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑S))).inv)
      ((MvPolynomial.map (CommRingCat.Hom.hom φ)) (X i✝))
Module: Mathlib.Topology.LocallyFinsupp.Pushforward

Goal state before:
pp: X : Type u_1
R : Type u_3
inst✝² : TopologicalSpace X
w : X → R
inst✝¹ : Semiring R
c : locallyFinsupp X R
inst✝ : PrespectralSpace X
hw : ∀ (z : X), w z = 1
⊢ map id w ⋯ c = c

Tactic:
by
  ext
  simp [map, hw]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: X Y Z : Scheme
inst✝³ : PreirreducibleSpace ↥X
inst✝² : Nonempty ↥Y
f₁ f₂ : X.PartialMap Y
inst✝¹ : IsDominant f₁.hom
inst✝ : IsDominant f₂.hom
h : f₁.equiv f₂
g : Y.PartialMap Z
⊢ (f₁.comp g).equiv (f₂.comp g)

Tactic:
obtain ⟨W, hW, hW₁, hW₂, e⟩ := h
  replace e : f₁.restrict W hW hW₁ = f₂.restrict W hW hW₂ :=
    PartialMap.ext _ _ rfl (by simpa using e)
  replace e := congr($(e).comp g)
  rw [comp_restrict_left, comp_restrict_left] at e
  exact equiv_of_restrict_eq _ _ e

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case e'_3.f.a
R₀ : Type u_1
inst✝² : CommRing R₀
n : ℕ
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := ⋯
q₂ : R →ₐ[R₀] R ⧸ Ideal.span {c} := ⋯
q₂_surjective : Surjective ⇑q₂
e₁ : InductionObj (Localization.Away c) n := ⋯
e₂ : InductionObj (R ⧸ Ideal.span {c}) n := ⋯
degBound_e₁_le : e₁.degBound ≤ e.degBound
degBound_e₂_lt : e₂.degBound < e.degBound
H₁ : Statement R₀ (Localization.Away c) n e₁
H₂ : Statement R₀ (R ⧸ Ideal.span {c}) n e₂
f : R[X]
T₁ : ConstructibleSetData (Localization.Away c)
T₂ : ConstructibleSetData (R ⧸ Ideal.span {c})
hT₁ : comap Polynomial.C '' (zeroLocus (Set.range e₁.val) \ zeroLocus {(mapRingHom ↑q₁) f}) = T₁.toSet
hT₁deg : ∀ x ∈ T₁, x.n ≤ e₁.degBound
hT₂ : comap Polynomial.C '' (zeroLocus (Set.range e₂.val) \ zeroLocus {(mapRingHom ↑q₂) f}) = T₂.toSet
hT₂deg : ∀ x ∈ T₂, x.n ≤ e₂.degBound
x✝ : Invertible (q₁ c) := ⋯
he₁span :
  coeffSubmodule R₀ e₁ ^ e₁.powBound =
    ⅟(q₁ c ^ e₁.powBound) • Submodule.map q₁.toLinearMap (span R₀ ({c} ∪ ⋃ i, coeff(e.val i)) ^ e₁.powBound)
g₁ : (x : BasicConstructibleSetData (Localization.Away c)) → Fin x.n → R
hg₁ : ∀ x ∈ T₁, ∀ (i : Fin x.n), g₁ x i ∈ ↑(span R₀ ({c} ∪ ⋃ i, coeff(e.val i)) ^ e₁.powBound)
hq₁g₁ : ∀ x ∈ T₁, ∀ (i : Fin x.n), q₁.toLinearMap (g₁ x i) = q₁ c ^ e₁.powBound * x.g i
n₁ : Localization.Away c → ℕ
f₁ : Localization.Away c → R
hf₁ : ∀ (x : Localization.Away c), x * q₁ c ^ n₁ x = q₁ (f₁ x)
g₂ : (x : BasicConstructibleSetData (R ⧸ Ideal.span {c})) → Fin x.n → R
hg₂ : ∀ x ∈ T₂, ∀ (i : Fin x.n), g₂ x i ∈ ↑(coeffSubmodule R₀ e ^ e₂.powBound)
hq₂g₂ : ∀ x ∈ T₂, ∀ (i : Fin x.n), q₂.toLinearMap (g₂ x i) = x.g i
f₂ : R ⧸ Ideal.span {c} → R
hf₂ : ∀ (x : R ⧸ Ideal.span {c}), q₂ (f₂ x) = x
S₁ : Finset (BasicConstructibleSetData R) := ⋯
S₂ : Finset (BasicConstructibleSetData R) := ⋯
x : BasicConstructibleSetData (R ⧸ Ideal.span {c})
hxT₂ : x ∈ ↑T₂
⊢ { f := f₂ x.f, n := x.n + 1, g := Fin.cons c (g₂ x) }.toSet ∈ 𝒫 Set.range (comap q₂.toRingHom)

Tactic:
rw [range_comap_of_surjective _ _ q₂_surjective]
          simp only [AlgHom.toRingHom_eq_coe, Ideal.Quotient.mkₐ_ker, zeroLocus_span, q₂]
          exact Set.sdiff_subset.trans (zeroLocus_anti_mono (by simp))

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

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
X : Scheme
𝒰 : X.OpenCover
inst✝ : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis (Set.range fun i ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
this : (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x ∈ Hom.opensRange (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
k : 𝒰.I₀
h : (fun i ↦ Hom.opensRange (𝒰.f i)) k ≤ Hom.opensRange (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
y : ↥(𝒰.X k)
hy : (𝒰.f k) y = (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x
⊢ Hom.opensRange (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) ≤ Hom.opensRange (𝒰.f j)

pp: case refine_3
P : MorphismProperty Scheme
X : Scheme
𝒰 : X.OpenCover
inst✝ : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis (Set.range fun i ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
this : (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x ∈ Hom.opensRange (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
k : 𝒰.I₀
h : (fun i ↦ Hom.opensRange (𝒰.f i)) k ≤ Hom.opensRange (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
y : ↥(𝒰.X k)
hy : (𝒰.f k) y = (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x
⊢ (pullback.lift (IsOpenImmersion.lift (𝒰.f i) (𝒰.f k) ⋯) (IsOpenImmersion.lift (𝒰.f j) (𝒰.f k) ⋯) ⋯) y = x

Tactic:
· simp_rw [pullback.condition, Scheme.Hom.opensRange_comp]
      exact Set.image_subset_range _ _

Goal state after:
case refine_3
P : MorphismProperty Scheme
X : Scheme
𝒰 : X.OpenCover
inst✝ : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis (Set.range fun i ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
this : (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x ∈ Hom.opensRange (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
k : 𝒰.I₀
h : (fun i ↦ Hom.opensRange (𝒰.f i)) k ≤ Hom.opensRange (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
y : ↥(𝒰.X k)
hy : (𝒰.f k) y = (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x
⊢ (pullback.lift (IsOpenImmersion.lift (𝒰.f i) (𝒰.f k) ⋯) (IsOpenImmersion.lift (𝒰.f j) (𝒰.f k) ⋯) ⋯) y = x
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: S : Scheme
𝒰 : S.OpenCover
inst✝² : Category.{u_2, u_1} 𝒰.I₀
inst✝¹ : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝ : Quiver.IsThin 𝒰.I₀
i j : 𝒰.I₀
⊢ ∀ (hij : i ⟶ j), Function.Injective ⇑(d.functor.map hij)

Tactic:
hij

Goal state after:
S : Scheme
𝒰 : S.OpenCover
inst✝² : Category.{u_2, u_1} 𝒰.I₀
inst✝¹ : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝ : Quiver.IsThin 𝒰.I₀
i j : 𝒰.I₀
hij : i ⟶ j
⊢ Function.Injective ⇑(d.functor.map hij)
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: case refine_1.refine_1
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : TopologicalSpace S
U : Set S
hU : IsCompact U
Us : (x : S) → x ∈ U → Set S
hU' : ∀ (x : S) (a : x ∈ U), Us x a ⊆ U
hUx : ∀ (x : S) (a : x ∈ U), x ∈ Us x a
hUo : ∀ (x : S) (a : x ∈ U), IsOpen (Us x a)
hU'' : ∀ (x : S) (a : x ∈ U), IsCompactOpenCovered f (Us x a)
x : S
⊢ x ∈ ⋃ t ∈ {x | ∃ x_1, ∃ (h : x_1 ∈ U), Us x_1 h = ↑x}, ↑t → x ∈ U

Tactic:
simp [Opens.forall]

Goal state after:
case refine_1.refine_1
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : TopologicalSpace S
U : Set S
hU : IsCompact U
Us : (x : S) → x ∈ U → Set S
hU' : ∀ (x : S) (a : x ∈ U), Us x a ⊆ U
hUx : ∀ (x : S) (a : x ∈ U), x ∈ Us x a
hUo : ∀ (x : S) (a : x ∈ U), IsOpen (Us x a)
hU'' : ∀ (x : S) (a : x ∈ U), IsCompactOpenCovered f (Us x a)
x : S
⊢ ∀ (U_1 : Set S), IsOpen U_1 → ∀ (x_1 : S) (x_2 : x_1 ∈ U), Us x_1 ⋯ = U_1 → x ∈ U_1 → x ∈ U
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case pos
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝¹ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k✝ : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : c.val i = 1
k : Fin n
h✝ : k = j
⊢ coeff(0) ⊆ ↑(coeffSubmodule R₀ c)

Tactic:
rintro _ ⟨_, rfl⟩

Goal state after:
case pos
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝¹ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k✝ : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : c.val i = 1
k : Fin n
h✝ : k = j
w✝ : ℕ
⊢ Polynomial.coeff 0 w✝ ∈ ↑(coeffSubmodule R₀ c)
Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact

Goal state before:
pp: S : Scheme
𝒰✝¹ 𝒰✝ : PreZeroHypercover S
K : Precoverage Scheme
X : Scheme
𝒰 : PreZeroHypercover X
inst✝¹ : QuasiCompactCover 𝒰
f : (x : 𝒰.I₀) → PreZeroHypercover (𝒰.X x)
inst✝ : ∀ (x : 𝒰.I₀), QuasiCompactCover (f x)
U : X.Opens
hU : IsAffineOpen U
⊢ IsCompactOpenCovered (fun x ↦ ⇑((𝒰.bind f).f x)) ↑U

Tactic:
obtain ⟨s, hs, V, hcV, hU⟩ := hU.isCompactOpenCovered 𝒰

Goal state after:
S : Scheme
𝒰✝¹ 𝒰✝ : PreZeroHypercover S
K : Precoverage Scheme
X : Scheme
𝒰 : PreZeroHypercover X
inst✝¹ : QuasiCompactCover 𝒰
f : (x : 𝒰.I₀) → PreZeroHypercover (𝒰.X x)
inst✝ : ∀ (x : 𝒰.I₀), QuasiCompactCover (f x)
U : X.Opens
hU✝ : IsAffineOpen U
s : Set 𝒰.I₀
hs : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun x ↦ ↥(𝒰.X x)) i)
hcV : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
hU : ⋃ i, ⋃ (h : i ∈ s), (fun x ↦ ⇑(𝒰.f x)) i '' ↑(V i h) = ↑U
⊢ IsCompactOpenCovered (fun x ↦ ⇑((𝒰.bind f).f x)) ↑U
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case refine_1.refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.129} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.129} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a : J
i j : (𝒱 a).I₀
⊢ ∀ (hij : i ⟶ j),
    Cover.trans (𝒱 a) hij ≫ ((d.cocone j).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor j =
      ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i

Tactic:
hij

Goal state after:
case refine_1.refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.129} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.129} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a : J
i j : (𝒱 a).I₀
hij : i ⟶ j
⊢ Cover.trans (𝒱 a) hij ≫ ((d.cocone j).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor j =
    ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : ¬c.val i = 1
⊢ (Function.update c.val j (c.val j %ₘ c.val i) j).degree.succ < (c.val j).degree.succ

Tactic:
gcongr; simpa using (degree_modByMonic_lt _ hi).trans_le hle

Goal state after:
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case refine_1.refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.117} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.117} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := d.relativeGluingData.cover
s : Cocone D
i j : 𝒱.I₀
⊢ ∀ (hij : i ⟶ j),
    Cover.trans 𝒱 hij ≫
        ((d.isColimit j).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f j)).mapCocone s)).left ≫
          pullback.fst s.pt.hom (𝒰.f j) =
      ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)).left ≫
        pullback.fst s.pt.hom (𝒰.f i)

Tactic:
hij

Goal state after:
case refine_1.refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.117} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.117} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := d.relativeGluingData.cover
s : Cocone D
i j : 𝒱.I₀
hij : i ⟶ j
⊢ Cover.trans 𝒱 hij ≫
      ((d.isColimit j).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f j)).mapCocone s)).left ≫
        pullback.fst s.pt.hom (𝒰.f j) =
    ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)).left ≫
      pullback.fst s.pt.hom (𝒰.f i)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W : Affine R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective ⇑f
x y : A
⊢ (W⁄B).Equation (f x) (f y) ↔ ((W⁄A).map ↑f).Equation (↑f x) (↑f y)

Tactic:
map_baseChange,

Goal state after:
R : Type r
inst✝¹⁰ : CommRing R
W : Affine R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective ⇑f
x y : A
⊢ (W⁄B).Equation (f x) (f y) ↔ (W⁄B).Equation (↑f x) (↑f y)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W : Affine R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective ⇑f
x y : A
⊢ (W⁄B).Nonsingular (f x) (f y) ↔ (W⁄A).Nonsingular x y

Tactic:
← map_nonsingular _ hf,

Goal state after:
R : Type r
inst✝¹⁰ : CommRing R
W : Affine R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective ⇑f
x y : A
⊢ (W⁄B).Nonsingular (f x) (f y) ↔ ((W⁄A).map f.toRingHom).Nonsingular (f.toRingHom x) (f.toRingHom y)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W : Affine R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective ⇑f
x y : A
⊢ (W⁄B).Nonsingular (f x) (f y) ↔ ((W⁄A).map ↑f).Nonsingular (↑f x) (↑f y)

Tactic:
map_baseChange,

Goal state after:
R : Type r
inst✝¹⁰ : CommRing R
W : Affine R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective ⇑f
x y : A
⊢ (W⁄B).Nonsingular (f x) (f y) ↔ (W⁄B).Nonsingular (↑f x) (↑f y)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case inr
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
Y_rw :
  (Y - C (C y)) * (Y - C (C (W.negY x y))) -
      C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
    W.polynomial * 1
hy : 2 * y + W.a₁ * x + W.a₃ ≠ 0
⊢ ∃ a a_1 a_2 a_3,
    a_3 * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
      1 + a * C (X - C x) + a_1 * (Y - C (C y)) + a_2 * (Y - C (C (W.negY x y)))

Tactic:
let W_Y := 2 * y + W.a₁ * x + W.a₃

Goal state after:
case inr
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
Y_rw :
  (Y - C (C y)) * (Y - C (C (W.negY x y))) -
      C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
    W.polynomial * 1
hy : 2 * y + W.a₁ * x + W.a₃ ≠ 0
W_Y : F := 2 * y + W.a₁ * x + W.a₃
⊢ ∃ a a_1 a_2 a_3,
    a_3 * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
      1 + a * C (X - C x) + a_1 * (Y - C (C y)) + a_2 * (Y - C (C (W.negY x y)))