mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
ι : Type u_1
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
this : ∀ (i : ι), VX i ≤ iX ⁻¹ᵁ US
algInst✝¹ : Algebra ↑Γ(S, US) ↑Γ(X, UX) := (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).toAlgebra
algInst✝ : Algebra ↑Γ(S, US) ↑Γ(T, UT) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).toAlgebra
algebraizeInst✝ : Module.Flat ↑Γ(S, US) ↑Γ(T, UT)
i : ι
⊢ VX i ≤ iX ⁻¹ᵁ US

Tactic:
by aesop

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S X : Scheme
inst✝ : X.Over S
f : { f // Scheme.Hom.IsOver f S }
⊢ (fun v ↦ ⟨homOfVector (X ↘ S) v, ⋯⟩) ((fun f i ↦ (ConcreteCategory.hom (Scheme.Hom.appTop ↑f)) (coord S i)) f) = f

Tactic:
by
    ext : 2
    · simp [f.2.1]
    · rw [homOfVector_appTop_coord]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n✝ : Type u
S✝ : Scheme
n : Type u
S : Scheme
hS : ∃ R, S = Spec R
⊢ topologically (@IsOpenMap) (𝔸(n; S) ↘ S)

Tactic:
obtain ⟨R, rfl⟩ := hS

Goal state after:
n✝ : Type u
S : Scheme
n : Type u
R : CommRingCat
⊢ topologically (@IsOpenMap) (𝔸(n; Spec R) ↘ Spec R)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
⊢ GeometricallyReduced (𝔸(n; S) ↘ S)

Tactic:
by
  rw [geometricallyReduced_iff]
  introv K h
  apply ObjectProperty.prop_of_iso _
    ((h.isoIsPullback _ _ (isPullback_map _)) ≪≫ (SpecIso n (.of K))).symm
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n✝ : Type u
S✝ : Scheme
n : Type u
S : Scheme
h : IsReduced S
hS : ∃ R, S = Spec R
⊢ IsReduced 𝔸(n; S)

Tactic:
obtain ⟨R, rfl⟩ := hS

Goal state after:
n✝ : Type u
S : Scheme
n : Type u
R : CommRingCat
h : IsReduced (Spec R)
⊢ IsReduced 𝔸(n; Spec R)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n✝ : Type u
S✝ : Scheme
n : Type u
S : Scheme
h : IsIntegralHom (𝔸(n; S) ↘ S)
h✝ : Nonempty ↥S
hS : ∃ R, S = Spec R
⊢ IsEmpty n

Tactic:
obtain ⟨R, rfl⟩ := hS

Goal state after:
n✝ : Type u
S : Scheme
n : Type u
R : CommRingCat
h : IsIntegralHom (𝔸(n; Spec R) ↘ Spec R)
h✝ : Nonempty ↥(Spec R)
⊢ IsEmpty n
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : DecidableEq X
inst✝ : Zero Y
x : X
⊢ single x 0 = 0

Tactic:
by aesop

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case right
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : SemilatticeSup Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ D₂.support).Finite
a : X
ha : a ∈ t₁ ∩ t₂ ∩ Function.support fun z ↦ D₁ z ⊔ D₂ z
⊢ a ∈ t₁ ∩ D₁.support ∪ t₂ ∩ D₂.support

Tactic:
simp_all only [mem_inter_iff, mem_support, ne_eq, mem_union, true_and]

Goal state after:
case right
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : SemilatticeSup Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ D₂.support).Finite
a : X
ha : (a ∈ t₁ ∧ a ∈ t₂) ∧ ¬D₁ a ⊔ D₂ a = 0
⊢ ¬D₁ a = 0 ∨ ¬D₂ a = 0
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case right
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : SemilatticeInf Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ D₂.support).Finite
a : X
ha : a ∈ t₁ ∩ t₂ ∩ Function.support fun z ↦ D₁ z ⊓ D₂ z
⊢ a ∈ t₁ ∩ D₁.support ∪ t₂ ∩ D₂.support

Tactic:
simp_all only [mem_inter_iff, mem_support, ne_eq, mem_union, true_and]

Goal state after:
case right
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : SemilatticeInf Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ D₂.support).Finite
a : X
ha : (a ∈ t₁ ∧ a ∈ t₂) ∧ ¬D₁ a ⊓ D₂ a = 0
⊢ ¬D₁ a = 0 ∨ ¬D₂ a = 0
Module: Mathlib.Topology.LocallyFinsupp.Pushforward

Goal state before:
pp: X : Type u_1
Y : Type u_2
R : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
hf✝ : IsSpectralMap f
w : X → R
inst✝¹ : Semiring R
W : Set Y
hW : IsOpen[inst✝²] W
c✝ : locallyFinsupp X R
inst✝ : PrespectralSpace Y
hf : IsSpectralMap f
c : locallyFinsupp X R
y : Y
x✝ : y ∈ univ
U : Set Y
hU : U ∈ {U | IsOpen[inst✝²] U ∧ IsCompact U} ∧ y ∈ U ∧ U ⊆ ⊤
⊢ (f ⁻¹' (U ∩ {z | (f ⁻¹' {z} ∩ locallyFinsuppWithin.support c).Nonempty}) ∩ locallyFinsuppWithin.support c).Finite

Tactic:
exact (c.locallyFiniteSupport.finite_inter_support_of_isCompact <| hf.2 hU.1.1 hU.1.2).subset
      (by simp; grind)

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

Goal state before:
pp: X Y : Scheme
f g h : X.PartialMap Y
W₁ : X.Opens
hW₁ : Dense ↑W₁
hW₁l : W₁ ≤ f.domain
hW₁r : W₁ ≤ g.domain
e₁ : X.homOfLE hW₁l ≫ f.hom = X.homOfLE hW₁r ≫ g.hom
W₂ : X.Opens
hW₂ : Dense ↑W₂
hW₂l : W₂ ≤ g.domain
hW₂r : W₂ ≤ h.domain
e₂ : X.homOfLE hW₂l ≫ g.hom = X.homOfLE hW₂r ≫ h.hom
⊢ X.homOfLE ⋯ ≫ X.homOfLE hW₁r ≫ g.hom = X.homOfLE ⋯ ≫ X.homOfLE hW₂l ≫ g.hom

Tactic:
simp only [homOfLE_homOfLE_assoc]

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

Goal state before:
pp: X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
f g : X.PartialMap Y
hfg : f.domain = g.domain
inst✝¹ : IsOver S f
inst✝ : IsOver S g
⊢ (f.restrict f.domain ⋯ ⋯).hom = (g.restrict f.domain ⋯ ⋯).hom ↔ f = g

Tactic:
obtain ⟨Uf, _, f⟩ := f

Goal state after:
X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
g : X.PartialMap Y
inst✝¹ : IsOver S g
Uf : X.Opens
dense_domain✝ : Dense ↑Uf
f : ↑Uf ⟶ Y
hfg : { domain := Uf, dense_domain := dense_domain✝, hom := f }.domain = g.domain
inst✝ : IsOver S { domain := Uf, dense_domain := dense_domain✝, hom := f }
⊢ ({ domain := Uf, dense_domain := dense_domain✝, hom := f }.restrict
          { domain := Uf, dense_domain := dense_domain✝, hom := f }.domain ⋯ ⋯).hom =
      (g.restrict { domain := Uf, dense_domain := dense_domain✝, hom := f }.domain ⋯ ⋯).hom ↔
    { domain := Uf, dense_domain := dense_domain✝, hom := f } = g
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝ : IrreducibleSpace ↥X
f : X ⤏ Y
⊢ Spec X.functionField ⟶ Y

Tactic:
refine Quotient.lift PartialMap.fromFunctionField ?_ f

Goal state after:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝ : IrreducibleSpace ↥X
f : X ⤏ Y
⊢ ∀ (a b : X.PartialMap Y), a ≈ b → a.fromFunctionField = b.fromFunctionField
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
f : X ⤏ Y
⊢ { I₀ := ↑{x | ∃ g, ∃ (_ : g.toRationalMap = f), g.domain = x}, X := fun U ↦ ↑↑U,
        f := fun U ↦ X.homOfLE ⋯ }.presieve₀ ∈
    (precoverage IsOpenImmersion).coverings ↑f.domain

Tactic:
by
    rw [presieve₀_mem_precoverage_iff]
    refine ⟨fun x ↦ ?_, inferInstance⟩
    use ⟨_, (TopologicalSpace.Opens.mem_sSup.mp x.2).choose_spec.1⟩
    exact ⟨⟨x.1, (TopologicalSpace.Opens.mem_sSup.mp x.2).choose_spec.2⟩, Subtype.ext (by simp)⟩

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

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_1, u_1} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
l : 𝒰.I₀
gi : l ⟶ i
gj : l ⟶ j
y : ↥(𝒰.X l)
hxij :
  (𝒰.trans fi) ((pullback.fst (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y)) =
    (𝒰.trans fj) ((pullback.snd (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y))
this :
  (𝒰.f i) ((pullback.fst (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y)) =
    (𝒰.f j) ((pullback.snd (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y))
⊢ ∃ l_1 fli flj x,
    (ConcreteCategory.hom ((𝒰.functorOfLocallyDirected ⋙ forget).map fli)) x =
        (pullback.fst (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y) ∧
      (ConcreteCategory.hom ((𝒰.functorOfLocallyDirected ⋙ forget).map flj)) x =
        (pullback.snd (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y)

Tactic:
refine ⟨l, gi, gj, y, ?_, ?_⟩

Goal state after:
case refine_1
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_1, u_1} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
l : 𝒰.I₀
gi : l ⟶ i
gj : l ⟶ j
y : ↥(𝒰.X l)
hxij :
  (𝒰.trans fi) ((pullback.fst (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y)) =
    (𝒰.trans fj) ((pullback.snd (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y))
this :
  (𝒰.f i) ((pullback.fst (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y)) =
    (𝒰.f j) ((pullback.snd (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y))
⊢ (ConcreteCategory.hom ((𝒰.functorOfLocallyDirected ⋙ forget).map gi)) y =
    (pullback.fst (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y)

case refine_2
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_1, u_1} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
l : 𝒰.I₀
gi : l ⟶ i
gj : l ⟶ j
y : ↥(𝒰.X l)
hxij :
  (𝒰.trans fi) ((pullback.fst (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y)) =
    (𝒰.trans fj) ((pullback.snd (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y))
this :
  (𝒰.f i) ((pullback.fst (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y)) =
    (𝒰.f j) ((pullback.snd (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y))
⊢ (ConcreteCategory.hom ((𝒰.functorOfLocallyDirected ⋙ forget).map gj)) y =
    (pullback.snd (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y)
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
s : Set (TopologicalSpace.Opens ↥c.pt)
hs : s ⊆ {x | ∃ i V, ∃ (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
hsf : s.Finite
hU : IsCompact ↑(sSup s)
this : Finite ↑s
i : ↑s → I
V : (x : ↑s) → (D.obj (i x)).Opens
hV : ∀ (x : ↑s), IsAffineOpen (V x)
hVi : ∀ (x : ↑s), c.π.app (i x) ⁻¹ᵁ V x = ↑x
j : I
fj : ∀ {X : I}, X ∈ Finset.image (fun x ↦ i ⟨↑x, ⋯⟩) hsf.toFinset.attach → Nonempty (j ⟶ X)
b : ↑s
⊢ i b ∈ Finset.image (fun x ↦ i ⟨↑x, ⋯⟩) hsf.toFinset.attach

Tactic:
by simpa using ⟨b.1, b.2, rfl⟩

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

Goal state before:

Tactic:
span R₀ ({c} ∪ ⋃ i, coeff(e i)) ^ e₁.powBound
        _ ≤ span R₀ (⋃ i, coeff(e i)) ^ e₁.powBound := by
          gcongr; simpa [Set.insert_subset_iff] using ⟨_, _, hi.symm⟩
        _ ≤ e.coeffSubmodule R₀ ^ e.powBound := by
          unfold coeffSubmodule powBound
          gcongr
          · exact one_le_coeffSubmodule
          · exact Set.subset_union_right
          · lia

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁷ : Category.{u, u} I
X : Scheme
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁶ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝⁵ : IsCofiltered I
inst✝⁴ : IsAffine X
inst✝³ : ∀ (i : I), IsAffine (D.obj i)
inst✝² : IsAffine c.pt
i : I
a : D.obj i ⟶ X
j : I
b : D.obj j ⟶ X
hab : c.π.app i ≫ a = c.π.app j ≫ b
S : Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsAffine S
ha : t.app i = a ≫ f
hb : t.app j = b ≫ f
hS : ∃ R, S = Spec R
⊢ ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b

Tactic:
obtain ⟨R, rfl⟩ := hS

Goal state after:
I : Type u
inst✝⁷ : Category.{u, u} I
X : Scheme
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁶ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝⁵ : IsCofiltered I
inst✝⁴ : IsAffine X
inst✝³ : ∀ (i : I), IsAffine (D.obj i)
inst✝² : IsAffine c.pt
i : I
a : D.obj i ⟶ X
j : I
b : D.obj j ⟶ X
hab : c.π.app i ≫ a = c.π.app j ≫ b
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
f : X ⟶ Spec R
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsAffine (Spec R)
ha : t.app i = a ≫ f
hb : t.app j = b ≫ f
⊢ ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: J : Type u_1
inst✝² : Category.{u_2, u_1} J
F G : J ⥤ Scheme
s : F ⟶ G
inst✝¹ : Quiver.IsThin J
hs : NatTrans.Equifibered s
H : ∀ {i j : J} (hij : i ⟶ j), Function.Injective ⇑(F.map hij)
inst✝ : (G ⋙ forget).IsLocallyDirected
i j k : J
fi : i ⟶ k
fj : j ⟶ k
xi : (F ⋙ forget).obj i
xj : (F ⋙ forget).obj j
heq : (F.map fi) xi = (F.map fj) xj
⊢ (G.map fi) ((s.app i) xi) = (G.map fj) ((s.app j) xj)

Tactic:
rw [← Scheme.Hom.comp_apply, ← s.naturality, Scheme.Hom.comp_apply, heq,
        ← Scheme.Hom.comp_apply, s.naturality]

Goal state after:
J : Type u_1
inst✝² : Category.{u_2, u_1} J
F G : J ⥤ Scheme
s : F ⟶ G
inst✝¹ : Quiver.IsThin J
hs : NatTrans.Equifibered s
H : ∀ {i j : J} (hij : i ⟶ j), Function.Injective ⇑(F.map hij)
inst✝ : (G ⋙ forget).IsLocallyDirected
i j k : J
fi : i ⟶ k
fj : j ⟶ k
xi : (F ⋙ forget).obj i
xj : (F ⋙ forget).obj j
heq : (F.map fi) xi = (F.map fj) xj
⊢ (s.app j ≫ G.map fj) xj = (G.map fj) ((s.app j) xj)
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: case h
S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{u_2, u_1} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, u_1} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i j k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
xk : ↥(d.functor.obj k)
h2 : (d.natTrans.app k) xk = uk
x✝ : (colimit.ι d.functor j) ((d.functor.map fj) xk) ∈ ⇑d.toBase ⁻¹' Set.range ⇑(𝒰.f i)
h✝ : (trans 𝒰 fj) uk = (d.natTrans.app j) ((d.functor.map fj) xk)
h : (𝒰.f i) ((trans 𝒰 fi) uk) = d.toBase ((colimit.ι d.functor j) ((d.functor.map fj) xk))
⊢ (colimit.ι d.functor i) ((d.functor.map fi) xk) = (colimit.ι d.functor j) ((d.functor.map fj) xk)

Tactic:
simp [← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply]

Goal state after:
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: 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
s : Set (Opens S)
hs : ⋃ t ∈ s, ↑t = U
H : ∀ t ∈ s, IsCompactOpenCovered f ↑t
t : Finset ↑s
ht : U ⊆ ⋃ i ∈ t, ↑↑i
x : S
h : x ∈ ⋃ t_1 ∈ SetLike.coe '' ↑(Finset.image Subtype.val t), t_1
⊢ x ∈ U

Tactic:
by aesop

Goal state after:
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
B : (i : ι) → Set (Opens (X i))
hB : ∀ (i : ι), IsBasis (B i)
hBc : ∀ (i : ι), ∀ U ∈ B i, IsCompact U.carrier
U : Set S
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hunion : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
Us : (i : ↑s) → Set (Opens (X ↑i))
UsB : ∀ (i : ↑s), Us i ⊆ B ↑i
hUsf : ∀ (i : ↑s), (Us i).Finite
hUs : ∀ (i : ↑s), V ↑i ⋯ = sSup (Us i)
σ : Type (max u_2 u_3) := (i : ↑s) × ↑(Us i)
this✝ : Finite ↑s
this : ∀ (i : ↑s), Finite ↑(Us i)
x : S
x✝ : ∃ i, x ∈ (fun a ↦ f (↑i.fst) a) '' ↑↑i.snd
i : σ
hi : X ↑i.fst
o : hi ∈ ↑↑i.snd
ho : (fun a ↦ f (↑i.fst) a) hi = x
⊢ ∃ i, ∃ (i_1 : i ∈ s), x ∈ f i '' ↑(V i i_1)

Tactic:
by aesop

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves

Goal state before:
pp: C✝ : Type u_1
inst✝⁶ : Category.{v_1, u_1} C✝
D✝ : Type u_2
inst✝⁵ : Category.{v_2, u_2} D✝
C : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : Category.{v_4, u_4} D
X Y : C
f : X ⟶ Y
inst✝² : EffectiveEpi f
F : C ⥤ D
inst✝¹ : F.PreservesEffectiveEpis
inst✝ : PreservesLimitsOfShape WalkingCospan F
c : PullbackCone f f
hc : IsLimit c
⊢ F.map c.fst ≫ F.map f = F.map c.snd ≫ F.map f

Tactic:
by rw [← F.map_comp, c.condition]; simp

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

Goal state before:
pp: case pos
R : Type u_6
inst✝ : CommRing R
M : Submodule ℤ R
hM : 1 ∈ M
S : ConstructibleSetData R[X]
hS : ∀ C ∈ S, ∀ (j : Fin C.n) (k : ℕ), (C.g j).coeff k ∈ M
f : BasicConstructibleSetData R[X] → ConstructibleSetData R
hf₁ :
  ∀ (C : BasicConstructibleSetData R[X]),
    comap Polynomial.C '' (zeroLocus (Set.range { val := C.g }.val) \ zeroLocus {C.f}) = (f C).toSet
hf₂ : ∀ (C : BasicConstructibleSetData R[X]), ∀ C_1 ∈ f C, C_1.n ≤ { val := C.g }.degBound
hf₃ :
  ∀ (C : BasicConstructibleSetData R[X]),
    ∀ C_1 ∈ f C, ∀ (i : Fin C_1.n), C_1.g i ∈ coeffSubmodule ℤ { val := C.g } ^ { val := C.g }.powBound
x : BasicConstructibleSetData R
y : BasicConstructibleSetData R[X]
hy : y ∈ S
hx : x ∈ f y
H : { val := y.g }.degBound ≤ S.degBound
i : Fin x.n
h : S.degBound = 0
⊢ { val := y.g }.degBound ^ { val := y.g }.degBound ≤ S.degBound ^ S.degBound

pp: case neg
R : Type u_6
inst✝ : CommRing R
M : Submodule ℤ R
hM : 1 ∈ M
S : ConstructibleSetData R[X]
hS : ∀ C ∈ S, ∀ (j : Fin C.n) (k : ℕ), (C.g j).coeff k ∈ M
f : BasicConstructibleSetData R[X] → ConstructibleSetData R
hf₁ :
  ∀ (C : BasicConstructibleSetData R[X]),
    comap Polynomial.C '' (zeroLocus (Set.range { val := C.g }.val) \ zeroLocus {C.f}) = (f C).toSet
hf₂ : ∀ (C : BasicConstructibleSetData R[X]), ∀ C_1 ∈ f C, C_1.n ≤ { val := C.g }.degBound
hf₃ :
  ∀ (C : BasicConstructibleSetData R[X]),
    ∀ C_1 ∈ f C, ∀ (i : Fin C_1.n), C_1.g i ∈ coeffSubmodule ℤ { val := C.g } ^ { val := C.g }.powBound
x : BasicConstructibleSetData R
y : BasicConstructibleSetData R[X]
hy : y ∈ S
hx : x ∈ f y
H : { val := y.g }.degBound ≤ S.degBound
i : Fin x.n
h : ¬S.degBound = 0
⊢ { val := y.g }.degBound ^ { val := y.g }.degBound ≤ S.degBound ^ S.degBound

Tactic:
· have : degBound ⟨y.g⟩ = 0 := by nlinarith
        rw [h, this]

Goal state after:
case neg
R : Type u_6
inst✝ : CommRing R
M : Submodule ℤ R
hM : 1 ∈ M
S : ConstructibleSetData R[X]
hS : ∀ C ∈ S, ∀ (j : Fin C.n) (k : ℕ), (C.g j).coeff k ∈ M
f : BasicConstructibleSetData R[X] → ConstructibleSetData R
hf₁ :
  ∀ (C : BasicConstructibleSetData R[X]),
    comap Polynomial.C '' (zeroLocus (Set.range { val := C.g }.val) \ zeroLocus {C.f}) = (f C).toSet
hf₂ : ∀ (C : BasicConstructibleSetData R[X]), ∀ C_1 ∈ f C, C_1.n ≤ { val := C.g }.degBound
hf₃ :
  ∀ (C : BasicConstructibleSetData R[X]),
    ∀ C_1 ∈ f C, ∀ (i : Fin C_1.n), C_1.g i ∈ coeffSubmodule ℤ { val := C.g } ^ { val := C.g }.powBound
x : BasicConstructibleSetData R
y : BasicConstructibleSetData R[X]
hy : y ∈ S
hx : x ∈ f y
H : { val := y.g }.degBound ≤ S.degBound
i : Fin x.n
h : ¬S.degBound = 0
⊢ { val := y.g }.degBound ^ { val := y.g }.degBound ≤ S.degBound ^ S.degBound
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : Nontrivial R
⊢ W.polynomial.natDegree = 2

Tactic:
rw [polynomial_eq]
  exact Cubic.natDegree_of_b_ne_zero' one_ne_zero

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

Goal state before:
pp: case pos
R : Type u_2
inst✝ : CommRing R
n✝ n : ℕ
IH :
  ∀ {M : Submodule ℤ R},
    1 ∈ M →
      ∀ (k : ℕ) (d : Multiset (Fin n)) (S : ConstructibleSetData (MvPolynomial (Fin n) R)),
        (∀ C ∈ S, C.n ≤ k) →
          (∀ C ∈ S, ∀ (j : Fin C.n), C.g j ∈ coeffsIn (Fin n) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) d)) →
            ∃ T,
              comap MvPolynomial.C '' S.toSet = T.toSet ∧
                ∀ C ∈ T,
                  C.n ≤ numBound k (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) n ∧
                    ∀ (i : Fin C.n), C.g i ∈ M ^ degBound k (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) n
M : Submodule ℤ R
hM : 1 ∈ M
k : ℕ
d : Multiset (Fin (n + 1))
S : ConstructibleSetData (MvPolynomial (Fin (n + 1)) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS :
  ∀ C ∈ S, ∀ (j : Fin C.n), C.g j ∈ coeffsIn (Fin (n + 1)) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin (n + 1)) d)
e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] (MvPolynomial (Fin n) R)[X] := MvPolynomial.finSuccEquiv R n
S' : ConstructibleSetData (MvPolynomial (Fin n) R)[X] := ConstructibleSetData.map e.toRingEquiv.toRingHom S
C : BasicConstructibleSetData (MvPolynomial (Fin (n + 1)) R)
hxS : C ∈ S
j : Fin { f := e C.f, n := C.n, g := ⇑e ∘ C.g }.n
hj : j ∈ Finset.univ
hgj : C.g j = 0
⊢ ((MvPolynomial.finSuccEquiv R n) (C.g j)).degree.succ ≤ 1 + Multiset.count 0 d

Tactic:
hgj,

Goal state after:
case pos
R : Type u_2
inst✝ : CommRing R
n✝ n : ℕ
IH :
  ∀ {M : Submodule ℤ R},
    1 ∈ M →
      ∀ (k : ℕ) (d : Multiset (Fin n)) (S : ConstructibleSetData (MvPolynomial (Fin n) R)),
        (∀ C ∈ S, C.n ≤ k) →
          (∀ C ∈ S, ∀ (j : Fin C.n), C.g j ∈ coeffsIn (Fin n) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) d)) →
            ∃ T,
              comap MvPolynomial.C '' S.toSet = T.toSet ∧
                ∀ C ∈ T,
                  C.n ≤ numBound k (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) n ∧
                    ∀ (i : Fin C.n), C.g i ∈ M ^ degBound k (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) n
M : Submodule ℤ R
hM : 1 ∈ M
k : ℕ
d : Multiset (Fin (n + 1))
S : ConstructibleSetData (MvPolynomial (Fin (n + 1)) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS :
  ∀ C ∈ S, ∀ (j : Fin C.n), C.g j ∈ coeffsIn (Fin (n + 1)) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin (n + 1)) d)
e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] (MvPolynomial (Fin n) R)[X] := MvPolynomial.finSuccEquiv R n
S' : ConstructibleSetData (MvPolynomial (Fin n) R)[X] := ConstructibleSetData.map e.toRingEquiv.toRingHom S
C : BasicConstructibleSetData (MvPolynomial (Fin (n + 1)) R)
hxS : C ∈ S
j : Fin { f := e C.f, n := C.n, g := ⇑e ∘ C.g }.n
hj : j ∈ Finset.univ
hgj : C.g j = 0
⊢ ((MvPolynomial.finSuccEquiv R n) 0).degree.succ ≤ 1 + Multiset.count 0 d
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a : ℤ
⊢ W ((a + a).tdiv 2) * W ((a - a).tdiv 2) = W a * W 0

Tactic:
← two_mul,

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a : ℤ
⊢ W ((2 * a).tdiv 2) * W ((a - a).tdiv 2) = W a * W 0
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b : ℤ
⊢ W ((a - b).tdiv 2) * W ((a - -b).tdiv 2) = W ((a + b).tdiv 2) * W ((a - b).tdiv 2)

Tactic:
sub_neg_eq_add,

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b : ℤ
⊢ W ((a - b).tdiv 2) * W ((a + b).tdiv 2) = W ((a + b).tdiv 2) * W ((a - b).tdiv 2)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b : ℤ
⊢ W ((2 * a + 2 * b + (1 + 1)).tdiv 2) * W ((2 * a + 1 - (2 * b + 1)).tdiv 2) = W (a + b + 1) * W (a - b)

Tactic:
← two_mul,

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b : ℤ
⊢ W ((2 * a + 2 * b + 2 * 1).tdiv 2) * W ((2 * a + 1 - (2 * b + 1)).tdiv 2) = W (a + b + 1) * W (a - b)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c d : ℤ
⊢ atomRel W a b c |d| = atomRel W a b c d

Tactic:
by
  simp_rw [atomRel, atom_abs_right]

Goal state after: