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

Goal state before:
pp: case mpr.refine_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x
y✝ : Localization.AtPrime P
x✝ : S × ↥P.primeCompl
y t : S
h : t ∈ P.primeCompl
yx ys : R
yc : S
hyc : yc ∉ P
hy : f ys ∉ P
ey : yc * f ys * y = yc * f yx
tx ts : R
yt : S
hyt : yt ∉ P
ht : f ts ∉ P
et : yt * f ts * t = yt * f tx
⊢ yc * yt * (t * (f yx * f ts)) = yc * yt * (f ys * f tx * y)

Tactic:
convert! congr($(ey.symm) * $(et)) using 1

Goal state after:
case e'_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x
y✝ : Localization.AtPrime P
x✝ : S × ↥P.primeCompl
y t : S
h : t ∈ P.primeCompl
yx ys : R
yc : S
hyc : yc ∉ P
hy : f ys ∉ P
ey : yc * f ys * y = yc * f yx
tx ts : R
yt : S
hyt : yt ∉ P
ht : f ts ∉ P
et : yt * f ts * t = yt * f tx
⊢ yc * yt * (t * (f yx * f ts)) = yc * f yx * (yt * f ts * t)

case e'_3
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x
y✝ : Localization.AtPrime P
x✝ : S × ↥P.primeCompl
y t : S
h : t ∈ P.primeCompl
yx ys : R
yc : S
hyc : yc ∉ P
hy : f ys ∉ P
ey : yc * f ys * y = yc * f yx
tx ts : R
yt : S
hyt : yt ∉ P
ht : f ts ∉ P
et : yt * f ts * t = yt * f tx
⊢ yc * yt * (f ys * f tx * y) = yc * f ys * y * (yt * f tx)
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
⊢ f.SurjectiveOnStalks ↔ ∀ (I : Ideal S), I.IsMaximal → ∀ (s : S), ∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x

Tactic:
by
  simp only [surjectiveOnStalks_iff_forall_maximal, surjective_localRingHom_iff]

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case tmul
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
x₁ : S
x₂ : T
y s : R
c : T
hs : c ∉ J
hc : (algebraMap R T) s ∉ J
e : c * (algebraMap R T) s * x₂ = c * (algebraMap R T) y
⊢ ∃ t r a, (algebraMap R T) r * t ∉ J ∧ 1 ⊗ₜ[R] ((algebraMap R T) r * t) * x₁ ⊗ₜ[R] x₂ = a ⊗ₜ[R] t

Tactic:
refine ⟨c, s, y • x₁, J.primeCompl.mul_mem hc hs, ?_⟩

Goal state after:
case tmul
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
x₁ : S
x₂ : T
y s : R
c : T
hs : c ∉ J
hc : (algebraMap R T) s ∉ J
e : c * (algebraMap R T) s * x₂ = c * (algebraMap R T) y
⊢ 1 ⊗ₜ[R] ((algebraMap R T) s * c) * x₁ ⊗ₜ[R] x₂ = (y • x₁) ⊗ₜ[R] c
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
S : Type u_2
inst✝⁵ : CommRing S
T : Type u_3
inst✝⁴ : CommRing T
S' : Type u_4
inst✝³ : CommRing S'
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R S'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
this✝ : Algebra S S' := f.toAlgebra
this : IsScalarTower R S S'
⊢ (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T)).toRingHom =
    ((↑(Algebra.TensorProduct.cancelBaseChange R S S S' T)).comp Algebra.TensorProduct.includeRight).toRingHom

Tactic:
congr

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
S : Type u_2
inst✝⁵ : CommRing S
T : Type u_3
inst✝⁴ : CommRing T
S' : Type u_4
inst✝³ : CommRing S'
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R S'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
this✝ : Algebra S S' := f.toAlgebra
this : IsScalarTower R S S'
⊢ Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T) =
    (↑(Algebra.TensorProduct.cancelBaseChange R S S S' T)).comp Algebra.TensorProduct.includeRight
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
T : Type u_3
inst✝⁶ : CommRing T
S' : Type u_4
T' : Type u_5
inst✝⁵ : CommRing S'
inst✝⁴ : CommRing T'
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra R S'
inst✝ : Algebra R T'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
g : T →ₐ[R] T'
Hg : g.SurjectiveOnStalks
⊢ ↑(Algebra.TensorProduct.map f g) =
    ↑((Algebra.TensorProduct.map f (AlgHom.id R T')).comp
        ((↑(Algebra.TensorProduct.comm R T' S)).comp
          ((Algebra.TensorProduct.map g (AlgHom.id R S)).comp ↑(Algebra.TensorProduct.comm R S T))))

Tactic:
congr

Goal state after:
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
T : Type u_3
inst✝⁶ : CommRing T
S' : Type u_4
T' : Type u_5
inst✝⁵ : CommRing S'
inst✝⁴ : CommRing T'
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra R S'
inst✝ : Algebra R T'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
g : T →ₐ[R] T'
Hg : g.SurjectiveOnStalks
⊢ Algebra.TensorProduct.map f g =
    (Algebra.TensorProduct.map f (AlgHom.id R T')).comp
      ((↑(Algebra.TensorProduct.comm R T' S)).comp
        ((Algebra.TensorProduct.map g (AlgHom.id R S)).comp ↑(Algebra.TensorProduct.comm R S T)))
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ Function.Injective ⇑(algebraMap (R ⧸ I) I.ResidueField)

Tactic:
by
  rw [RingHom.injective_iff_ker_eq_bot]
  refine (Ideal.ker_quotient_lift _ _).trans ?_
  change map (Quotient.mk I) (RingHom.ker (algebraMap R I.ResidueField)) = ⊥
  rw [Ideal.ker_algebraMap_residueField, map_quotient_self]

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : FaithfullyFlat A B
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module A M
x : B
⊢ ∀ (y : M),
    (lTensor B ((TensorProduct.mk A B M) 1)) (x ⊗ₜ[A] y) =
      (↑(leftComm A B B M).symm ∘ₗ (TensorProduct.mk A B (B ⊗[A] M)) 1) (x ⊗ₜ[A] y)

Tactic:
y

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : FaithfullyFlat A B
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module A M
x : B
y : M
⊢ (lTensor B ((TensorProduct.mk A B M) 1)) (x ⊗ₜ[A] y) =
    (↑(leftComm A B B M).symm ∘ₗ (TensorProduct.mk A B (B ⊗[A] M)) 1) (x ⊗ₜ[A] y)
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case inl
ι : Type u_3
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
x✝¹ x✝ : (i : ι) × PrimeSpectrum (R i)
i : ι
p q : PrimeSpectrum (R i)
eq : sigmaToPi R ⟨i, p⟩ = sigmaToPi R ⟨i, q⟩
⊢ ⟨i, p⟩ = ⟨i, q⟩

Tactic:
congr

Goal state after:
case inl
ι : Type u_3
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
x✝¹ x✝ : (i : ι) × PrimeSpectrum (R i)
i : ι
p q : PrimeSpectrum (R i)
eq : sigmaToPi R ⟨i, p⟩ = sigmaToPi R ⟨i, q⟩
⊢ p = q
Module: Mathlib.RingTheory.Localization.AsSubring

Goal state before:
pp: case e'_2
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
x : K
x✝² x✝¹ : A
x✝ : x✝¹ ∈ S
⊢ (algebraMap A K) x✝² * ((algebraMap A K) x✝¹)⁻¹ = IsLocalization.mk' K x✝² ⟨x✝¹, ⋯⟩

Tactic:
congr

Goal state after:
case e'_2.e_a
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
x : K
x✝² x✝¹ : A
x✝ : x✝¹ ∈ S
⊢ ((algebraMap A K) x✝¹)⁻¹ =
    ↑((IsUnit.liftRight ((IsLocalization.toLocalizationMap A⁰ K).toMonoidHom.domRestrict A⁰) ⋯) ⟨x✝¹, ⋯⟩)⁻¹
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mp.refine_2
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
hp : p ∈ (Ideal.map (algebraMap R A) J).minimalPrimes
this : p.IsPrime
I : Ideal R
hI : I.IsPrime ∧ J ≤ I
e : I ≤ Ideal.under R p
hI' : Disjoint ↑S ↑I
⊢ Ideal.comap (algebraMap R A) (Ideal.map (algebraMap R A) I) = I

Tactic:
exact IsLocalization.under_map_of_isPrime_disjoint S A hI.1 hI'

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
x✝² x✝¹ : Opens α
carrier✝¹ : Set α
is_open'✝¹ : IsOpen[inst✝²] carrier✝¹
carrier✝ : Set α
is_open'✝ : IsOpen[inst✝²] carrier✝
x✝ : { carrier := carrier✝¹, is_open' := is_open'✝¹ }.carrier = { carrier := carrier✝, is_open' := is_open'✝ }.carrier
⊢ { carrier := carrier✝¹, is_open' := is_open'✝¹ } = { carrier := carrier✝, is_open' := is_open'✝ }

Tactic:
congr

Goal state after:
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (closure[inst✝] s \ s)ᶜ ∩ closure[inst✝] s = s

Tactic:
← sdiff_eq_compl_inter,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ closure[inst✝] s \ (closure[inst✝] s \ s) = s
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ sᶜ ∩ frontier s = closure[inst✝] s \ s

Tactic:
← sdiff_eq_compl_inter,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ frontier s \ s = closure[inst✝] s \ s
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : GeneralizingMap f
s : Set β
x : ↑(f ⁻¹' s)
⊢ ∀ ⦃b : ↑s⦄,
    (fun x1 x2 ↦ x1 ⤳ x2) b (s.restrictPreimage f x) → ∃ a', (fun x1 x2 ↦ x1 ⤳ x2) a' x ∧ s.restrictPreimage f a' = b

Tactic:
y

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : GeneralizingMap f
s : Set β
x : ↑(f ⁻¹' s)
y : ↑s
⊢ (fun x1 x2 ↦ x1 ⤳ x2) y (s.restrictPreimage f x) → ∃ a', (fun x1 x2 ↦ x1 ⤳ x2) a' x ∧ s.restrictPreimage f a' = y
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BooleanAlgebra γ
L M✝ : BooleanSubalgebra α
f : BoundedLatticeHom α β
s t : Set α
a b : α
M : BooleanSubalgebra α
carrier✝ : Set α
supClosed'✝ : SupClosed carrier✝
infClosed'✝ : InfClosed carrier✝
compl_mem'✝ :
  ∀ {a : α},
    a ∈ { carrier := carrier✝, supClosed' := supClosed'✝, infClosed' := infClosed'✝ }.carrier →
      aᶜ ∈ { carrier := carrier✝, supClosed' := supClosed'✝, infClosed' := infClosed'✝ }.carrier
bot_mem'✝ : ⊥ ∈ { carrier := carrier✝, supClosed' := supClosed'✝, infClosed' := infClosed'✝ }.carrier
h :
  (fun L ↦ L.carrier)
      { carrier := carrier✝, supClosed' := supClosed'✝, infClosed' := infClosed'✝, compl_mem' := compl_mem'✝,
        bot_mem' := bot_mem'✝ } =
    (fun L ↦ L.carrier) M
⊢ { carrier := carrier✝, supClosed' := supClosed'✝, infClosed' := infClosed'✝, compl_mem' := compl_mem'✝,
      bot_mem' := bot_mem'✝ } =
    M

Tactic:
congr

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst✝¹, inst✝] f
H : ∀ (x : α), 𝓝 x = Filter.comap f (𝓝 (f x))
i : ι
x : ↑(f ⁻¹' (U i).carrier)
⊢ 𝓝 x = Filter.comap Subtype.val (Filter.comap f (𝓝 ((f ∘ Subtype.val) x)))

Tactic:
Function.comp_apply,

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst✝¹, inst✝] f
H : ∀ (x : α), 𝓝 x = Filter.comap f (𝓝 (f x))
i : ι
x : ↑(f ⁻¹' (U i).carrier)
⊢ 𝓝 x = Filter.comap Subtype.val (Filter.comap f (𝓝 (f ↑x)))
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: case mk.mk
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
carrier✝¹ : Set α
isClosed'✝¹ : IsClosed[inst✝¹] carrier✝¹
carrier✝ : Set α
isClosed'✝ : IsClosed[inst✝¹] carrier✝
h :
  { carrier := carrier✝¹, isClosed' := isClosed'✝¹ }.carrier = { carrier := carrier✝, isClosed' := isClosed'✝ }.carrier
⊢ { carrier := carrier✝¹, isClosed' := isClosed'✝¹ } = { carrier := carrier✝, isClosed' := isClosed'✝ }

Tactic:
congr

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

Goal state before:
pp: case mk.mk
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
carrier✝¹ : Set α
isClopen'✝¹ : IsClopen carrier✝¹
carrier✝ : Set α
isClopen'✝ : IsClopen carrier✝
h :
  (fun s ↦ s.carrier) { carrier := carrier✝¹, isClopen' := isClopen'✝¹ } =
    (fun s ↦ s.carrier) { carrier := carrier✝, isClopen' := isClopen'✝ }
⊢ { carrier := carrier✝¹, isClopen' := isClopen'✝¹ } = { carrier := carrier✝, isClopen' := isClopen'✝ }

Tactic:
congr

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

Goal state before:
pp: case mk.mk
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
carrier✝¹ : Set α
isIrreducible'✝¹ : IsIrreducible carrier✝¹
isClosed'✝¹ : IsClosed[inst✝¹] carrier✝¹
carrier✝ : Set α
isIrreducible'✝ : IsIrreducible carrier✝
isClosed'✝ : IsClosed[inst✝¹] carrier✝
h :
  { carrier := carrier✝¹, isIrreducible' := isIrreducible'✝¹, isClosed' := isClosed'✝¹ }.carrier =
    { carrier := carrier✝, isIrreducible' := isIrreducible'✝, isClosed' := isClosed'✝ }.carrier
⊢ { carrier := carrier✝¹, isIrreducible' := isIrreducible'✝¹, isClosed' := isClosed'✝¹ } =
    { carrier := carrier✝, isIrreducible' := isIrreducible'✝, isClosed' := isClosed'✝ }

Tactic:
congr

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
⊢ ∃ S, (∀ (k : ↥S), IsIrreducible ↑↑k) ∧ s = S.sup id

Tactic:
by
  simpa [Set.exists_finite_iff_finset, Finset.sup_id_eq_sSup]
    using NoetherianSpace.exists_finite_set_closeds_irreducible s

Goal state after:
Module: Mathlib.Topology.Spectral.Hom

Goal state before:
pp: case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
toFun✝¹ : α → β
spectral'✝¹ : IsSpectralMap toFun✝¹
toFun✝ : α → β
spectral'✝ : IsSpectralMap toFun✝
h : { toFun := toFun✝¹, spectral' := spectral'✝¹ }.toFun = { toFun := toFun✝, spectral' := spectral'✝ }.toFun
⊢ { toFun := toFun✝¹, spectral' := spectral'✝¹ } = { toFun := toFun✝, spectral' := spectral'✝ }

Tactic:
congr

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
b : ι → Set α
basis : IsTopologicalBasis (range b)
isCompact_inter : ∀ (i j : ι), IsCompact (b i ∩ b j)
U V : Set α
hUopen : IsOpen[inst✝] U
hUcomp : IsCompact U
hVopen : IsOpen[inst✝] V
hVcomp : IsCompact V
⊢ IsCompact (U ∩ V)

Tactic:
have aux := isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis b basis fun i ↦ by
      simpa using isCompact_inter i i
    obtain ⟨s, hs, rfl⟩ := (aux _).1 ⟨hUcomp, hUopen⟩
    obtain ⟨t, ht, rfl⟩ := (aux _).1 ⟨hVcomp, hVopen⟩
    rw [iUnion₂_inter_iUnion₂]
    exact hs.isCompact_biUnion fun i hi ↦ ht.isCompact_biUnion fun j hj ↦ isCompact_inter ..

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: case mk.mk
P : Type u_1
inst✝ : LE P
toLowerSet✝¹ : LowerSet P
nonempty'✝¹ : toLowerSet✝¹.carrier.Nonempty
directed'✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) toLowerSet✝¹.carrier
toLowerSet✝ : LowerSet P
nonempty'✝ : toLowerSet✝.carrier.Nonempty
directed'✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) toLowerSet✝.carrier
x✝ :
  { toLowerSet := toLowerSet✝¹, nonempty' := nonempty'✝¹, directed' := directed'✝¹ }.toLowerSet =
    { toLowerSet := toLowerSet✝, nonempty' := nonempty'✝, directed' := directed'✝ }.toLowerSet
⊢ { toLowerSet := toLowerSet✝¹, nonempty' := nonempty'✝¹, directed' := directed'✝¹ } =
    { toLowerSet := toLowerSet✝, nonempty' := nonempty'✝, directed' := directed'✝ }

Tactic:
congr

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

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
carrier✝¹ : Set α
isCompact'✝¹ : IsCompact carrier✝¹
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
h :
  { carrier := carrier✝¹, isCompact' := isCompact'✝¹ }.carrier =
    { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier
⊢ { carrier := carrier✝¹, isCompact' := isCompact'✝¹ } = { carrier := carrier✝, isCompact' := isCompact'✝ }

Tactic:
congr

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_4
s✝ : Finset ι
f : ι → Compacts α
a : ι
s : Finset ι
x✝ : a ∉ s
h : ↑(s.sup f) = s.sup fun i ↦ ↑(f i)
⊢ ↑(f a) ∪ ↑(s.sup f) = ↑(f a) ∪ s.sup fun i ↦ ↑(f i)

Tactic:
congr

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
carrier✝¹ : Set α
isCompact'✝¹ : IsCompact carrier✝¹
nonempty'✝¹ : { carrier := carrier✝¹, isCompact' := isCompact'✝¹ }.carrier.Nonempty
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
nonempty'✝ : { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier.Nonempty
h :
  (fun s ↦ s.carrier) { carrier := carrier✝¹, isCompact' := isCompact'✝¹, nonempty' := nonempty'✝¹ } =
    (fun s ↦ s.carrier) { carrier := carrier✝, isCompact' := isCompact'✝, nonempty' := nonempty'✝ }
⊢ { carrier := carrier✝¹, isCompact' := isCompact'✝¹, nonempty' := nonempty'✝¹ } =
    { carrier := carrier✝, isCompact' := isCompact'✝, nonempty' := nonempty'✝ }

Tactic:
congr

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case cons
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : (∀ i ∈ s, IsRetrocompact (t i)) → IsRetrocompact (s.inf t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)
⊢ IsRetrocompact ((Finset.cons i s ih).inf t)

Tactic:
Finset.inf_cons

Goal state after:
case cons
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : (∀ i ∈ s, IsRetrocompact (t i)) → IsRetrocompact (s.inf t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)
⊢ IsRetrocompact (t i ⊓ s.inf t)
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case refine_2
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsSpectralMap Subtype.val
t : Set X
htcomp : IsCompact t
htopen : IsOpen[inst✝] t
⊢ IsCompact (s ∩ t)

Tactic:
simpa using (hs.isCompact_preimage_of_isOpen htopen htcomp).image continuous_subtype_val

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
carrier✝¹ : Set α
isCompact'✝¹ : IsCompact carrier✝¹
interior_nonempty'✝¹ : (interior { carrier := carrier✝¹, isCompact' := isCompact'✝¹ }.carrier).Nonempty
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
interior_nonempty'✝ : (interior { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier).Nonempty
h :
  (fun s ↦ s.carrier) { carrier := carrier✝¹, isCompact' := isCompact'✝¹, interior_nonempty' := interior_nonempty'✝¹ } =
    (fun s ↦ s.carrier) { carrier := carrier✝, isCompact' := isCompact'✝, interior_nonempty' := interior_nonempty'✝ }
⊢ { carrier := carrier✝¹, isCompact' := isCompact'✝¹, interior_nonempty' := interior_nonempty'✝¹ } =
    { carrier := carrier✝, isCompact' := isCompact'✝, interior_nonempty' := interior_nonempty'✝ }

Tactic:
congr

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
carrier✝¹ : Set α
isCompact'✝¹ : IsCompact carrier✝¹
isOpen'✝¹ : IsOpen { carrier := carrier✝¹, isCompact' := isCompact'✝¹ }.carrier
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
isOpen'✝ : IsOpen { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier
h :
  (fun s ↦ s.carrier) { carrier := carrier✝¹, isCompact' := isCompact'✝¹, isOpen' := isOpen'✝¹ } =
    (fun s ↦ s.carrier) { carrier := carrier✝, isCompact' := isCompact'✝, isOpen' := isOpen'✝ }
⊢ { carrier := carrier✝¹, isCompact' := isCompact'✝¹, isOpen' := isOpen'✝¹ } =
    { carrier := carrier✝, isCompact' := isCompact'✝, isOpen' := isOpen'✝ }

Tactic:
congr

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : QuasiSober α
inst✝ : T0Space α
⊢ ∀ {a b : TopologicalSpace.IrreducibleCloseds α},
    { toFun := fun s ↦ ⋯.genericPoint,
            invFun := fun x ↦ { carrier := closure {x}, isIrreducible' := ⋯, isClosed' := ⋯ }, left_inv := ⋯,
            right_inv := ⋯ }
          a ≤
        { toFun := fun s ↦ ⋯.genericPoint,
            invFun := fun x ↦ { carrier := closure {x}, isIrreducible' := ⋯, isClosed' := ⋯ }, left_inv := ⋯,
            right_inv := ⋯ }
          b ↔
      a ≤ b

Tactic:
by
    rintro ⟨s, hs, hs'⟩ ⟨t, ht, ht'⟩
    refine specializes_iff_closure_subset.trans ?_
    simp
    rfl

Goal state after:
Module: Mathlib.Topology.KrullDimension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : QuasiSober Y
inst✝² : T0Space Y
inst✝¹ : QuasiSober X
inst✝ : T0Space X
x : X
f : X → Y
hf : IsOpenEmbedding f
⊢ coheight (irreducibleSetEquivPoints.symm (f x)) = coheight (map f ⋯ (irreducibleSetEquivPoints.symm x))

Tactic:
congr

Goal state after:
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : QuasiSober Y
inst✝² : T0Space Y
inst✝¹ : QuasiSober X
inst✝ : T0Space X
x : X
f : X → Y
hf : IsOpenEmbedding f
⊢ irreducibleSetEquivPoints.symm (f x) = map f ⋯ (irreducibleSetEquivPoints.symm x)
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case union
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s✝ : Set Y
hfcont : Continuous[inst✝¹, inst✝] f
hf : ∀ (s : Set Y), IsOpen[inst✝] s → IsRetrocompact s → IsRetrocompact (f ⁻¹' s)
s : Set Y
hs : IsConstructible s
t : Set Y
ht : IsConstructible t
hs' : IsConstructible (f ⁻¹' s)
ht' : IsConstructible (f ⁻¹' t)
⊢ IsConstructible (f ⁻¹' (s ∪ t))

Tactic:
rw [preimage_union]; exact hs'.union ht'

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case cons
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : (∀ i ∈ s, IsLocallyConstructible (t i)) → IsLocallyConstructible (s.inf t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsLocallyConstructible (t i_1)
⊢ IsLocallyConstructible ((Finset.cons i s ih).inf t)

Tactic:
Finset.inf_cons

Goal state after:
case cons
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : (∀ i ∈ s, IsLocallyConstructible (t i)) → IsLocallyConstructible (s.inf t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsLocallyConstructible (t i_1)
⊢ IsLocallyConstructible (t i ⊓ s.inf t)