mathlib-initiative/mathlib-tactics huggingface dataset:
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 ⊆ ⊤
⊢ (U ∩ support fun z ↦ ∑ᶠ (x : X) (_ : x ∈ f ⁻¹' {z}), c x * w x).Finite

Tactic:
suffices h : (U ∩ {z | (f ⁻¹' {z} ∩ support ⇑c).Nonempty}).Finite by
      refine h.subset (inter_subset_inter_right U fun y hy ↦ ?_)
      obtain ⟨x, (hx : f x = y), h'⟩ := exists_ne_zero_of_finsum_mem_ne_zero hy
      use x
      grind [mem_support]

Goal state after:
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 ⊆ ⊤
⊢ (U ∩ {z | (f ⁻¹' {z} ∩ support ⇑c).Nonempty}).Finite
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
c : locallyFinsupp X R
inst✝ : PrespectralSpace Y
s : Set X
t : Set Y
hc : locallyFinsuppWithin.support c ⊆ s
h : ∀ x ∈ s, w x ≠ 0 → f x ∈ t
⊢ locallyFinsuppWithin.support (map f w hf c) ⊆ t

Tactic:
intro y hy

Goal state after:
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
c : locallyFinsupp X R
inst✝ : PrespectralSpace Y
s : Set X
t : Set Y
hc : locallyFinsuppWithin.support c ⊆ s
h : ∀ x ∈ s, w x ≠ 0 → f x ∈ t
y : Y
hy : y ∈ locallyFinsuppWithin.support (map f w hf c)
⊢ y ∈ t
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
t : ↑Γ(X, U)
s : ↥(Submonoid.powers f)
ht :
  (algebraMap ↑Γ(X, U) ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) t *
      IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) 1 s ∈
    RingHom.ker (ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hf))
⊢ IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) t s = 0

Tactic:
Ideal.mul_unit_mem_iff_mem,

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
t : ↑Γ(X, U)
s : ↥(Submonoid.powers f)
ht :
  (algebraMap ↑Γ(X, U) ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) t ∈
    RingHom.ker (ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hf))
⊢ IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) t s = 0

case hy
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
t : ↑Γ(X, U)
s : ↥(Submonoid.powers f)
ht :
  (algebraMap ↑Γ(X, U) ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) t *
      IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) 1 s ∈
    RingHom.ker (ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hf))
⊢ IsUnit (IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) 1 s)
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
t : ↑Γ(X, U)
s : ↥(Submonoid.powers f)
ht : (ConcreteCategory.hom (X.presheaf.germ U x ⋯)) t = 0
⊢ IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) 0 s = 0

Tactic:
IsLocalization.mk'_zero

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
t : ↑Γ(X, U)
s : ↥(Submonoid.powers f)
ht : (ConcreteCategory.hom (X.presheaf.germ U x ⋯)) t = 0
⊢ 0 = 0
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case refine_2
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↥(Spec R)
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
x : ↑R
s : ↥(Submonoid.powers f)
hx :
  (algebraMap ↑R ↑((Spec.structureSheaf ↑R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) x *
      IsLocalization.mk' (↑((Spec.structureSheaf ↑R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) 1 s ∈
    RingHom.ker (ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf))
⊢ IsLocalization.mk' (↑((Spec.structureSheaf ↑R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) x s = 0

Tactic:
Ideal.mul_unit_mem_iff_mem,

Goal state after:
case refine_2
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↥(Spec R)
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
x : ↑R
s : ↥(Submonoid.powers f)
hx :
  (algebraMap ↑R ↑((Spec.structureSheaf ↑R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) x ∈
    RingHom.ker (ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf))
⊢ IsLocalization.mk' (↑((Spec.structureSheaf ↑R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) x s = 0

case refine_2.hy
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↥(Spec R)
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
x : ↑R
s : ↥(Submonoid.powers f)
hx :
  (algebraMap ↑R ↑((Spec.structureSheaf ↑R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) x *
      IsLocalization.mk' (↑((Spec.structureSheaf ↑R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) 1 s ∈
    RingHom.ker (ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf))
⊢ IsUnit (IsLocalization.mk' (↑((Spec.structureSheaf ↑R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) 1 s)
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : f x = g x
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
⊢ ∃ U, x ∈ U ∧ U.ι ≫ f = U.ι ≫ g

Tactic:
obtain ⟨_, ⟨V : Y.Opens, hV, rfl⟩, hxV, -⟩ :=
    Y.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ (f x)) isOpen_univ

Goal state after:
X Y : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : f x = g x
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : f x ∈ ↑V
⊢ ∃ U, x ∈ U ∧ U.ι ≫ f = U.ι ≫ g
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case refine_1
X : Scheme
R A : CommRingCat
x : ↥X
inst✝ : X.IsGermInjectiveAt x
U : X.Opens
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
hφRA : (CommRingCat.Hom.hom φRA).FiniteType
e✝ : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
V : X.Opens
hxV : x ∈ V
iVU : V ≤ U
hV : (CommRingCat.Hom.hom φ).range ≤ (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range
V' : X.Opens
hxV' : x ∈ V'
hV' : IsAffineOpen V'
iV'V : V' ≤ V
H : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ V' x hxV'))
f : X.presheaf.obj (Opposite.op V') ⟶ X.presheaf.stalk x := X.presheaf.germ V' x hxV'
hf' : (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range ≤ (CommRingCat.Hom.hom f).range
e : ↑(X.presheaf.obj (Opposite.op V')) ≃+* ↥(ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range :=
  RingEquiv.ofLeftInverse ⋯
a : ↑A
⊢ (ConcreteCategory.hom φ) a =
    ↑(e (e.symm (((CommRingCat.Hom.hom φ).codRestrict (ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range ⋯) a)))

Tactic:
simp only [RingEquiv.apply_symm_apply]

Goal state after:
case refine_1
X : Scheme
R A : CommRingCat
x : ↥X
inst✝ : X.IsGermInjectiveAt x
U : X.Opens
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
hφRA : (CommRingCat.Hom.hom φRA).FiniteType
e✝ : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
V : X.Opens
hxV : x ∈ V
iVU : V ≤ U
hV : (CommRingCat.Hom.hom φ).range ≤ (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range
V' : X.Opens
hxV' : x ∈ V'
hV' : IsAffineOpen V'
iV'V : V' ≤ V
H : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ V' x hxV'))
f : X.presheaf.obj (Opposite.op V') ⟶ X.presheaf.stalk x := X.presheaf.germ V' x hxV'
hf' : (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range ≤ (CommRingCat.Hom.hom f).range
e : ↑(X.presheaf.obj (Opposite.op V')) ≃+* ↥(ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range :=
  RingEquiv.ofLeftInverse ⋯
a : ↑A
⊢ (ConcreteCategory.hom φ) a =
    ↑(((CommRingCat.Hom.hom φ).codRestrict (ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range ⋯) a)
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
U : X.Opens
x : ↥X
hx : x ∈ U
⊢ ∀ (a : ↑(X.presheaf.obj (op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) a = 0 → a = 0

Tactic:
intro y hy

Goal state after:
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
x : ↥X
hx : x ∈ U
y : ↑(X.presheaf.obj (op U))
hy : (ConcreteCategory.hom (X.presheaf.germ U x hx)) y = 0
⊢ y = 0
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↥X
hx : x ∈ U
e : ⟨x, ⋯⟩ = (X.homOfLE hU') ⟨x, hx⟩
⊢ Spec.map (inv (Hom.stalkMap U.ι ⟨x, hx⟩)) ≫
      Spec.map (Hom.stalkMap (X.homOfLE hU') ⟨x, hx⟩) ≫ (↑f.domain).fromSpecStalk ((X.homOfLE hU') ⟨x, hx⟩) ≫ f.hom =
    (Spec.map (inv (Hom.stalkMap f.domain.ι ⟨x, ⋯⟩)) ≫
        Spec.map ((↑f.domain).presheaf.stalkSpecializes ⋯) ≫ (↑f.domain).fromSpecStalk ((X.homOfLE hU') ⟨x, hx⟩)) ≫
      f.hom

Tactic:
← TopCat.Presheaf.stalkCongr_inv _ (Inseparable.of_eq e)

Goal state after:
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↥X
hx : x ∈ U
e : ⟨x, ⋯⟩ = (X.homOfLE hU') ⟨x, hx⟩
⊢ Spec.map (inv (Hom.stalkMap U.ι ⟨x, hx⟩)) ≫
      Spec.map (Hom.stalkMap (X.homOfLE hU') ⟨x, hx⟩) ≫ (↑f.domain).fromSpecStalk ((X.homOfLE hU') ⟨x, hx⟩) ≫ f.hom =
    (Spec.map (inv (Hom.stalkMap f.domain.ι ⟨x, ⋯⟩)) ≫
        Spec.map ((↑f.domain).presheaf.stalkCongr ⋯).inv ≫ (↑f.domain).fromSpecStalk ((X.homOfLE hU') ⟨x, hx⟩)) ≫
      f.hom
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✝¹ : IsCofilteredOrEmpty I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
Z : (i : I) → Set ↥(D.obj i)
hZc : ∀ (i : I), IsClosed (Z i)
hZne : ∀ (i : I), (Z i).Nonempty
hZcpt : ∀ (i : I), IsCompact (Z i)
hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (⇑(D.map f)) (Z i) (Z i')
⊢ ∃ s, ∀ (i : I), (c.π.app i) s ∈ Z i

Tactic:
let D' : I ⥤ Scheme :=
  { obj i := (vanishingIdeal ⟨Z i, hZc i⟩).subscheme
    map {X Y} f := subschemeMap _ _ (D.map f) (by
      rw [map_vanishingIdeal, ← le_support_iff_le_vanishingIdeal]
      simpa [(hZc _).closure_subset_iff] using (hmapsTo f).subset_preimage)
    map_id _ := by simp [← cancel_mono (subschemeι _)]
    map_comp _ _ := by simp [← cancel_mono (subschemeι _)] }

Goal state after:
I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofilteredOrEmpty I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
Z : (i : I) → Set ↥(D.obj i)
hZc : ∀ (i : I), IsClosed (Z i)
hZne : ∀ (i : I), (Z i).Nonempty
hZcpt : ∀ (i : I), IsCompact (Z i)
hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (⇑(D.map f)) (Z i) (Z i')
D' : I ⥤ Scheme :=
  { obj := fun i ↦ (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subscheme,
    map := fun {X Y} f ↦
      (vanishingIdeal { carrier := Z X, isClosed' := ⋯ }).subschemeMap
        (vanishingIdeal { carrier := Z Y, isClosed' := ⋯ }) (D.map f) ⋯,
    map_id := ⋯, map_comp := ⋯ }
⊢ ∃ s, ∀ (i : I), (c.π.app i) s ∈ Z i
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
g : Y.PartialMap Z
⊢ f.toRationalMap.comp g.toRationalMap = (f.comp g).toRationalMap

Tactic:
by
  rw [RationalMap.comp_def, PartialMap.toRationalMap_eq_iff]
  exact PartialMap.comp_equiv_of_equiv_left f.representative_toRationalMap_equiv _

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

Goal state before:
pp: case hP₁
R✝ : Type u_2
inst✝¹ : CommRing R✝
n : ℕ
R : Type u_2
inst✝ : CommRing R
⊢ ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R], Statement R₀ R n { val := 0 }

Tactic:
R₀

Goal state after:
case hP₁
R✝ : Type u_2
inst✝¹ : CommRing R✝
n : ℕ
R : Type u_2
inst✝ : CommRing R
R₀ : Type u_1
⊢ ∀ [inst : CommRing R₀] [inst_1 : Algebra R₀ R], Statement R₀ R n { val := 0 }
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hP₂
R✝ : Type u_2
inst✝¹ : CommRing R✝
n : ℕ
R : Type u_2
inst✝ : CommRing R
g : InductionObj R n
i : Fin n
hi : (g.val i).Monic
hi_min : ∀ (j : Fin n), j ≠ i → g.val j = 0
R₀✝ : Type u_1
⊢ ∀ [inst : CommRing R₀✝] [inst_1 : Algebra R₀✝ R], Statement R₀✝ R n g

Tactic:
R₀

Goal state after:
case hP₂
R✝ : Type u_2
inst✝¹ : CommRing R✝
n : ℕ
R : Type u_2
inst✝ : CommRing R
g : InductionObj R n
i : Fin n
hi : (g.val i).Monic
hi_min : ∀ (j : Fin n), j ≠ i → g.val j = 0
R₀✝ : Type u_1
R₀ : CommRing R₀✝
⊢ ∀ [inst : Algebra R₀✝ R], Statement R₀✝ R n g
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hP₃
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_1 : Algebra R₀ R], Statement R₀ R n c

Tactic:
R₀

Goal state after:
case hP₃
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_1 : Algebra R₀ R], Statement R₀ R n c
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: case intro
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
hU✝ : IsCompactOpenCovered f U
κ : Type ?u.68
w✝ : Finite κ
a : κ → ι
V : (i : κ) → Opens (X (a i))
hB : ∀ (i : κ), V i ∈ B (a i)
hc : ∀ (i : κ), IsCompact (V i).carrier
hU : ⋃ i, f (a i) '' ↑(V i) = U
val✝ : Fintype κ
⊢ ⋃ i, f ((a ∘ ⇑(Fintype.equivFin κ).symm) i) '' ↑((fun i ↦ V ((Fintype.equivFin κ).symm i)) i) = U

Tactic:
simp [← hU, ← (Fintype.equivFin κ).symm.surjective.iUnion_comp, Function.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✝² : ∀ (i : ι), PrespectralSpace (X i)
inst✝¹ : TopologicalSpace S
σ : Type u_4
Y : σ → Type u_5
inst✝ : (i : σ) → TopologicalSpace (Y i)
g : (i : σ) → Y i → S
a : σ → ι
t : (i : σ) → Y i → X (a i)
ht : ∀ (i : σ), Continuous (t i)
hge : ∀ (i : σ), g i = f (a i) ∘ t i
hf : ∀ (i : ι), Continuous (f i)
U : Set S
ho : IsOpen U
hU : ∃ V, IsCompact V.carrier ∧ (fun p ↦ g p.fst p.snd) '' V.carrier = U
⊢ ∃ V, IsCompact V.carrier ∧ (fun p ↦ f p.fst p.snd) '' V.carrier = U

Tactic:
let p : (Σ i, Y i) → (Σ i, X i) := Sigma.map a t

Goal state after:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝³ : (i : ι) → TopologicalSpace (X i)
inst✝² : ∀ (i : ι), PrespectralSpace (X i)
inst✝¹ : TopologicalSpace S
σ : Type u_4
Y : σ → Type u_5
inst✝ : (i : σ) → TopologicalSpace (Y i)
g : (i : σ) → Y i → S
a : σ → ι
t : (i : σ) → Y i → X (a i)
ht : ∀ (i : σ), Continuous (t i)
hge : ∀ (i : σ), g i = f (a i) ∘ t i
hf : ∀ (i : ι), Continuous (f i)
U : Set S
ho : IsOpen U
hU : ∃ V, IsCompact V.carrier ∧ (fun p ↦ g p.fst p.snd) '' V.carrier = U
p : (i : σ) × Y i → (i : ι) × X i := Sigma.map a t
⊢ ∃ V, IsCompact V.carrier ∧ (fun p ↦ f p.fst p.snd) '' V.carrier = 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
a✝ : k ∈ Finset.univ
hkj : k = j
⊢ (c.val j %ₘ c.val i).degree.succ ≤ (c.val k).degree.succ

Tactic:
subst hkj; gcongr; exact (degree_modByMonic_le _ hi).trans hle

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

Goal state before:
pp: case hP₄
R✝ : Type u_2
inst✝¹ : CommRing R✝
n : ℕ
R : Type u_2
inst✝ : CommRing R
c : R
i : Fin n
e : InductionObj R n
he : c = (e.val i).leadingCoeff
hc : c ≠ 0
H₁ :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ (Away c)],
    Statement R₀ (Away c) n
      { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val }
H₂ :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ (R ⧸ Ideal.span {c})],
    Statement R₀ (R ⧸ Ideal.span {c}) n { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val }
⊢ ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R], Statement R₀ R n e

Tactic:
R₀

Goal state after:
case hP₄
R✝ : Type u_2
inst✝¹ : CommRing R✝
n : ℕ
R : Type u_2
inst✝ : CommRing R
c : R
i : Fin n
e : InductionObj R n
he : c = (e.val i).leadingCoeff
hc : c ≠ 0
H₁ :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ (Away c)],
    Statement R₀ (Away c) n
      { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val }
H₂ :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ (R ⧸ Ideal.span {c})],
    Statement R₀ (R ⧸ Ideal.span {c}) n { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val }
R₀ : Type u_1
⊢ ∀ [inst : CommRing R₀] [inst_1 : Algebra R₀ R], Statement R₀ R n e
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ 4 * (W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2) =
    (W.a₁ ^ 2 + 4 * W.a₂) * (W.a₃ ^ 2 + 4 * W.a₆) - (2 * W.a₄ + W.a₁ * W.a₃) ^ 2

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ 1728 *
      (-(W.a₁ ^ 2 + 4 * W.a₂) ^ 2 *
              (W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2) -
            8 * (2 * W.a₄ + W.a₁ * W.a₃) ^ 3 -
          27 * (W.a₃ ^ 2 + 4 * W.a₆) ^ 2 +
        9 * (W.a₁ ^ 2 + 4 * W.a₂) * (2 * W.a₄ + W.a₁ * W.a₃) * (W.a₃ ^ 2 + 4 * W.a₆)) =
    ((W.a₁ ^ 2 + 4 * W.a₂) ^ 2 - 24 * (2 * W.a₄ + W.a₁ * W.a₃)) ^ 3 -
      (-(W.a₁ ^ 2 + 4 * W.a₂) ^ 3 + 36 * (W.a₁ ^ 2 + 4 * W.a₂) * (2 * W.a₄ + W.a₁ * W.a₃) -
          216 * (W.a₃ ^ 2 + 4 * W.a₆)) ^
        2

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (W.a₁ ^ 2 + 4 * W.a₂) ^ 2 * (2 * (2 * W.a₄ + W.a₁ * W.a₃)) ^ 2 - 4 * 4 * (2 * (2 * W.a₄ + W.a₁ * W.a₃)) ^ 3 -
          4 * (W.a₁ ^ 2 + 4 * W.a₂) ^ 3 * (W.a₃ ^ 2 + 4 * W.a₆) -
        27 * 4 ^ 2 * (W.a₃ ^ 2 + 4 * W.a₆) ^ 2 +
      18 * 4 * (W.a₁ ^ 2 + 4 * W.a₂) * (2 * (2 * W.a₄ + W.a₁ * W.a₃)) * (W.a₃ ^ 2 + 4 * W.a₆) =
    16 *
      (-(W.a₁ ^ 2 + 4 * W.a₂) ^ 2 *
              (W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2) -
            8 * (2 * W.a₄ + W.a₁ * W.a₃) ^ 3 -
          27 * (W.a₃ ^ 2 + 4 * W.a₆) ^ 2 +
        9 * (W.a₁ ^ 2 + 4 * W.a₂) * (2 * W.a₄ + W.a₁ * W.a₃) * (W.a₃ ^ 2 + 4 * W.a₆))

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: case u
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C C' x✝² x✝¹ x✝ : VariableChange R
⊢ ↑x✝².u * ↑x✝¹.u * ↑x✝.u = ↑x✝².u * (↑x✝¹.u * ↑x✝.u)

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: case r
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C C' x✝² x✝¹ x✝ : VariableChange R
⊢ (x✝².r * ↑x✝¹.u ^ 2 + x✝¹.r) * ↑x✝.u ^ 2 + x✝.r = x✝².r * (↑x✝¹.u * ↑x✝.u) ^ 2 + (x✝¹.r * ↑x✝.u ^ 2 + x✝.r)

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: case s
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C C' x✝² x✝¹ x✝ : VariableChange R
⊢ ↑x✝.u * (↑x✝¹.u * x✝².s + x✝¹.s) + x✝.s = ↑x✝¹.u * ↑x✝.u * x✝².s + (↑x✝.u * x✝¹.s + x✝.s)

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: case t
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C C' x✝² x✝¹ x✝ : VariableChange R
⊢ (x✝².t * ↑x✝¹.u ^ 3 + x✝².r * x✝¹.s * ↑x✝¹.u ^ 2 + x✝¹.t) * ↑x✝.u ^ 3 +
        (x✝².r * ↑x✝¹.u ^ 2 + x✝¹.r) * x✝.s * ↑x✝.u ^ 2 +
      x✝.t =
    x✝².t * (↑x✝¹.u * ↑x✝.u) ^ 3 + x✝².r * (↑x✝.u * x✝¹.s + x✝.s) * (↑x✝¹.u * ↑x✝.u) ^ 2 +
      (x✝¹.t * ↑x✝.u ^ 3 + x✝¹.r * x✝.s * ↑x✝.u ^ 2 + x✝.t)

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
W : WeierstrassCurve R
inst✝² : W.IsElliptic
inst✝¹ : CharP R 3
inst✝ : IsReduced R
⊢ W.j = 0 ↔ W.b₂ = 0

Tactic:
rw [j_eq_zero_iff_of_char_three', pow_eq_zero_iff (Nat.succ_ne_zero _)]

Goal state after: