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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
a b : S
h : IsNilpotent (a - b)
⊢ IsNilpotent ((aeval a) P - (aeval b) P)

Tactic:
by
  simp only [← eval_map_algebraMap]
  have ⟨c, hc⟩ := evalSubFactor (map (algebraMap R S) P) a b
  exact hc ▸ (Commute.all _ _).isNilpotent_mul_left h

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
⊢ ∃ s, s.card = p.spanFinrank ∧ span R ↑s = p

Tactic:
obtain ⟨s, ⟨hs₁, hs₂⟩⟩ := exists_span_set_encard_eq_spanFinrank h

Goal state after:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
s : Set M
hs₁ : s.encard = ↑p.spanFinrank
hs₂ : span R s = p
⊢ ∃ s, s.card = p.spanFinrank ∧ span R ↑s = p
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case neg
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : (∏ i, (X - C (M i i)) - M.charpoly + M.charpoly).leadingCoeff = 1
⊢ (-(M.charpoly - ∏ i, (X - C (M i i)))).degree < ↑(Fintype.card n)

Tactic:
degree_neg

Goal state after:
case neg
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : (∏ i, (X - C (M i i)) - M.charpoly + M.charpoly).leadingCoeff = 1
⊢ (M.charpoly - ∏ i, (X - C (M i i))).degree < ↑(Fintype.card n)
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
n : ℕ
⊢ ∀ (n_1 : ℕ) (c : R), c ≠ 0 → ((hasseDeriv n) ((monomial n_1) c)).natDegree = n_1 - n

Tactic:
simp only [Ne, hasseDeriv_monomial, natDegree_monomial, ite_eq_right_iff]

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
n : ℕ
⊢ ∀ (n_1 : ℕ) (c : R), ¬c = 0 → ↑(n_1.choose n) * c = 0 → 0 = n_1 - n
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case inr.inr.cons
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h✝ : Nontrivial R
hp0 : p ≠ 0
a : R
s : Multiset R
IH : ((Multiset.map (fun x ↦ X + C x) s).prod.scaleRoots r).Splits
⊢ ((Multiset.map (fun x ↦ X + C x) (a ::ₘ s)).prod.scaleRoots r).Splits

Tactic:
| cons a s IH =>

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι : Sort u_5
S : ι → Subalgebra R A
⊢ iSup S ≤ integralClosure R A ↔ ∀ (i : ι), S i ≤ integralClosure R A

Tactic:
iSup_le_iff

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsIntegralClosure A R B
inst✝² : Module R A
inst✝¹ : IsScalarTower R A B
inst✝ : IsTorsionFree R B
⊢ IsTorsionFree R A

Tactic:
refine
    Function.Injective.moduleIsTorsionFree _ (IsIntegralClosure.algebraMap_injective A R B)
      fun _ _ => ?_
  simp only [Algebra.algebraMap_eq_smul_one, IsScalarTower.smul_assoc]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f : R[X]
hf : f.Splits
x : R
hx : eval x f ≠ 0
⊢ eval x (derivative f) = eval x f * (Multiset.map (fun z ↦ 1 / (x - z)) f.roots).sum

Tactic:
by
  classical
  simp only [hf.eval_derivative, hf.eval_eq_prod_roots, ← Multiset.sum_map_mul_left, mul_assoc]
  refine congr_arg Multiset.sum (Multiset.map_congr rfl fun z hz ↦ ?_)
  rw [← Multiset.prod_map_erase hz, mul_one_div, mul_div_cancel_left₀]
  aesop (add simp sub_eq_zero)

Goal state after:
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: case refine_3
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
p_nonzero : p ≠ 0
⊢ (p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I) →
    p * X ≠ 0 → eval₂ f r (p * X) = 0 → ∃ i, (p * X).coeff i ≠ 0 ∧ (p * X).coeff i ∈ comap f I

Tactic:
ih

Goal state after:
case refine_3
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
p_nonzero : p ≠ 0
ih : p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I
⊢ p * X ≠ 0 → eval₂ f r (p * X) = 0 → ∃ i, (p * X).coeff i ≠ 0 ∧ (p * X).coeff i ∈ comap f I
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: case refine_3.refine_2
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
p_nonzero : p ≠ 0
ih : p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I
a✝ : p * X ≠ 0
hp : eval₂ f r p * r = 0
i : ℕ
hi : p.coeff i ≠ 0
mem : p.coeff i ∈ comap f I
⊢ (p * X).coeff (i + 1) ∈ comap f I

Tactic:
· simpa [hi] using mem

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

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
this : Nontrivial R
r : A → R
hr : ∀ (x : A), r x ≠ 0
int : ∀ (x : A), IsIntegral R (r x • x)
x✝ : A
h : x✝ ∈ s
⊢ IsIntegral R ((∏ x ∈ s, r x) • x✝)

Tactic:
classical rw [← Finset.prod_erase_mul _ _ h, mul_smul]

Goal state after:
R : Type u_1
A : Type u_3
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
this : Nontrivial R
r : A → R
hr : ∀ (x : A), r x ≠ 0
int : ∀ (x : A), IsIntegral R (r x • x)
x✝ : A
h : x✝ ∈ s
⊢ IsIntegral R ((∏ x ∈ s.erase x✝, r x) • r x✝ • x✝)
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
Rf : Type u_5
Sf : Type u_6
inst✝¹² : CommRing Rf
inst✝¹¹ : CommRing Sf
inst✝¹⁰ : Algebra R Rf
inst✝⁹ : Algebra S Sf
inst✝⁸ : Algebra Rf Sf
inst✝⁷ : Algebra R Sf
inst✝⁶ : IsScalarTower R S Sf
inst✝⁵ : IsScalarTower R Rf Sf
M : Submonoid R
inst✝⁴ : IsLocalization M Rf
inst✝³ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sf
inst✝² : Algebra ↥(integralClosure R S) ↥(integralClosure Rf Sf)
inst✝¹ : IsScalarTower (↥(integralClosure R S)) (↥(integralClosure Rf Sf)) Sf
inst✝ : IsScalarTower R ↥(integralClosure R S) ↥(integralClosure Rf Sf)
⊢ ∀ (z : ↥(integralClosure Rf Sf)),
    ∃ x,
      z * (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf)) ↑x.2 =
        (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf)) x.1

Tactic:
rintro ⟨s, hs⟩

Goal state after:
case refine_2
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
Rf : Type u_5
Sf : Type u_6
inst✝¹² : CommRing Rf
inst✝¹¹ : CommRing Sf
inst✝¹⁰ : Algebra R Rf
inst✝⁹ : Algebra S Sf
inst✝⁸ : Algebra Rf Sf
inst✝⁷ : Algebra R Sf
inst✝⁶ : IsScalarTower R S Sf
inst✝⁵ : IsScalarTower R Rf Sf
M : Submonoid R
inst✝⁴ : IsLocalization M Rf
inst✝³ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sf
inst✝² : Algebra ↥(integralClosure R S) ↥(integralClosure Rf Sf)
inst✝¹ : IsScalarTower (↥(integralClosure R S)) (↥(integralClosure Rf Sf)) Sf
inst✝ : IsScalarTower R ↥(integralClosure R S) ↥(integralClosure Rf Sf)
s : Sf
hs : s ∈ integralClosure Rf Sf
⊢ ∃ x,
    ⟨s, hs⟩ * (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf)) ↑x.2 =
      (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf)) x.1
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
⊢ IsAlgebraic R (a * b)

Tactic:
have ⟨ra, a0, int_a⟩ := ha.exists_integral_multiple

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
⊢ IsAlgebraic R (a * b)
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
⊢ IsAlgebraic R (a + b)

Tactic:
have ⟨ra, a0, int_a⟩ := ha.exists_integral_multiple

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
⊢ IsAlgebraic R (a + b)
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
inst✝ : FaithfulSMul S T
h : FaithfulSMul R S
this✝ : FaithfulSMul R T
this : IsDomain R
⊢ finrank R S * finrank S T = finrank R T

Tactic:
have : IsDomain S := (FaithfulSMul.algebraMap_injective S T).isDomain

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
inst✝ : FaithfulSMul S T
h : FaithfulSMul R S
this✝¹ : FaithfulSMul R T
this✝ : IsDomain R
this : IsDomain S
⊢ finrank R S * finrank S T = finrank R T
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 ≠ ⊤ → ∀ (s : S), ∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x

Tactic:
SurjectiveOnStalks,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
⊢ (∀ (P : Ideal S) (x : P.IsPrime), Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯)) ↔
    ∀ (I : Ideal S), I ≠ ⊤ → ∀ (s : S), ∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f 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
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : FaithfullyFlat R S
inst✝⁴ : Flat S (S ⊗[R] M)
N P : Type (max u v)
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
⊢ ∀ (f : N →ₗ[R] P), Function.Injective ⇑f → Function.Injective ⇑(LinearMap.lTensor M f)

Tactic:
f

Goal state after:
R : Type u
M : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : FaithfullyFlat R S
inst✝⁴ : Flat S (S ⊗[R] M)
N P : Type (max u v)
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
⊢ Function.Injective ⇑f → Function.Injective ⇑(LinearMap.lTensor M f)
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).2 = (↑b).2
⊢ a = b

Tactic:
by
  refine Subtype.ext <| Prod.ext_iff.mpr ⟨eq_of_mul_eq_add_eq_one a.1.2 ?_ ?_ ?_, eq⟩
  · rw [mul_comm, a.2.1, eq, b.2.1]
  · rw [add_comm, a.2.2]
  · rw [add_comm, eq, b.2.2]

Goal state after:
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⟩
x : R i
⊢ x ∈ p.asIdeal ↔ x ∈ q.asIdeal

Tactic:
simpa using congr_arg (Function.update (0 : ∀ i, R i) i x ∈ ·.asIdeal) eq

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
q : Ideal (Localization.AtPrime p)
hq' : map (algebraMap R (Localization.AtPrime p)) I ≤ q
hq : q.IsPrime
h₁ : (↑((IsLocalization.AtPrime.orderIsoOfPrime (Localization.AtPrime p) p) ⟨q, hq⟩)).IsPrime
h₂ : ↑((IsLocalization.AtPrime.orderIsoOfPrime (Localization.AtPrime p) p) ⟨q, hq⟩) ≤ p
⊢ map (algebraMap R (Localization.AtPrime p)) p ≤ q

Tactic:
Ideal.map_le_iff_le_comap

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
q : Ideal (Localization.AtPrime p)
hq' : I ≤ comap (algebraMap R (Localization.AtPrime p)) q
hq : q.IsPrime
h₁ : (↑((IsLocalization.AtPrime.orderIsoOfPrime (Localization.AtPrime p) p) ⟨q, hq⟩)).IsPrime
h₂ : ↑((IsLocalization.AtPrime.orderIsoOfPrime (Localization.AtPrime p) p) ⟨q, hq⟩) ≤ p
⊢ p ≤ comap (algebraMap R (Localization.AtPrime p)) q
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : R
reg : IsSMulRegular M x
p : Ideal R
hp : p ∈ (Module.annihilator R M).minimalPrimes
⊢ x ∉ p

Tactic:
intro hx
  rcases Ideal.exists_mul_mem_of_mem_minimalPrimes hp hx with ⟨y, hy, hxy⟩
  rcases not_forall.mp (Module.mem_annihilator.not.mp hy) with ⟨m, hm⟩
  exact hm (reg.right_eq_zero_of_smul ((smul_smul x y m).trans (Module.mem_annihilator.mp hxy m)))

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

Goal state before:
pp: case h
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
k : Type u := p.asIdeal.ResidueField
h : Nontrivial (p.asIdeal.ResidueField ⊗[R] S)
m : Ideal (k ⊗[R] S)
hm : m.IsMaximal
⊢ (comap (Algebra.TensorProduct.includeLeftRingHom.comp (algebraMap R k)) { asIdeal := m, isPrime := ⋯ }).asIdeal =
    p.asIdeal

Tactic:
comap_comp_apply

Goal state after:
case h
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
k : Type u := p.asIdeal.ResidueField
h : Nontrivial (p.asIdeal.ResidueField ⊗[R] S)
m : Ideal (k ⊗[R] S)
hm : m.IsMaximal
⊢ (comap (algebraMap R k) (comap Algebra.TensorProduct.includeLeftRingHom { asIdeal := m, isPrime := ⋯ })).asIdeal =
    p.asIdeal
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ ⨅ v, Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯ = ⊥

Tactic:
refine bot_unique (.trans (fun _ ↦ ?_) (MaximalSpectrum.iInf_localization_eq_bot R K).le)
  simpa only [Algebra.mem_iInf] using fun hx ⟨v, hv⟩ ↦ hx ⟨v, hv.isPrime⟩

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
s t : Opens α
⊢ Disjoint ↑s ↑t ↔ Disjoint s t

Tactic:
by
  simp [disjoint_iff, ← SetLike.coe_set_eq]

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

Goal state before:
pp: case of_equiv
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_5
inst✝ : Finite ι
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
ih : ∀ (U : α✝ → Opens α), ↑(⨅ i, U i) = ⋂ i, ↑(U i)
U : β✝ → Opens α
⊢ ↑(⨅ x, U (e x)) = ⋂ x, ↑(U (e x))

Tactic:
ih

Goal state after:
case of_equiv
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_5
inst✝ : Finite ι
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
ih : ∀ (U : α✝ → Opens α), ↑(⨅ i, U i) = ⋂ i, ↑(U i)
U : β✝ → Opens α
⊢ ⋂ i, ↑(U (e i)) = ⋂ x, ↑(U (e x))
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: case h_option
α : Type u_2
inst✝² : TopologicalSpace α
ι : Type u_5
inst✝¹ : Finite ι
α✝ : Type u_5
inst✝ : Fintype α✝
ih : ∀ (U : α✝ → Opens α), ↑(⨅ i, U i) = ⋂ i, ↑(U i)
U : Option α✝ → Opens α
⊢ ↑(U none) ∩ ↑(⨅ b, U (some b)) = ↑(U none) ∩ ⋂ i, ↑(U (some i))

Tactic:
ih

Goal state after:
case h_option
α : Type u_2
inst✝² : TopologicalSpace α
ι : Type u_5
inst✝¹ : Finite ι
α✝ : Type u_5
inst✝ : Fintype α✝
ih : ∀ (U : α✝ → Opens α), ↑(⨅ i, U i) = ⋂ i, ↑(U i)
U : Option α✝ → Opens α
⊢ ↑(U none) ∩ ⋂ i, ↑(U (some i)) = ↑(U none) ∩ ⋂ i, ↑(U (some i))
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
U V : Opens α
i : U ≤ V
⊢ IsOpen[instTopologicalSpaceSubtype] (range (Set.inclusion ⋯))

Tactic:
rw [Set.range_inclusion i]

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
U V : Opens α
i : U ≤ V
⊢ IsOpen[instTopologicalSpaceSubtype] {x | ↑x ∈ ↑U}
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
s : Set Y
⊢ f ⁻¹' coborder s ⊆ coborder (f ⁻¹' s)

Tactic:
rw [coborder, coborder, preimage_compl, preimage_sdiff, compl_subset_compl]
  apply sdiff_subset_sdiff_left
  exact hf.closure_preimage_subset s

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

Goal state before:
pp: case h.refine_2
X : Type u
inst✝ : TopologicalSpace X
ι : Type u_5
U : ι → Opens X
hU : IsBasis (range U)
W : Opens X
hW : IsCompact W.carrier
κ : Type u
a : κ → ι
heq : W = ⨆ k, U (a k)
s : Finset κ
hs : W.carrier ⊆ ⋃ i ∈ s, (U (a i)).carrier
⊢ ⨆ k, U ((a ∘ Subtype.val) k) ≤ ⨆ k, U (a k)

Tactic:
iSup_le_iff

Goal state after:
case h.refine_2
X : Type u
inst✝ : TopologicalSpace X
ι : Type u_5
U : ι → Opens X
hU : IsBasis (range U)
W : Opens X
hW : IsCompact W.carrier
κ : Type u
a : κ → ι
heq : W = ⨆ k, U (a k)
s : Finset κ
hs : W.carrier ⊆ ⋃ i ∈ s, (U (a i)).carrier
⊢ ∀ (i : ↥s), U ((a ∘ Subtype.val) i) ≤ ⨆ k, U (a k)
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⟩

Goal state after:
case refine_1
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
t : Finset (↑s × ↑s)
⊢ (t.sup fun x ↦ ↑x.1 \ ↑x.2) ∈ closure s
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ CompleteLattice.IsSupFiniteCompact (Opens α) ↔ ∀ (s : Opens α), IsCompact ↑s

Tactic:
CompleteLattice.isSupFiniteCompact_iff_all_elements_compact

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ (∀ (k : Opens α), IsCompactElement k) ↔ ∀ (s : Opens α), IsCompact ↑s
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α✝
inst✝ : TopologicalSpace β
α : Type u_3
s : Set (CofiniteTopology α)
⊢ ∀ (f : Ultrafilter (CofiniteTopology α)), s ∈ ↑f → ∃ x ∈ s, ↑f ≤ pure x ∨ ↑f ≤ Filter.cofinite

Tactic:
f

Goal state after:
α✝ : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α✝
inst✝ : TopologicalSpace β
α : Type u_3
s : Set (CofiniteTopology α)
f : Ultrafilter (CofiniteTopology α)
⊢ s ∈ ↑f → ∃ x ∈ s, ↑f ≤ pure x ∨ ↑f ≤ Filter.cofinite
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α✝
inst✝ : TopologicalSpace β
α : Type u_3
s : Set (CofiniteTopology α)
f : Ultrafilter (CofiniteTopology α)
hs : s ∈ ↑f
⊢ ∃ x ∈ s, ↑f ≤ pure x ∨ ↑f ≤ Filter.cofinite

Tactic:
rcases f.le_cofinite_or_eq_pure with (hf | ⟨a, rfl⟩)

Goal state after:
case inl
α✝ : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α✝
inst✝ : TopologicalSpace β
α : Type u_3
s : Set (CofiniteTopology α)
f : Ultrafilter (CofiniteTopology α)
hs : s ∈ ↑f
hf : ↑f ≤ Filter.cofinite
⊢ ∃ x ∈ s, ↑f ≤ pure x ∨ ↑f ≤ Filter.cofinite

case inr
α✝ : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α✝
inst✝ : TopologicalSpace β
α : Type u_3
s : Set (CofiniteTopology α)
a : CofiniteTopology α
hs : s ∈ ↑(pure a)
⊢ ∃ x ∈ s, ↑(pure a) ≤ pure x ∨ ↑(pure a) ≤ Filter.cofinite
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
s t : Clopens α
⊢ Disjoint ↑s ↑t ↔ Disjoint s t

Tactic:
by
  simp [disjoint_iff, ← SetLike.coe_set_eq]

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
p : (g : α) → g ∈ closure s → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup : ∀ (x : α) (hx : x ∈ closure s) (y : α) (hy : y ∈ closure s), p x hx → p y hy → p (x ⊔ y) ⋯
t✝ : Finset (↑s × ↑s)
x : ↑s × ↑s
t : Finset (↑s × ↑s)
x✝ : x ∉ t
ih : ∀ (hx : (t.sup fun x ↦ ↑x.1 \ ↑x.2) ∈ closure s), p (t.sup fun x ↦ ↑x.1 \ ↑x.2) hx
hxt✝ : ((insert x t).sup fun x ↦ ↑x.1 \ ↑x.2) ∈ closure s
hxt : (↑x.1 \ ↑x.2 ⊔ t.sup fun x ↦ ↑x.1 \ ↑x.2) ∈ closure s
⊢ p (↑x.1 \ ↑x.2 ⊔ t.sup fun x ↦ ↑x.1 \ ↑x.2) ⋯

Tactic:
exact sup _ _ _ ((mem_closure_iff_sup_sdiff isSublattice bot_mem top_mem).mpr ⟨_, rfl⟩)
    (sdiff _ x.1.2 _ x.2.2) (ih _)

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

Goal state before:
pp: case a
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
U : Opens X
⊢ ∀ i ∈ { carrier := {V | ↑V ⊆ ↑U}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ }, i.toOpens ≤ U

Tactic:
exact fun _ ↦ id

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case sdiff.empty
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
P : (s : Set X) → IsConstructible s → Prop
inst✝¹ : QuasiSeparatedSpace X
ι : Type u_4
inst✝ : Nonempty ι
b : ι → Set X
basis : IsTopologicalBasis (range b)
isCompact_basis : ∀ (i : ι), IsCompact (b i)
sdiff : ∀ (i : ι) (s : Set ι) (hs : s.Finite), P (b i \ ⋃ j ∈ s, b j) ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), P s hs → P t ht → P (s ∪ t) ⋯
s✝ : Set X
this : ∀ (U : Set X), IsCompact U ∧ IsOpen[inst✝³] U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
s t : Set ι
ht : t.Finite
hV : ⋃ i ∈ t, b i ∈ {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}
hU : ⋃ i ∈ ∅, b i ∈ {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}
⊢ P (⋃ i ∈ ∅, b i \ ⋃ i ∈ t, b i) ⋯

Tactic:
simpa using sdiff (Classical.arbitrary _) {Classical.arbitrary _}

Goal state after: