mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ Mᵀ.charmatrix = M.charmatrixᵀ

Tactic:
simp [charmatrix, transpose_map]

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
⊢ toENat p.spanRank = ⨅ s, ↑(↑s).card

Tactic:
rw [spanRank_toENat_eq_iInf_encard]

Goal state after:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ ⨅ s, ⨅ (_ : span R s = p), s.encard = ⨅ s, ↑(↑s).card
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
r : R
hp : p ∈ lifts f
⊢ C (f r) * p ∈ lifts f

Tactic:
simp only [lifts, RingHom.mem_rangeS] at hp ⊢
  obtain ⟨p₁, rfl⟩ := hp
  use C r * p₁
  simp only [coe_mapRingHom, map_C, map_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
M : Matrix n n R
inst✝ : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
⊢ M.charpoly = X ^ 2 - C M.trace * X + C M.det

Tactic:
ext i

Goal state after:
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
M : Matrix n n R
inst✝ : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
i : ℕ
⊢ M.charpoly.coeff i = (X ^ 2 - C M.trace * X + C M.det).coeff i
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ (hasseDeriv n) p = 0

Tactic:
rw [hasseDeriv_apply, sum_def]
  refine Finset.sum_eq_zero fun x hx => ?_
  simp [Nat.choose_eq_zero_of_lt ((le_natDegree_of_mem_supp _ hx).trans_lt h)]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
⊢ (hasseDeriv k) ((monomial n) r) = (monomial (n - k)) (↑(n.choose k) * r)

Tactic:
ext i

Goal state after:
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
⊢ ((hasseDeriv k) ((monomial n) r)).coeff i = ((monomial (n - k)) (↑(n.choose k) * r)).coeff i
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case inr.inr
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
i j : { a // a ∉ s }
⊢ s.piecewise M 1 ↑i ↑j = 1 i j

Tactic:
· simp only [Finset.piecewise, if_neg i.prop, Matrix.one_apply, Subtype.ext_iff]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
n : ℕ
⊢ lcoeff R n ∘ₗ taylor r = leval r ∘ₗ hasseDeriv n

Tactic:
ext i

Goal state after:
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
⊢ ((lcoeff R n ∘ₗ taylor r) ∘ₗ monomial i) 1 = ((leval r ∘ₗ hasseDeriv n) ∘ₗ monomial i) 1
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
i : ℕ
⊢ p.coeff i ≠ 0 → p.coeff i * s ^ (p.natDegree - i) ≠ 0

Tactic:
intro p_ne_zero ps_zero

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
i : ℕ
p_ne_zero : p.coeff i ≠ 0
ps_zero : p.coeff i * s ^ (p.natDegree - i) = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : x.1 ≤ m
hn : x.2 ≤ n
⊢ (monomial (m + n - (x.1 + x.2))) (↑(m.choose x.1) * (r * ↑(n.choose x.2) * s)) =
    (monomial (m + n - (x.1 + x.2))) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))

Tactic:
← (Nat.cast_commute _ r).eq,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : x.1 ≤ m
hn : x.2 ≤ n
⊢ (monomial (m + n - (x.1 + x.2))) (↑(m.choose x.1) * (↑(n.choose x.2) * r * s)) =
    (monomial (m + n - (x.1 + x.2))) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.integralNormalization * C p.leadingCoeff = p.scaleRoots p.leadingCoeff

Tactic:
ext i

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
⊢ (p.integralNormalization * C p.leadingCoeff).coeff i = (p.scaleRoots p.leadingCoeff).coeff i
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
A : Type u_1
inst✝ : Semiring A
f : R →+* A
p : R[X]
H : f p.leadingCoeff ≠ 0
⊢ (map f p).integralNormalization = map f p.integralNormalization

Tactic:
ext i

Goal state after:
R : Type u
inst✝¹ : Semiring R
A : Type u_1
inst✝ : Semiring A
f : R →+* A
p : R[X]
H : f p.leadingCoeff ≠ 0
i : ℕ
⊢ (map f p).integralNormalization.coeff i = (map f p.integralNormalization).coeff i
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
a✝ : Nontrivial R
this : IsDomain R
hf : ¬f = 0
⊢ f.integralNormalization.support = f.support

Tactic:
ext i

Goal state after:
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
a✝ : Nontrivial R
this : IsDomain R
hf : ¬f = 0
i : ℕ
⊢ i ∈ f.integralNormalization.support ↔ i ∈ f.support
Module: Mathlib.RingTheory.Polynomial.Subring

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
⊢ (p.toSubring T hp).support = p.support

Tactic:
ext i

Goal state after:
R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
i : ℕ
⊢ i ∈ (p.toSubring T hp).support ↔ i ∈ p.support
Module: Mathlib.RingTheory.Polynomial.Subring

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
T : Subring R
⊢ toSubring 0 T ⋯ = 0

Tactic:
ext i

Goal state after:
R : Type u_1
inst✝ : Ring R
T : Subring R
i : ℕ
⊢ ↑((toSubring 0 T ⋯).coeff i) = ↑(coeff 0 i)
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
⊢ f.natDegree = f.roots.card

Tactic:
by_cases hf0 : f.leadingCoeff = 0
  · simp [leadingCoeff_eq_zero.mp hf0]
  · conv_lhs => rw [hf.eq_prod_roots, natDegree_C_mul hf0, natDegree_multiset_prod_X_sub_C_eq_card]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
⊢ Function.Injective
    ⇑(quotientMap (map (mapRingHom (Quotient.mk (comap C P))) P) (mapRingHom (Quotient.mk (comap C P))) ⋯)

Tactic:
refine quotientMap_injective' (le_of_eq ?_)
  rw [comap_map_of_surjective (mapRingHom (Ideal.Quotient.mk (P.comap (C : R →+* R[X]))))
      (map_surjective (Ideal.Quotient.mk (P.comap (C : R →+* R[X]))) Ideal.Quotient.mk_surjective)]
  refine le_antisymm (sup_le le_rfl ?_) (le_sup_of_le_left le_rfl)
  refine fun p hp =>
    polynomial_mem_ideal_of_coeff_mem_ideal P p fun n => Ideal.Quotient.eq_zero_iff_mem.mp ?_
  simpa only [coeff_map, coe_mapRingHom] using! ext_iff.mp (Ideal.mem_bot.mp (mem_comap.mp hp)) n

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Ring A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : NoZeroDivisors S
inst✝¹ : Algebra.IsAlgebraic R S
inst✝ : FaithfulSMul R S
⊢ Algebra.IsAlgebraic R A ↔ Algebra.IsAlgebraic S A

Tactic:
by
  simp_rw [Algebra.isAlgebraic_def, Algebra.IsAlgebraic.isAlgebraic_iff R S]

Goal state after:
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
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
x : S ⊗[R] T
J : Ideal T
hJ : J.IsPrime
⊢ ∃ t r a, r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t

Tactic:
induction x with

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

Goal state before:
pp: case inr
ι : Type u_3
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
x✝¹ x✝ : (i : ι) × PrimeSpectrum (R i)
i : ι
p : PrimeSpectrum (R i)
j : ι
q : PrimeSpectrum (R j)
eq : sigmaToPi R ⟨i, p⟩ = sigmaToPi R ⟨j, q⟩
ne : i ≠ j
this : Function.update 1 j 0 ∈ (sigmaToPi R ⟨j, q⟩).asIdeal
⊢ 1 ∈ p.asIdeal

Tactic:
simpa [← eq, Function.update_of_ne ne]

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

Goal state before:
pp: ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
⊢ ∀ (c : (i : ι) → R i) {x : (i : ι) → R i},
    x ∈ (AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom).carrier →
      c • x ∈ (AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom).carrier

Tactic:
rintro r _ ⟨x, rfl⟩

Goal state after:
ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
r : (i : ι) → R i
x : Π₀ (i : ι), R i
⊢ r • DFinsupp.coeFnAddMonoidHom x ∈ (AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom).carrier
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mpr.refine_1
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.under R ⁻¹' J.minimalPrimes
⊢ (Ideal.under R p).IsPrime ∧ Disjoint ↑S ↑(Ideal.under R p)

Tactic:
IsLocalization.disjoint_under_iff S

Goal state after:
case mpr.refine_1
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.under R ⁻¹' J.minimalPrimes
⊢ (Ideal.under R p).IsPrime ∧ p ≠ ⊤
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ c✝ : α
hac : a✝ ≤ b✝
hbc : a✝ ≤ c✝
⊢ a✝ ≤ inf b✝ c✝

Tactic:
simp [eq_inf, hac, hbc]

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : GeneralizedHeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
himp : α → α → α
eq_himp : himp = HImp.himp
⊢ ∀ (x y : α), x ≤ y ↔ x ≤ y

Tactic:
by rw [← eq_le]; exact fun _ _ ↦ .rfl

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : GeneralizedCoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
⊢ ∀ (x y : α), x ≤ y ↔ x ≤ y

Tactic:
by rw [← eq_le]; exact fun _ _ ↦ .rfl

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : HeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
himp : α → α → α
eq_himp : himp = HImp.himp
compl : α → α
eq_compl : compl = Compl.compl
⊢ ∀ (x y : α), x ≤ y ↔ x ≤ y

Tactic:
by rw [← eq_le]; exact fun _ _ ↦ .rfl

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
eq_hnot : hnot = HNot.hnot
⊢ ∀ (x y : α), x ≤ y ↔ x ≤ y

Tactic:
by rw [← eq_le]; exact fun _ _ ↦ .rfl

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

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us
⊢ ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U

Tactic:
intro U

Goal state after:
case mpr
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us
U : Opens α
⊢ ∀ {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
L M : BooleanSubalgebra α
f : BoundedLatticeHom α β
hf : Injective ⇑f
⊢ map f (L ⊓ M) = map f L ⊓ map f M

Tactic:
rw [← SetLike.coe_set_eq]

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
L M : BooleanSubalgebra α
f : BoundedLatticeHom α β
hf : Injective ⇑f
⊢ ↑(map f (L ⊓ M)) = ↑(map f L ⊓ map f M)
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
⊢ closure[inst✝] (range f) = univ ↔ ∀ (i : ι), closure[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' range f) = univ

Tactic:
← (U _).2.isOpenEmbedding_subtypeVal.isOpenMap.preimage_closure_eq_closure_preimage
      continuous_subtype_val

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
⊢ closure[inst✝] (range f) = univ ↔ ∀ (i : ι), Subtype.val ⁻¹' closure[inst✝] (range f) = univ
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: case refine_3
α : 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, (t✝.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = t.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✝² : ↑s × ↑s
tc : Finset (↑s × ↑s)
x✝¹ : ∃ t, ((↑x \ ↑y)ᶜ ⊓ tc.sup fun x ↦ ↑x.1 \ ↑x.2) = t.sup fun x ↦ ↑x.1 \ ↑x.2
z w : ↑s
x✝ : (z, w) ∉ tc
t : Finset (↑s × ↑s)
eq : ((↑x \ ↑y)ᶜ ⊓ tc.sup fun x ↦ ↑x.1 \ ↑x.2) = t.sup fun x ↦ ↑x.1 \ ↑x.2
⊢ ∃ t, ((↑x \ ↑y)ᶜ ⊓ (insert (z, w) tc).sup fun x ↦ ↑x.1 \ ↑x.2) = t.sup fun x ↦ ↑x.1 \ ↑x.2

Tactic:
simp_rw [Finset.sup_insert, inf_sup_left, eq]

Goal state after:
case refine_3
α : 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, (t✝.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = t.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✝² : ↑s × ↑s
tc : Finset (↑s × ↑s)
x✝¹ : ∃ t, ((↑x \ ↑y)ᶜ ⊓ tc.sup fun x ↦ ↑x.1 \ ↑x.2) = t.sup fun x ↦ ↑x.1 \ ↑x.2
z w : ↑s
x✝ : (z, w) ∉ tc
t : Finset (↑s × ↑s)
eq : ((↑x \ ↑y)ᶜ ⊓ tc.sup fun x ↦ ↑x.1 \ ↑x.2) = t.sup fun x ↦ ↑x.1 \ ↑x.2
⊢ ∃ t_1, ((↑x \ ↑y)ᶜ ⊓ ↑z \ ↑w ⊔ t.sup fun x ↦ ↑x.1 \ ↑x.2) = t_1.sup fun x ↦ ↑x.1 \ ↑x.2
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : Closeds α
s : Set (Closeds α)
⊢ ↑(⨅ b ∈ s, a ⊔ b) = ↑(a ⊔ sInf s)

Tactic:
by simp only [coe_sup, coe_iInf, coe_sInf, Set.union_iInter₂]

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
⊢ IsQuasiSeparated (f '' s)

Tactic:
intro U

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U : Set β
⊢ ∀ (V : Set β),
    U ⊆ f '' s → IsOpen[inst✝] U → IsCompact U → V ⊆ f '' s → IsOpen[inst✝] V → IsCompact V → IsCompact (U ∩ V)
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: X : Type u_6
Y : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : Continuous[inst✝², inst✝¹] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ ↑(iSup U)
V : ι → Type u_5
inst✝ : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst✝ i, inst✝²] (iV i)
hV : ∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
⊢ IsEmbedding f

Tactic:
wlog hU' : iSup U = ⊤
  · let f₀ : X → Set.range f := fun x ↦ ⟨f x, ⟨x, rfl⟩⟩
    suffices IsEmbedding f₀ from IsEmbedding.subtypeVal.comp this
    have hU'' : (⨆ i, (U i).comap ⟨Subtype.val, continuous_subtype_val⟩ :
        Opens (Set.range f)) = ⊤ := by
      rw [← top_le_iff]
      simpa [Set.range_subset_iff, SetLike.le_def] using hU
    refine this _ ?_ _ ?_ V iV hiV ?_ ?_ hU''
    · fun_prop
    · rw [hU'']; simp
    · exact hV
    · exact fun i ↦ IsEmbedding.of_comp (by fun_prop) continuous_subtype_val (hV' i)
  rw [(IsOpenCover.mk hU').isEmbedding_iff_restrictPreimage h]
  intro i
  let f' := (Subtype.val ∘ (f ⁻¹' U i).restrictPreimage (iV i))
  have : IsEmbedding f' :=
    IsEmbedding.subtypeVal.comp ((IsEmbedding.of_comp (hiV i) h (hV' _)).restrictPreimage _)
  have hf' : Set.range f' = f ⁻¹' U i := by
    simpa [f', Set.range_comp, Set.range_restrictPreimage] using hV i
  let e := this.toHomeomorph.trans (Homeomorph.setCongr hf')
  refine IsEmbedding.of_comp (by fun_prop) continuous_subtype_val ?_
  convert! ((hV' i).comp IsEmbedding.subtypeVal).comp e.symm.isEmbedding
  ext x
  obtain ⟨x, rfl⟩ := e.surjective x
  simp
  rfl

Goal state after:
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:
intro U

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
ht : IsQuasiSeparated t
h : s ⊆ t
U : Set α
⊢ ∀ (V : Set α), U ⊆ s → IsOpen[inst✝] U → IsCompact U → V ⊆ s → IsOpen[inst✝] V → IsCompact V → IsCompact (U ∩ V)
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
I : Order.Ideal (CompactOpens X)
U : CompactOpens X
H : ↑U.toOpens ⊆ ⋃ i ∈ I, ↑i.toOpens
s : Set (CompactOpens X)
hsI : s ⊆ ↑I
hs : s.Finite
hU : ↑U ⊆ ⋃ i ∈ s, ↑i.toOpens
⊢ U ∈ ↑I

Tactic:
exact I.lower (a := hs.toFinset.sup fun i ↦ i) (by simpa [← SetLike.coe_subset_coe]) (by simpa)

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
this :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)},
    s.Finite →
      s.Nonempty → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen t) → IsCompact (⋂₀ s)
a : Set (Set α) := {t | t ∈ s ∧ IsOpen[inst✝¹] t}
b : Set (Set α) := {t | t ∈ s ∧ IsClosed[inst✝¹] t}
heq : s = a ∪ b
t : Set α
ht : t ∈ s
hno : ¬IsOpen[inst✝¹] t
ha : a.Nonempty
⊢ IsCompact (⋂₀ a ∩ ⋂₀ b)

Tactic:
apply IsCompact.inter_right
      · apply this (hf.subset (by grind)) ha <;> grind
      · exact isClosed_sInter (by grind)

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K L : Compacts α
h : Disjoint K L
⊢ Disjoint ↑K ↑L

Tactic:
rw [Set.disjoint_iff]
    intro x ⟨hxK, hxL⟩
    specialize @h {x}
    simp_rw [← SetLike.coe_subset_coe, coe_singleton, singleton_subset_iff] at h
    exact h hxK hxL

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, IsRetrocompact (t i)) → IsRetrocompact (s.sup t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)
⊢ IsRetrocompact ((Finset.cons i s ih).sup t)

Tactic:
rw [Finset.sup_cons]
    exact (ht _ <| by simp).union <| hi <| Finset.forall_of_forall_cons ht

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
⊢ QuasiSober α ↔ ∀ (i : ι), QuasiSober ↥(U i)

Tactic:
refine ⟨fun h i ↦ (U i).isOpenEmbedding'.quasiSober, fun hU' ↦ (quasiSober_iff _).mpr ?_⟩
  · rintro t ⟨⟨x, hx⟩, h⟩ h'
    obtain ⟨i, hi⟩ := hU.exists_mem x
    have H : IsIrreducible ((↑) ⁻¹' t : Set (U i)) :=
      ⟨⟨⟨x, hi⟩, hx⟩, h.preimage (U i).isOpenEmbedding'⟩
    use H.genericPoint
    apply le_antisymm
    · simpa [h'.closure_subset_iff, h'.closure_eq] using!
        continuous_subtype_val.closure_preimage_subset _ H.isGenericPoint_genericPoint_closure.mem
    rw [← image_singleton, ← closure_image_closure continuous_subtype_val,
      H.isGenericPoint_genericPoint_closure.def]
    refine (subset_closure_inter_of_isPreirreducible_of_isOpen h (U i).isOpen ⟨x, ⟨hx, hi⟩⟩).trans
      (closure_mono ?_)
    simpa only [inter_comm t, ← Subtype.image_preimage_coe] using! Set.image_mono subset_closure

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : R1Space α
S✝ : Set α
h : IsIrreducible S✝
hs : IsClosed S✝
⊢ ∃ x, IsGenericPoint x S✝

Tactic:
obtain ⟨x, hx⟩ := h.nonempty

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : R1Space α
S✝ : Set α
h : IsIrreducible S✝
hs : IsClosed S✝
x : α
hx : x ∈ S✝
⊢ ∃ x, IsGenericPoint x S✝
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case open_retrocompact
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
U : Set X
hUopen : IsOpen[inst✝¹] U
hUcomp : IsRetrocompact U
hfU : IsOpen[inst✝] (f '' U ∪ (range f)ᶜ)
V : Set Y
hVcomp : IsCompact V
hVopen : IsOpen[inst✝] V
⊢ IsCompact ((f '' U ∪ (range f)ᶜ) ∩ V)

Tactic:
union_inter_distrib_right,

Goal state after:
case open_retrocompact
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
U : Set X
hUopen : IsOpen[inst✝¹] U
hUcomp : IsRetrocompact U
hfU : IsOpen[inst✝] (f '' U ∪ (range f)ᶜ)
V : Set Y
hVcomp : IsCompact V
hVopen : IsOpen[inst✝] V
⊢ IsCompact (f '' U ∩ V ∪ (range f)ᶜ ∩ V)
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsLocallyConstructible s
hf : IsOpenEmbedding f
⊢ IsLocallyConstructible (f ⁻¹' s)

Tactic:
intro x
  obtain ⟨U, hxU, hU, H⟩ := hs (f x)
  exact ⟨f ⁻¹' U, hf.continuous.continuousAt.preimage_mem_nhds hxU, hU.preimage hf.continuous,
    (H.preimage_of_isOpenEmbedding (hf.restrictPreimage _) :)⟩

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

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : HasGoingDown R S
inst✝ : HasGoingDown S T
⊢ HasGoingDown R T

Tactic:
rw [iff_generalizingMap_primeSpectrumComap, IsScalarTower.algebraMap_eq R S T]
  simp only [PrimeSpectrum.comap_comp]
  apply GeneralizingMap.comp
  · rwa [← iff_generalizingMap_primeSpectrumComap]
  · rwa [← iff_generalizingMap_primeSpectrumComap]

Goal state after: