mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ih : ∀ {f g : R[X]}, f ≠ 0 → g ≠ 0 → ∀ (p : R[X]), f * g = p → p.Splits → p.natDegree = n → f.Splits ∧ g.Splits
f g : R[X]
hf₀ : f ≠ 0
hg₀ : g ≠ 0
p : R[X]
hp : f * g = p
h : p.Splits
hn : p.natDegree = n + 1
⊢ n + 1 ≠ Zero.zero

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case inr.refine_3
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Rₘ : Type u_3
inst✝⁴ : CommRing Rₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : p.Monic
hp₂ : eval₂ (algebraMap Rₘ S) x p = 0
p' : R[X]
hp'₁ : Polynomial.map (algebraMap R Rₘ) p' = p.scaleRoots ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff))
hp'₂ : p'.Monic
⊢ eval₂ (algebraMap R S) (commonDenom M p.support p.coeff • x) p' = 0

Tactic:
IsScalarTower.algebraMap_eq R Rₘ S,

Goal state after:
case inr.refine_3
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Rₘ : Type u_3
inst✝⁴ : CommRing Rₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : p.Monic
hp₂ : eval₂ (algebraMap Rₘ S) x p = 0
p' : R[X]
hp'₁ : Polynomial.map (algebraMap R Rₘ) p' = p.scaleRoots ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff))
hp'₂ : p'.Monic
⊢ eval₂ ((algebraMap Rₘ S).comp (algebraMap R Rₘ)) (commonDenom M p.support p.coeff • x) p' = 0
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R S
inst✝³ : Algebra S Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R S Sₘ
M : Submonoid R
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
x : S
hx : IsIntegral R ((algebraMap S Sₘ) x)
⊢ ∃ m ∈ M, IsIntegral R (m • x)

Tactic:
obtain ⟨p, hpm, hp⟩ := hx

Goal state after:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R S
inst✝³ : Algebra S Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R S Sₘ
M : Submonoid R
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
x : S
p : R[X]
hpm : p.Monic
hp : eval₂ (algebraMap R Sₘ) ((algebraMap S Sₘ) x) p = 0
⊢ ∃ m ∈ M, IsIntegral R (m • x)
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R S
inst✝³ : Algebra S Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst✝ : Away r Sₘ
x : S
hx : IsIntegral R ((algebraMap S Sₘ) x)
a✝ : Nontrivial S
⊢ ∃ n, IsIntegral R (r ^ n * x)

Tactic:
obtain ⟨p, hpm, hp⟩ := hx

Goal state after:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R S
inst✝³ : Algebra S Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst✝ : Away r Sₘ
x : S
a✝ : Nontrivial S
p : R[X]
hpm : p.Monic
hp : eval₂ (algebraMap R Sₘ) ((algebraMap S Sₘ) x) p = 0
⊢ ∃ n, IsIntegral R (r ^ n * x)
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
f : R →+* S
I J : Ideal S
inst✝³ : Algebra R S
inst✝² : Algebra.IsIntegral R S
inst✝¹ : FaithfulSMul R S
P : Ideal R
inst✝ : P.IsPrime
⊢ comap (algebraMap R S) ⊥ ≤ P

Tactic:
simp [← RingHom.ker_eq_comap_bot]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
e : H ⊗[R] M ≃ₗ[R]
  ↥l23.ker ⊗[R] M ⧸ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id).range :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
⊢ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) 0 = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R S
inst✝³ : Algebra S Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R S Sₘ
x : S
inst✝ : Away x Sₘ
hx : IsIntegral R ((algebraMap S Sₘ) x)
⊢ IsIntegral R x

Tactic:
obtain ⟨p, hpm, hp⟩ := hx

Goal state after:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R S
inst✝³ : Algebra S Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R S Sₘ
x : S
inst✝ : Away x Sₘ
p : R[X]
hpm : p.Monic
hp : eval₂ (algebraMap R Sₘ) ((algebraMap S Sₘ) x) p = 0
⊢ IsIntegral R x
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
e : H ⊗[R] M ≃ₗ[R]
  ↥l23.ker ⊗[R] M ⧸ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id).range :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
x y : ↥(Submodule.inclusion complex).range ⊗[R] M
⊢ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) (x + y) =
    (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) x +
      (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) y

Tactic:
by simp

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

Goal state before:
pp: case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + R ∙ z
x : R
hx : x ∉ M
y : R
hy : y ∉ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + R ∙ x
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + R ∙ y
⊢ (M + R ∙ x) * (M + R ∙ y) ≤ M

Tactic:
add_mul

Goal state after:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + R ∙ z
x : R
hx : x ∉ M
y : R
hy : y ∉ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + R ∙ x
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + R ∙ y
⊢ M * (M + R ∙ y) + (R ∙ x) * (M + R ∙ y) ≤ M
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FaithfullyFlat R S
inst✝ : FaithfullyFlat S M
N : Type (max u_1 u_3)
x✝³ : AddCommGroup N
x✝² : Module R N
N' : Type (max u_1 u_3)
x✝¹ : AddCommGroup N'
x✝ : Module R N'
f : N →ₗ[R] N'
eq : f = 0
⊢ lTensor M 0 = 0

Tactic:
by simp

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

Goal state before:
pp: case h.refine_1
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt : ∀ J > M, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
lt_add : ∀ z ∉ M, M < M + A ∙ z
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + A ∙ x
h_Wx_ne✝ : (Multiset.map asIdeal Wx).prod ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + A ∙ y
h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥
⊢ (M + A ∙ x) * (M + A ∙ y) ≤ M

Tactic:
add_mul

Goal state after:
case h.refine_1
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt : ∀ J > M, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
lt_add : ∀ z ∉ M, M < M + A ∙ z
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + A ∙ x
h_Wx_ne✝ : (Multiset.map asIdeal Wx).prod ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + A ∙ y
h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥
⊢ M * (M + A ∙ y) + (A ∙ x) * (M + A ∙ y) ≤ M
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✝³ : IsLocalRing A
inst✝² : IsLocalRing B
inst✝¹ : Flat A B
inst✝ : IsLocalHom (algebraMap A B)
m : Ideal A
hm : m.IsMaximal
⊢ Submodule.restrictScalars A (Ideal.map (algebraMap A B) m) ≠ ⊤

Tactic:
IsLocalRing.eq_maximalIdeal hm

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalRing A
inst✝² : IsLocalRing B
inst✝¹ : Flat A B
inst✝ : IsLocalHom (algebraMap A B)
m : Ideal A
hm : m.IsMaximal
⊢ Submodule.restrictScalars A (Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A)) ≠ ⊤
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✝³ : IsLocalRing A
inst✝² : IsLocalRing B
inst✝¹ : Flat A B
inst✝ : IsLocalHom (algebraMap A B)
m : Ideal A
hm : m.IsMaximal
eqt : Submodule.restrictScalars A (Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A)) = ⊤
⊢ False

Tactic:
have : Submodule.restrictScalars A (Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A)) ≤
      Submodule.restrictScalars A (IsLocalRing.maximalIdeal B) :=
    ((IsLocalRing.local_hom_TFAE (algebraMap A B)).out 0 2).mp ‹_›

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalRing A
inst✝² : IsLocalRing B
inst✝¹ : Flat A B
inst✝ : IsLocalHom (algebraMap A B)
m : Ideal A
hm : m.IsMaximal
eqt : Submodule.restrictScalars A (Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A)) = ⊤
this :
  Submodule.restrictScalars A (Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A)) ≤
    Submodule.restrictScalars A (IsLocalRing.maximalIdeal B)
⊢ False
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal R
inst✝¹ : I.IsPrime
inst✝ : IsDomain R
⊢ ∀ (x : R), (algebraMap R ⊥.ResidueField) x = (algebraMap (R ⧸ ⊥) ⊥.ResidueField) ((RingEquiv.quotientBot R).symm x)

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Localization.AsSubring

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
a : A
⊢ (↑↑(IsLocalization.lift ⋯)).toFun ((algebraMap A B) a) = (algebraMap A K) a

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
hp : p ∈ I.minimalPrimes
x : R
hx✝ : x ∈ p
y : R
hy : y ∉ I.radical
n : ℕ
hx : (x * y) ^ n ∈ I
H : ∃ m, x ^ m * y ^ n ∈ I
this : Nat.find H ≠ 0
⊢ x * x ^ (Nat.find H - 1) * y ^ n ∈ I

Tactic:
← pow_succ',

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
hp : p ∈ I.minimalPrimes
x : R
hx✝ : x ∈ p
y : R
hy : y ∉ I.radical
n : ℕ
hx : (x * y) ^ n ∈ I
H : ∃ m, x ^ m * y ^ n ∈ I
this : Nat.find H ≠ 0
⊢ x ^ (Nat.find H - 1 + 1) * y ^ n ∈ I
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: 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 A
⊢ Ideal.comap (algebraMap R A) '' J.minimalPrimes ⊆ Set.range (Ideal.comap (algebraMap R A))

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case refine_2
R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst✝ : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this✝ : IsLocalRing A
J : Ideal A
hJ : J ∈ Ideal.under R ⁻¹' I.minimalPrimes
this : Disjoint ↑q.primeCompl ↑(Ideal.under R J)
⊢ Ideal.under R J ≤ q

Tactic:
exact Set.disjoint_compl_left_iff_subset.mp this

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: ι : Type u_5
R : ι → Type u_4
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : ∀ (i : ι), Nontrivial (R i)
inst✝ : Infinite ι
surj : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
J : Ideal ((i : ι) → R i)
max : J.IsMaximal
notMem : { asIdeal := J, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)
r : (i : ι) → R i
hr : (toPiLocalization ((i : ι) → R i)) r = Function.update 0 { asIdeal := J, isMaximal := max } 1
i : ι
I : MaximalSpectrum (R i)
⊢ (toPiLocalization (R i)) (r i) I = (toPiLocalization (R i)) (0 i) I

Tactic:
replace hr := congr_fun hr ⟨_, I.2.comap_piEvalRingHom⟩
    dsimp only [toPiLocalization_apply_apply, Subtype.coe_mk] at hr
    simp_rw [toPiLocalization_apply_apply,
      ← Localization.AtPrime.mapPiEvalRingHom_algebraMap_apply, hr]
    rw [Function.update_of_ne]; · simp_rw [Pi.zero_apply, map_zero]
    exact fun h ↦ notMem ⟨⟨i, I.1, I.2.isPrime⟩, PrimeSpectrum.ext congr($h.1)⟩

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✝ : Set (Opens α)
⊢ ↑(sSup x✝) = sSup ((fun x ↦ ↑x) '' x✝)

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyClosed s
ht : IsLocallyClosed t
⊢ IsLocallyClosed (s ∩ t)

Tactic:
obtain ⟨U₁, Z₁, hU₁, hZ₁, rfl⟩ := hs
  obtain ⟨U₂, Z₂, hU₂, hZ₂, rfl⟩ := ht
  refine ⟨_, _, hU₁.inter hU₂, hZ₁.inter hZ₂, inter_inter_inter_comm U₁ Z₁ U₂ Z₂⟩

Goal state after:
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 x✝ : α
⊢ x✝ ∈ {⊥, ⊤} → ∀ ⦃b : α⦄, b ∈ {⊥, ⊤} → x✝ ⊔ b ∈ {⊥, ⊤}

Tactic:
by simp

Goal state after:
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 x✝ : α
⊢ x✝ ∈ {⊥, ⊤} → ∀ ⦃b : α⦄, b ∈ {⊥, ⊤} → x✝ ⊓ b ∈ {⊥, ⊤}

Tactic:
by simp

Goal state after:
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 : α
⊢ ∀ {a : α}, a ∈ {⊥, ⊤} → aᶜ ∈ {⊥, ⊤}

Tactic:
by simp

Goal state after:
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 : α
⊢ ⊥ ∈ {⊥, ⊤}

Tactic:
by simp

Goal state after:
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 : α
f : BoundedLatticeHom α β
L : BooleanSubalgebra β
⊢ ⊥ ∈ ⇑f ⁻¹' ↑L

Tactic:
by simp

Goal state after:
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 : α
f : BoundedLatticeHom α β
L : BooleanSubalgebra α
⊢ ⊥ ∈ ↑L ∧ f ⊥ = ⊥

Tactic:
by simp

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
hU : IsCompact U.carrier
Us' : Set (Opens α)
hsub : Us' ⊆ B
hsup : U = sSup Us'
t : Finset ↑Us'
ht : U.carrier ⊆ ⋃ i ∈ t, ↑↑i
⊢ ↑(Finset.image Subtype.val t) ⊆ Us'

Tactic:
by simp

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
hU : IsCompact U.carrier
Us' : Set (Opens α)
hsub : Us' ⊆ B
hsup : U = sSup Us'
t : Finset ↑Us'
ht : U.carrier ⊆ ⋃ i ∈ t, ↑↑i
⊢ ⋃ i ∈ t, ↑↑i ⊆ ↑(sSup ↑(Finset.image Subtype.val t))

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a x : α
h : x ∈ s
⊢ x = {(⟨x, h⟩, ⟨⊥, bot_mem⟩)}.sup fun x ↦ ↑x.1 \ ↑x.2

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
⊢ ⊥ = ∅.sup fun x ↦ ↑x.1 \ ↑x.2

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
⊢ (∃ t, a = t.sup fun x ↦ ↑x.1 \ ↑x.2) → a ∈ closure s

Tactic:
rintro ⟨t, rfl⟩
    exact t.sup_mem _ (subset_closure bot_mem) (fun _ h _ ↦ sup_mem h) _
      fun x hx ↦ sdiff_mem (subset_closure x.1.2) (subset_closure x.2.2)

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
t : Finset (↑s × ↑s)
⊢ (∅.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = {(⟨⊤, top_mem⟩, ⟨⊥, bot_mem⟩)}.sup fun x ↦ ↑x.1 \ ↑x.2

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
t✝ : Finset (↑s × ↑s)
x✝² : ↑s × ↑s
t : Finset (↑s × ↑s)
x✝¹ : ∃ t_1, (t.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = t_1.sup fun x ↦ ↑x.1 \ ↑x.2
x y : ↑s
x✝ : (x, y) ∉ t
tc : Finset (↑s × ↑s)
eq : (t.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = tc.sup fun x ↦ ↑x.1 \ ↑x.2
⊢ ((↑x \ ↑y)ᶜ ⊓ ∅.sup fun x ↦ ↑x.1 \ ↑x.2) = ∅.sup fun x ↦ ↑x.1 \ ↑x.2

Tactic:
by simp

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

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

Tactic:
cases t

Goal state after:
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'✝ }
Module: Mathlib.Topology.Sets.Closeds

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

Tactic:
cases t

Goal state after:
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'✝ }
Module: Mathlib.Topology.Sets.Closeds

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

Tactic:
cases t

Goal state after:
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'✝ }
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
ht : IsQuasiSeparated t
h : s ⊆ t
⊢ IsQuasiSeparated s

Tactic:
by
  intro U V hU hU' hU'' hV hV' hV''
  exact ht U V (hU.trans h) hU' hU'' (hV.trans h) hV' hV''

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
U : Opens X
⊢ ⊥ ∈ { carrier := {V | ↑V ⊆ ↑U}, lower' := ⋯ }.carrier

Tactic:
by simp

Goal state after: