mathlib-initiative/mathlib-tactics huggingface dataset:
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:
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:
simp

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a : α
S : Set (BooleanSubalgebra α)
⊢ a ∈ ↑(sInf S) ↔ ∀ L ∈ S, a ∈ L

Tactic:
simp

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : BooleanAlgebra α
a : α
f : ι → BooleanSubalgebra α
⊢ a ∈ ↑(⨅ i, f i) ↔ ∀ (i : ι), a ∈ f i

Tactic:
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:
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:
simp

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

Goal state before:
pp: case e'_3
α : Type u_2
inst✝ : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U x✝ : Set α
⊢ (x✝ ∈ range fun i ↦ (b i).carrier) ↔ x✝ ∈ SetLike.coe '' range b

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ IsCompact U ∧ IsOpen[inst✝] U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, ↑(b i)

Tactic:
apply isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis fun i : ι => (b i).1
  · convert! (config := { transparency := .default }) hb
    ext
    simp
  · exact hb'

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:
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:
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:
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:
simp

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

Goal state before:
pp: ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (α i)
B : (i : ι) → Set (Opens (α i))
hB : ∀ (i : ι), IsBasis (B i)
⊢ IsTopologicalBasis (⋃ i, (SetLike.coe ∘ fun U ↦ { carrier := Sigma.mk i '' U.carrier, is_open' := ⋯ }) '' B i) ↔
    IsTopologicalBasis (⋃ i, (fun u ↦ Sigma.mk i '' u) ∘ SetLike.coe '' B i)

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
B : Set (Opens β)
H : IsTopologicalBasis (SetLike.coe '' B)
f : α → β
h : IsInducing f
x✝ : Set α
⊢ x✝ ∈ SetLike.coe '' {x | ∃ U ∈ B, { carrier := f ⁻¹' ↑U, is_open' := ⋯ } = x} ↔ x✝ ∈ preimage f '' SetLike.coe '' B

Tactic:
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)
⊢ (∅.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = {(⟨⊤, top_mem⟩, ⟨⊥, bot_mem⟩)}.sup fun x ↦ ↑x.1 \ ↑x.2

Tactic:
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:
simp

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
H : ∀ y < ⊥, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
⊢ ∅.Finite ∧ (∀ t ∈ ∅, IsIrreducible ↑t) ∧ ⊥ = sSup ∅

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
ι : Sort u_4
s : ι → Closeds α
x✝ : α
⊢ x✝ ∈ ↑(⨅ i, s i) ↔ x✝ ∈ ⋂ i, ↑(s i)

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
ι : Sort u_4
s : ι → Closeds α
⊢ ↑(⨅ i, s i) = ↑{ carrier := ⋂ i, ↑(s i), isClosed' := ⋯ }

Tactic:
simp

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

Goal state before:
pp: case empty
ι : Type u_1
α : Type u_2
inst✝ : TopologicalSpace α
U : ι → Clopens α
⊢ ↑(∅.sup U) = ⋃ i ∈ ∅, ↑(U i)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: case inr.refine_2
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)
this :
  ∀ {X : Type u_6} {Y : Type u_7} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f →
      ∀ {ι : Type u_4} (U : ι → Opens Y),
        range f ⊆ ↑(iSup U) →
          ∀ (V : ι → Type u_5) [inst_2 : (i : ι) → TopologicalSpace (V i)] (iV : (i : ι) → V i → X),
            (∀ (i : ι), Continuous (iV i)) →
              (∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)) →
                (∀ (i : ι), IsEmbedding (f ∘ iV i)) → iSup U = ⊤ → IsEmbedding f
hU' : ¬iSup U = ⊤
f₀ : X → ↑(range f) := fun x ↦ ⟨f x, ⋯⟩
hU'' : ⨆ i, (Opens.comap { toFun := Subtype.val, continuous_toFun := ⋯ }) (U i) = ⊤
⊢ range f₀ ⊆ ↑⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: case e'_5
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)
hU' : iSup U = ⊤
i : ι
f' : ↑(iV i ⁻¹' f ⁻¹' ↑(U i)) → X := Subtype.val ∘ (f ⁻¹' ↑(U i)).restrictPreimage (iV i)
this : IsEmbedding f'
hf' : range f' = f ⁻¹' ↑(U i)
e : ↑(iV i ⁻¹' f ⁻¹' ↑(U i)) ≃ₜ ↑(f ⁻¹' ↑(U i)) := this.toHomeomorph.trans (Homeomorph.setCongr hf')
e_1✝ : ↑(f ⁻¹' (U i).carrier) = ↑(f ⁻¹' ↑(U i))
x : ↑(iV i ⁻¹' f ⁻¹' ↑(U i))
⊢ (Subtype.val ∘ (U i).carrier.restrictPreimage f) (e x) = (((f ∘ iV i) ∘ Subtype.val) ∘ ⇑e.symm) (e x)

Tactic:
simp

Goal state after:
case e'_5
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)
hU' : iSup U = ⊤
i : ι
f' : ↑(iV i ⁻¹' f ⁻¹' ↑(U i)) → X := Subtype.val ∘ (f ⁻¹' ↑(U i)).restrictPreimage (iV i)
this : IsEmbedding f'
hf' : range f' = f ⁻¹' ↑(U i)
e : ↑(iV i ⁻¹' f ⁻¹' ↑(U i)) ≃ₜ ↑(f ⁻¹' ↑(U i)) := this.toHomeomorph.trans (Homeomorph.setCongr hf')
e_1✝ : ↑(f ⁻¹' (U i).carrier) = ↑(f ⁻¹' ↑(U i))
x : ↑(iV i ⁻¹' f ⁻¹' ↑(U i))
⊢ f ↑(e x) = f (iV i ↑x)
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsOpen[inst✝] s
⊢ s = Subtype.val '' univ

Tactic:
simp

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:
simp

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : Preorder P
inst✝ : OrderBot P
⊢ ∀ (a : Ideal P), principal ⊥ ≤ a

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: case empty
α✝ : Type u_1
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
ho : ∀ t ∈ ∅, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ ∅, IsCompact t
h : ∀ t ∈ ∅, IsOpen[inst✝¹] t
⊢ ∅.Nonempty → IsCompact (⋂₀ ∅)

Tactic:
simp

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
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst✝¹] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U | IsCompact ↑U}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ } = sSup Us
t : Finset ↑Us
ht : U ⊆ ⋃ i ∈ t, f '' ↑↑i
⊢ ⋃ i, ⋃ (x : i ∈ Us), ⋃ (_ : ⟨i, ⋯⟩ ∈ t), f '' ↑i = ⋃ i ∈ t, f '' ↑↑i

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : IsCodirectedOrder P
x✝ : P
I✝ J✝ s t I J : Ideal P
x : P
hx : x ∈ (I.toLowerSet ⊓ J.toLowerSet).carrier
y : P
hy : y ∈ (I.toLowerSet ⊓ J.toLowerSet).carrier
⊢ (fun x1 x2 ↦ x1 ≤ x2) x (x ⊔ y) ∧ (fun x1 x2 ↦ x1 ≤ x2) y (x ⊔ y)

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hKU : K ⊆ U
⊢ IsCompact ∅ ∧ IsOpen[inst✝¹] ∅ ∧ ∅ ⊆ ∅ ∧ ∅ ⊆ U

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K : Compacts α
U : Opens α
h : U ∈ K.openRcNhds
x : ↥K
⊢ ↑x ∈ ↑K

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case empty
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
t : ι → Set X
ht : ∀ i ∈ ∅, IsRetrocompact (t i)
⊢ IsRetrocompact (∅.sup t)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: 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)
⊢ i ∈ Finset.cons i s ih

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: case refine_2
P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
S : Set (Ideal P)
hS₁ : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
hS₂ : S.Nonempty
hS₃ : ⊤ ∉ S
⊢ ∀ (x y : Ideal P), x ≤ y → ↑x ⊆ ↑y

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case empty
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
ι : Type u_4
t : ι → Set X
ht : ∀ i ∈ ∅, IsRetrocompact (t i)
⊢ IsRetrocompact (∅.inf t)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: 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)
⊢ i ∈ Finset.cons i s ih

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K : NonemptyCompacts α
x✝ : α
⊢ x✝ ∈ ↑(NonemptyCompacts.map id ⋯ K) ↔ x✝ ∈ ↑K

Tactic:
simp

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 γ
f : β → γ
g : α → β
hf : Continuous f
hg : Continuous g
K : NonemptyCompacts α
x✝ : γ
⊢ x✝ ∈ ↑(NonemptyCompacts.map (f ∘ g) ⋯ K) ↔ x✝ ∈ ↑(NonemptyCompacts.map f hf (NonemptyCompacts.map g hg K))

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous f
x : α
x✝ : β
⊢ x✝ ∈ ↑(NonemptyCompacts.map f hf {x}) ↔ x✝ ∈ ↑{f x}

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : QuasiSober α
inst✝ : IrreducibleSpace α
x : α
⊢ x ∈ closure univ

Tactic:
simp

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 α
s : Set α
hs : IsIrreducible s
hs' : IsClosed s
t : Set α
ht : IsIrreducible t
ht' : IsClosed t
⊢ closure
        {{ toFun := fun s ↦ ⋯.genericPoint,
              invFun := fun x ↦ { carrier := closure {x}, isIrreducible' := ⋯, isClosed' := ⋯ }, left_inv := ⋯,
              right_inv := ⋯ }
            { carrier := s, isIrreducible' := hs, isClosed' := hs' }} ⊆
      closure
        {{ toFun := fun s ↦ ⋯.genericPoint,
              invFun := fun x ↦ { carrier := closure {x}, isIrreducible' := ⋯, isClosed' := ⋯ }, left_inv := ⋯,
              right_inv := ⋯ }
            { carrier := t, isIrreducible' := ht, isClosed' := ht' }} ↔
    { carrier := s, isIrreducible' := hs, isClosed' := hs' } ≤ { carrier := t, isIrreducible' := ht, isClosed' := ht' }

Tactic:
simp

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : QuasiSober α
inst✝ : T0Space α
s : Set α
hs : IsIrreducible s
hs' : IsClosed s
t : Set α
ht : IsIrreducible t
ht' : IsClosed t
⊢ s ⊆ t ↔
    { carrier := s, isIrreducible' := hs, isClosed' := hs' } ≤ { carrier := t, isIrreducible' := ht, isClosed' := ht' }
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
V W : Set α
inst✝ : QuasiSober ↑W
hV : IsClosed V
⊢ QuasiSober ↑(W ∩ V)

Tactic:
by
  refine QuasiSober.of_subset ?_ (Set.inter_subset_left : W ∩ V ⊆ W)
  rw [Subtype.preimage_coe_self_inter W V]
  exact IsClosed.preimage_val hV

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsConstructible s
x✝ : X
⊢ univ ∈ 𝓝 x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsConstructible s
x✝ : X
⊢ IsOpen[inst✝] univ

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsConstructible s
x✝ : X
⊢ IsRetrocompact (range Subtype.val)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsConstructible s
x✝ : X
⊢ s ⊆ range Subtype.val

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case empty
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
t : ι → Set X
ht : ∀ i ∈ ∅, IsLocallyConstructible (t i)
⊢ IsLocallyConstructible (∅.inf t)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: 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)
⊢ i ∈ Finset.cons i s ih

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst✝] U
hsU : IsConstructible (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen[inst✝] V
htV : IsConstructible (V ↓∩ t)
x✝ : ↑(U ∩ V)
⊢ x✝ ∈ (U ∩ V) ↓∩ (s ∪ t) ↔ x✝ ∈ inclusion ⋯ ⁻¹' U ↓∩ s ∪ inclusion ⋯ ⁻¹' V ↓∩ t

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.RingHom.FaithfullyFlat

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Bijective ⇑f
p : PrimeSpectrum R
x✝ : R
⊢ (RingEquiv.ofBijective f hf) (((↑(RingEquiv.ofBijective f hf).symm).comp f) x✝) =
    (RingEquiv.ofBijective f hf) ((id R) x✝)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.RingHom.FaithfullyFlat

Goal state before:
pp: ⊢ IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ FaithfullyFlat

Tactic:
refine .mk respectsIso (fun R S T _ _ _ _ _ _ ↦ show (algebraMap _ _).FaithfullyFlat from ?_)

Goal state after:
R S T : Type u_3
x✝⁵ : CommRing R
x✝⁴ : CommRing S
x✝³ : CommRing T
x✝² : Algebra R S
x✝¹ : Algebra R T
x✝ : (algebraMap R T).FaithfullyFlat
⊢ (algebraMap S (TensorProduct R S T)).FaithfullyFlat
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: case refine_2
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)
⊢ ↑((diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯) 1) = ↑0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : CommMonoid H
inst✝ : PartialOrder H
e : G ≃*o H
⊢ ∀ {a b : Additive G}, (MulEquiv.toAdditive ↑e).toFun a ≤ (MulEquiv.toAdditive ↑e).toFun b ↔ a ≤ b

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : CommMonoid H
inst✝ : PartialOrder H
e : Additive G ≃+o Additive H
⊢ ∀ {a b : G}, (MulEquiv.toAdditive.symm ↑e).toFun a ≤ (MulEquiv.toAdditive.symm ↑e).toFun b ↔ a ≤ b

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : CommMonoid H
inst✝ : PartialOrder H
e : G ≃*o H
a✝ : G
⊢ ((fun e ↦ { toMulEquiv := MulEquiv.toAdditive.symm ↑e, map_le_map_iff' := ⋯ })
        ((fun e ↦ { toAddEquiv := MulEquiv.toAdditive ↑e, map_le_map_iff' := ⋯ }) e))
      a✝ =
    e a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : CommMonoid H
inst✝ : PartialOrder H
e : Additive G ≃+o Additive H
a✝ : Additive G
⊢ Additive.toMul
      (((fun e ↦ { toAddEquiv := MulEquiv.toAdditive ↑e, map_le_map_iff' := ⋯ })
          ((fun e ↦ { toMulEquiv := MulEquiv.toAdditive.symm ↑e, map_le_map_iff' := ⋯ }) e))
        a✝) =
    Additive.toMul (e a✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : AddCommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : G ≃+o H
⊢ ∀ {a b : Multiplicative G}, (AddEquiv.toMultiplicative ↑e).toFun a ≤ (AddEquiv.toMultiplicative ↑e).toFun b ↔ a ≤ b

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : AddCommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : Multiplicative G ≃*o Multiplicative H
⊢ ∀ {a b : G}, (AddEquiv.toMultiplicative.symm ↑e).toFun a ≤ (AddEquiv.toMultiplicative.symm ↑e).toFun b ↔ a ≤ b

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : AddCommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : G ≃+o H
a✝ : G
⊢ ((fun e ↦ { toAddEquiv := AddEquiv.toMultiplicative.symm ↑e, map_le_map_iff' := ⋯ })
        ((fun e ↦ { toMulEquiv := AddEquiv.toMultiplicative ↑e, map_le_map_iff' := ⋯ }) e))
      a✝ =
    e a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : AddCommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : Multiplicative G ≃*o Multiplicative H
a✝ : Multiplicative G
⊢ Multiplicative.toAdd
      (((fun e ↦ { toMulEquiv := AddEquiv.toMultiplicative ↑e, map_le_map_iff' := ⋯ })
          ((fun e ↦ { toAddEquiv := AddEquiv.toMultiplicative.symm ↑e, map_le_map_iff' := ⋯ }) e))
        a✝) =
    Multiplicative.toAdd (e a✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : Additive G ≃+o H
⊢ ∀ {a b : G},
    (AddEquiv.toMultiplicativeRight e.toAddEquiv).toFun a ≤ (AddEquiv.toMultiplicativeRight e.toAddEquiv).toFun b ↔
      a ≤ b

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : G ≃*o Multiplicative H
⊢ ∀ {a b : Additive G},
    (MulEquiv.toAdditiveLeft e.toMulEquiv).toFun a ≤ (MulEquiv.toAdditiveLeft e.toMulEquiv).toFun b ↔ a ≤ b

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : Additive G ≃+o H
a✝ : Additive G
⊢ ((fun e ↦ { toAddEquiv := MulEquiv.toAdditiveLeft e.toMulEquiv, map_le_map_iff' := ⋯ })
        ((fun e ↦ { toMulEquiv := AddEquiv.toMultiplicativeRight e.toAddEquiv, map_le_map_iff' := ⋯ }) e))
      a✝ =
    e a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : G ≃*o Multiplicative H
a✝ : G
⊢ Multiplicative.toAdd
      (((fun e ↦ { toMulEquiv := AddEquiv.toMultiplicativeRight e.toAddEquiv, map_le_map_iff' := ⋯ })
          ((fun e ↦ { toAddEquiv := MulEquiv.toAdditiveLeft e.toMulEquiv, map_le_map_iff' := ⋯ }) e))
        a✝) =
    Multiplicative.toAdd (e a✝)

Tactic:
simp

Goal state after: