mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: a b m n✝ p : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
⊢ motive (k + 2)

Tactic:
letI p := (k + 2).minFac
      haveI hp : Prime p := minFac_prime (succ_succ_ne_one k)
      letI t := (k + 2).factorization p
      haveI hpt : p ^ t ∣ k + 2 := ordProj_dvd _ _
      haveI htp : 0 < t := hp.factorization_pos_of_dvd (k + 1).succ_ne_zero (k + 2).minFac_dvd
      convert! prime_pow_mul ((k + 2) / p ^ t) p t hp _ htp (hk _ (Nat.div_lt_of_lt_mul _)) using 1
      · rw [Nat.mul_div_cancel' hpt]
      · rw [Nat.dvd_div_iff_mul_dvd hpt, ← Nat.pow_succ]
        exact pow_succ_factorization_not_dvd (k + 1).succ_ne_zero hp
      · simp [htp.ne', hp.one_lt]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: motive : ℕ → Prop
zero : motive 0
one : motive 1
prime_mul : ∀ (p a : ℕ), Prime p → motive a → motive (p * a)
a p n : ℕ
hp : Prime p
ha : motive a
⊢ motive (p ^ n * a)

Tactic:
induction n with
  | zero => simpa using ha
  | succ n ih =>
    rw [pow_succ', mul_assoc]
    exact prime_mul _ _ hp ih

Goal state after:
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p : ℕ
hp : 1 < p
inst✝ : Fintype (ZMod p)ˣ
⊢ Fintype.card (ZMod p)ˣ ≤ p - 1

Tactic:
have : NeZero p := ⟨(pos_of_gt hp).ne'⟩

Goal state after:
p : ℕ
hp : 1 < p
inst✝ : Fintype (ZMod p)ˣ
this : NeZero p
⊢ Fintype.card (ZMod p)ˣ ≤ p - 1
Module: Mathlib.Order.Filter.Curry

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
m : Filter β
s : Set α
t : Set β
inst✝¹ : l.NeBot
inst✝ : m.NeBot
⊢ (∀ᶠ (x : α × β) in l.curry m, x ∈ s ×ˢ t) ↔ s ∈ l ∧ t ∈ m

Tactic:
by
  simp [eventually_curry_iff]

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a b - b = -toIocDiv hp a b • p

Tactic:
by
  rw [toIocMod, sub_sub_cancel_left, neg_smul]

Goal state after:
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht : t ∈ iInf f
⊢ ⨅ i, (f i).lift g ≤ g univ

Tactic:
inhabit ι

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht : t ∈ iInf f
inhabited_h : Inhabited ι
⊢ ⨅ i, (f i).lift g ≤ g univ
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a (p + b) = toIcoMod hp a b

Tactic:
rw [add_comm, toIcoMod_add_right]

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : toIcoMod hp a b = toIcoMod hp a c
⊢ c - b = (toIcoDiv hp a c - toIcoDiv hp a b) • p

Tactic:
conv_lhs => rw [← toIcoMod_add_toIcoDiv_zsmul hp a b, ← toIcoMod_add_toIcoDiv_zsmul hp a c]
    rw [h, sub_smul]
    abel

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ s ⊆ t ∪ closure t ↔ s ⊆ closure t

Tactic:
union_eq_self_of_subset_left subset_closure

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ s ⊆ closure t ↔ s ⊆ closure t
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
tfae_3_to_2 : toIcoMod hp a b ≠ toIocMod hp a b → ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : toIcoMod hp a b + p = toIocMod hp a b → toIcoMod hp a b ≠ toIocMod hp a b
x✝ : toIcoMod hp a b = a
h : toIcoMod hp a b = a := x✝
⊢ a < a + p ∧ ∃ z, b = a + p + z • p

Tactic:
refine ⟨lt_add_of_pos_right a hp, toIcoDiv hp a b - 1, ?_⟩

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
tfae_3_to_2 : toIcoMod hp a b ≠ toIocMod hp a b → ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : toIcoMod hp a b + p = toIocMod hp a b → toIcoMod hp a b ≠ toIocMod hp a b
x✝ : toIcoMod hp a b = a
h : toIcoMod hp a b = a := x✝
⊢ b = a + p + (toIcoDiv hp a b - 1) • p
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ ¬a ≡ b [PMOD p] ↔ toIcoDiv hp a b = toIocDiv hp a b

Tactic:
not_modEq_iff_toIcoMod_eq_toIocMod hp,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a b = toIocMod hp a b ↔ toIcoDiv hp a b = toIocDiv hp a b
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case H.H.H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
z✝² z✝¹ z✝ : α
h₁₂₃ : btw ↑z✝² ↑z✝¹ ↑z✝
h₃₂₁ : btw ↑z✝² ↑z✝ ↑z✝¹
⊢ ↑z✝² = ↑z✝¹ ∨ ↑z✝¹ = ↑z✝ ∨ ↑z✝ = ↑z✝²

Tactic:
simp_rw [btw_coe_iff] at h₁₂₃ h₃₂₁

Goal state after:
case H.H.H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
z✝² z✝¹ z✝ : α
h₁₂₃ : toIcoMod ⋯ z✝² z✝¹ ≤ toIocMod ⋯ z✝² z✝
h₃₂₁ : toIcoMod ⋯ z✝² z✝ ≤ toIocMod ⋯ z✝² z✝¹
⊢ ↑z✝² = ↑z✝¹ ∨ ↑z✝¹ = ↑z✝ ∨ ↑z✝ = ↑z✝²
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
p : R
hp : 0 < p
a b : R
⊢ b - ↑(toIcoDiv hp a b) * p = toIcoMod hp a b

Tactic:
simpa using self_sub_toIcoDiv_zsmul hp a b

Goal state after:
Module: Mathlib.Topology.Maps.OpenQuotient

Goal state before:
pp: case mpr
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
⊢ (∃ x, IsOpen[inst✝¹] (q ⁻¹' q '' x) ∧ g ⁻¹' q '' x = U) → ∃ t, IsOpen[inst✝¹] t ∧ f ⁻¹' t = p ⁻¹' U

Tactic:
· rintro ⟨V, hV, rfl⟩
    refine ⟨_, hV, ?_⟩
    simp_rw [← Set.preimage_comp, h]

Goal state after:
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
⊢ HasSeparatingCover s t ∧ HasSeparatingCover t s → SeparatedNhds s t

pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
⊢ SeparatedNhds s t → HasSeparatingCover s t ∧ HasSeparatingCover t s

Tactic:
· rintro ⟨⟨u, u_cov, u_props⟩, ⟨v, v_cov, v_props⟩⟩
    have open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ n, IsOpen (u₀ n)) →
      IsOpen (⋃ n, u₀ n \ closure (a n)) := fun _ _ u₀i_open ↦
        isOpen_iUnion fun i ↦ (u₀i_open i).sdiff isClosed_closure
    have cover_lemma : ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
        (h₀ ⊆ ⋃ n, u₀ n) → (∀ n, Disjoint (closure (v₀ n)) h₀) →
        (h₀ ⊆ ⋃ n, u₀ n \ closure (⋃ m ≤ n, v₀ m)) :=
        fun h₀ u₀ v₀ h₀_cov dis x xinh ↦ by
      rcases h₀_cov xinh with ⟨un, ⟨n, rfl⟩, xinun⟩
      simp only [mem_iUnion]
      refine ⟨n, xinun, ?_⟩
      simp_all only [closure_iUnion₂_le_nat, disjoint_right, mem_iUnion,
        exists_false, not_false_eq_true]
    refine
      ⟨⋃ n : ℕ, u n \ (closure (⋃ m ≤ n, v m)),
       ⋃ n : ℕ, v n \ (closure (⋃ m ≤ n, u m)),
       open_lemma u (fun n ↦ ⋃ m ≤ n, v m) (fun n ↦ (u_props n).1),
       open_lemma v (fun n ↦ ⋃ m ≤ n, u m) (fun n ↦ (v_props n).1),
       cover_lemma s u v u_cov (fun n ↦ (v_props n).2),
       cover_lemma t v u v_cov (fun n ↦ (u_props n).2),
       ?_⟩
    rw [Set.disjoint_left]
    rintro x ⟨un, ⟨n, rfl⟩, xinun⟩
    suffices ∀ (m : ℕ), x ∈ v m → x ∈ closure (⋃ m' ∈ {m' | m' ≤ m}, u m') by simpa
    intro m xinvm
    have n_le_m : n ≤ m := by
      by_contra m_gt_n
      exact xinun.2 (subset_closure (mem_biUnion (le_of_lt (not_le.mp m_gt_n)) xinvm))
    exact subset_closure (mem_biUnion n_le_m xinun.1)

Goal state after:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
⊢ SeparatedNhds s t → HasSeparatingCover s t ∧ HasSeparatingCover t s
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
f : α → β
t₁ t₂ : TopologicalSpace α
t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₁
h₂ : t₁ ≤ induced f t₃
⊢ t₂ ≤ induced f t₃

Tactic:
exact le_trans h₁ h₂

Goal state after:
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
h : X ≃ₜ Y
f : Z → X
⊢ IsOpenMap (⇑h ∘ f) ↔ IsOpenMap f

Tactic:
by
  refine ⟨?_, fun hf => h.isOpenMap.comp hf⟩
  intro hf
  rw [← Function.id_comp f, ← h.symm_comp_self, Function.comp_assoc]
  exact h.symm.isOpenMap.comp hf

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
l : Filter α
x✝ : TopologicalSpace β
⊢ Continuous[nhdsAdjoint a l, x✝] f ↔ map f l ≤ (fun t ↦ 𝓝 (f a)) x✝

Tactic:
continuous_nhdsAdjoint_dom,

Goal state after:
α : Type u
β : Type v
f : α → β
a : α
l : Filter α
x✝ : TopologicalSpace β
⊢ Tendsto f l (𝓝 (f a)) ↔ map f l ≤ (fun t ↦ 𝓝 (f a)) x✝
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
x : α
⊢ t ∈ 𝓝[s] x ↔ s =ᶠ[𝓝 x] s ∩ t

Tactic:
by
  simp_rw [mem_nhdsWithin_iff_eventually, eventuallyEq_set, mem_inter_iff, iff_self_and]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: ι : Type u_5
X : ι → Type u_6
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : Finite ι
s : (i : ι) → Set (X i)
x : (i : ι) → X i
⊢ 𝓝[univ.pi s] x = ⨅ i, comap (fun x ↦ x i) (𝓝[s i] x i)

Tactic:
simpa [nhdsWithin] using nhdsWithin_pi_eq finite_univ s x

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
⊢ ClusterPt a (𝓟 J) ↔ ∃ᶠ (x : α) in 𝓝[t] ↑a, ∃ (h : x ∈ s), ⟨x, h⟩ ∈ J

Tactic:
rw [nhdsWithin_eq_map_subtype_coe (hst a.prop), Filter.frequently_map,
    clusterPt_principal_iff_frequently,
    Topology.IsInducing.subtypeVal.nhds_eq_comap, Filter.frequently_comap,
    Topology.IsInducing.subtypeVal.nhds_eq_comap, Filter.frequently_comap, Subtype.coe_mk]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
⊢ (∃ᶠ (b : α) in 𝓝 ↑a, ∃ a, ↑a = b ∧ a ∈ J) ↔ ∃ᶠ (b : α) in 𝓝 ↑a, ∃ a, ↑a = b ∧ ∃ (h : ↑a ∈ s), ⟨↑a, h⟩ ∈ J
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
p : X → Prop
f : Y → X
hf : IsOpenMap f
hp : ∀ (x : Y), p (f x)
u : Set Y
hu : IsOpen[inst✝] u
⊢ IsOpen[instTopologicalSpaceSubtype] ((fun x ↦ ⟨f x, ⋯⟩) '' u)

Tactic:
convert! (hf u hu).preimage continuous_subtype_val

Goal state after:
case e'_3
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
p : X → Prop
f : Y → X
hf : IsOpenMap f
hp : ∀ (x : Y), p (f x)
u : Set Y
hu : IsOpen[inst✝] u
⊢ (fun x ↦ ⟨f x, ⋯⟩) '' u = Subtype.val ⁻¹' f '' u
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
p : X → Prop
f : Y → X
hf : IsClosedMap f
hp : ∀ (x : Y), p (f x)
u : Set Y
hu : IsClosed[inst✝] u
⊢ IsClosed[instTopologicalSpaceSubtype] ((fun x ↦ ⟨f x, ⋯⟩) '' u)

Tactic:
convert! (hf u hu).preimage continuous_subtype_val

Goal state after:
case e'_3
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
p : X → Prop
f : Y → X
hf : IsClosedMap f
hp : ∀ (x : Y), p (f x)
u : Set Y
hu : IsClosed[inst✝] u
⊢ (fun x ↦ ⟨f x, ⋯⟩) '' u = Subtype.val ⁻¹' f '' u
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
r : Set (Set α)
hsg : t = generateFrom r
hsi : ∀ ⦃s : Set α⦄, s ∈ r → ∀ ⦃t : Set α⦄, t ∈ r → s ∩ t ∈ r
⊢ t = generateFrom (insert univ r)

Tactic:
by simpa using hsg

Goal state after:
Module: Mathlib.Topology.Bornology.Basic

Goal state before:
pp: α : Type u_2
x✝ : Bornology α
⊢ IsBounded ∅

Tactic:
rw [isBounded_def, compl_empty]
  exact univ_mem

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t✝ : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable ↑(t i)
a✝ : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
f : (I : Finset ι) × ((i : ↥I) → ↑(t ↑i)) → (i : ι) → X i :=
  fun x i ↦
    match x with
    | ⟨I, g⟩ => if hi : i ∈ I then ↑(g ⟨i, hi⟩) else default i
U : Set ((i : ι) → X i)
hU : IsOpen[Pi.topologicalSpace] U
x✝ : U.Nonempty
g : (i : ι) → X i
hg : g ∈ U
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst✝² a] (u a) ∧ g a ∈ u a
huU : (↑I).pi u ⊆ U
y : (i : ↥I) → ↑(t ↑i)
hyu : ∀ (i : ↥I), (fun i ↦ ↑(y i)) i ∈ u ↑i
i : ι
hi : i ∈ I
⊢ f ⟨I, y⟩ i ∈ u i

Tactic:
simp only [f, dif_pos hi]

Goal state after:
α : Type u
β : Type u_1
t✝ : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable ↑(t i)
a✝ : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
f : (I : Finset ι) × ((i : ↥I) → ↑(t ↑i)) → (i : ι) → X i :=
  fun x i ↦
    match x with
    | ⟨I, g⟩ => if hi : i ∈ I then ↑(g ⟨i, hi⟩) else default i
U : Set ((i : ι) → X i)
hU : IsOpen[Pi.topologicalSpace] U
x✝ : U.Nonempty
g : (i : ι) → X i
hg : g ∈ U
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst✝² a] (u a) ∧ g a ∈ u a
huU : (↑I).pi u ⊆ U
y : (i : ↥I) → ↑(t ↑i)
hyu : ∀ (i : ↥I), (fun i ↦ ↑(y i)) i ∈ u ↑i
i : ι
hi : i ∈ I
⊢ ↑(y ⟨i, ⋯⟩) ∈ u i
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
I : Set ι
s : (i : ι) → Set (A i)
a : (i : ι) → A i
hs : I.pi s ∈ 𝓝 a
i : ι
hi : i ∈ I
⊢ s i ∈ 𝓝 (a i)

Tactic:
by
  rw [nhds_pi] at hs; exact mem_of_pi_mem_pi hs hi

Goal state after:
Module: Mathlib.Topology.Compactness.LocallyCompact

Goal state before:
pp: case refine_2
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s✝ t✝ : Set X✝
X : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), LocallyCompactSpace (X i)
inst✝ : Finite ι
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
x✝ : (i : ι) → X i
h : x✝ ∈ univ.pi n''
⊢ x✝ ∈ s.pi n'

Tactic:
exact fun i _ => hsub' i (h i trivial)

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
⊢ ts = generateFrom (⋃ u ∈ s', f u)

Tactic:
· apply le_antisymm
    · apply le_generateFrom_iff_subset_isOpen.2
      simp only [iUnion_subset_iff]
      intro u hu v hv
      rw [ht]
      apply isOpen_generateFrom_of_mem
      exact ft u hu hv
    · rw [hs'.eq_generateFrom]
      apply le_generateFrom_iff_subset_isOpen.2
      intro u hu
      rw [← hf u hu, sInter_eq_biInter]
      change IsOpen[generateFrom _] (⋂ i ∈ f u, i)
      apply @Finite.isOpen_biInter _ _ (generateFrom (⋃ u ∈ s', f u)) _ _
      · apply f_fin u hu
      · intro i hi
        apply isOpen_generateFrom_of_mem
        simp
        grind

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case refine_1
X : Type u
inst✝ : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs✝ : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
t t' : Set X
ht : t ⊆ t'
hs : s ∈ 𝓝ˢ t' ×ˢ l
⊢ s ∈ 𝓝ˢ t ×ˢ l

pp: case refine_2
X : Type u
inst✝ : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
t t' : Set X
ht : s ∈ 𝓝ˢ t ×ˢ l
ht' : s ∈ 𝓝ˢ t' ×ˢ l
⊢ s ∈ 𝓝ˢ (t ∪ t') ×ˢ l

pp: case refine_3
X : Type u
inst✝ : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
x : X
hx : x ∈ K
⊢ ∃ t ∈ 𝓝[K] x, s ∈ 𝓝ˢ t ×ˢ l

Tactic:
· exact prod_mono (nhdsSet_mono ht) le_rfl hs

Goal state after:
case refine_2
X : Type u
inst✝ : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
t t' : Set X
ht : s ∈ 𝓝ˢ t ×ˢ l
ht' : s ∈ 𝓝ˢ t' ×ˢ l
⊢ s ∈ 𝓝ˢ (t ∪ t') ×ˢ l

case refine_3
X : Type u
inst✝ : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
x : X
hx : x ∈ K
⊢ ∃ t ∈ 𝓝[K] x, s ∈ 𝓝ˢ t ×ˢ l
Module: Mathlib.Order.UpperLower.Principal

Goal state before:
pp: α : Type u_1
ι : Sort u_3
inst✝ : CompleteLattice α
f : ι → α
c : α
⊢ c ∈ Ici (⨆ i, f i) ↔ c ∈ ⨆ i, Ici (f i)

Tactic:
simp only [mem_Ici_iff, mem_iSup_iff, iSup_le_iff]

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case refine_2
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : IsCompact (closure[inst✝] sᶜ)
⊢ ∃ i, (IsClosed[inst✝] i ∧ IsCompact i) ∧ iᶜ ⊆ s

Tactic:
· exact ⟨closure sᶜ, ⟨isClosed_closure, h⟩, compl_subset_comm.2 subset_closure⟩

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : Bornology Y
s : Set X
hs : IsCompact s
f : X → Y
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x ∧ IsBounded (f '' U x)
I : Finset X
hI : (∀ x ∈ I, x ∈ s) ∧ s ⊆ ⋃ x ∈ I, U x
⊢ f '' ⋃ x ∈ I, U x = ⋃ x ∈ I, f '' U x

Tactic:
simp [Set.image_iUnion₂]

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
f : Ultrafilter (X × Y)
⊢ s ×ˢ t ∈ f → ∃ x ∈ s ×ˢ t, ↑f ≤ 𝓝 x

Tactic:
hfs

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
⊢ ∃ x ∈ s ×ˢ t, ↑f ≤ 𝓝 x
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
h : ∀ (i : ι) (f : Ultrafilter (X i)), s i ∈ ↑f → ∃ x ∈ s i, ↑f ≤ 𝓝 x
f : Ultrafilter ((i : ι) → X i)
⊢ {x | ∀ (i : ι), x i ∈ s i} ∈ ↑f → ∃ x ∈ {x | ∀ (i : ι), x i ∈ s i}, ∀ (i : ι), Tendsto (eval i) (↑f) (𝓝 (x i))

Tactic:
hfs

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
h : ∀ (i : ι) (f : Ultrafilter (X i)), s i ∈ ↑f → ∃ x ∈ s i, ↑f ≤ 𝓝 x
f : Ultrafilter ((i : ι) → X i)
hfs : {x | ∀ (i : ι), x i ∈ s i} ∈ ↑f
⊢ ∃ x ∈ {x | ∀ (i : ι), x i ∈ s i}, ∀ (i : ι), Tendsto (eval i) (↑f) (𝓝 (x i))
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
s : Set X
hs : T0Space ↑s
x y : { x // x ∈ s }
hxy : Inseparable ↑x ↑y
⊢ ↑x = ↑y

Tactic:
← subtype_inseparable_iff

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
s : Set X
hs : T0Space ↑s
x y : { x // x ∈ s }
hxy : Inseparable x y
⊢ ↑x = ↑y
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
t : Set X
ht : IsIrreducible t
f : Y → X
hf₂ : IsOpenMap f
hf₃ : ∀ (x : X), IsPreirreducible (f ⁻¹' {x})
h : (t ∩ range f).Nonempty
⊢ IsIrreducible (f ⁻¹' t)

Tactic:
refine ⟨?_, IsPreirreducible.preimage_of_isPreirreducible_fiber ht.2 f hf₂ hf₃⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
t : Set X
ht : IsIrreducible t
f : Y → X
hf₂ : IsOpenMap f
hf₃ : ∀ (x : X), IsPreirreducible (f ⁻¹' {x})
h : (t ∩ range f).Nonempty
⊢ (f ⁻¹' t).Nonempty
Module: Mathlib.Topology.Order.LeftRight

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
a : α
⊢ 𝓝[Iic a ∪ Ici a] a = 𝓝 a

Tactic:
Iic_union_Ici,

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
a : α
⊢ 𝓝[univ] a = 𝓝 a
Module: Mathlib.Topology.Order.LeftRight

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
s : Set α
a : α
⊢ 𝓝[s ∩ (Iic a ∪ Ici a)] a = 𝓝[s] a

Tactic:
Iic_union_Ici,

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
s : Set α
a : α
⊢ 𝓝[s ∩ univ] a = 𝓝[s] a
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
p : X
s : Set X
hs : Disjoint (𝓝[s] p) cofinite
t : Set X
h₁t : t ∈ 𝓝[s] p
h₂t : t.Finite
S : Set X := {y | y ∈ t ∩ s ∧ ¬y ⤳ p}
hS_nhds : ∀ y ∈ S, (closure[inst✝] {y})ᶜ ∈ 𝓝 p
x : X
hxt : x ∈ t
hxS : x ∈ ⋂ i ∈ S, (closure[inst✝] {i})ᶜ
⊢ x ∈ s → x ⤳ p

Tactic:
contrapose

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
p : X
s : Set X
hs : Disjoint (𝓝[s] p) cofinite
t : Set X
h₁t : t ∈ 𝓝[s] p
h₂t : t.Finite
S : Set X := ⋯
hS_nhds : ∀ y ∈ S, (closure[inst✝] {y})ᶜ ∈ 𝓝 p
x : X
hxt : x ∈ t
hxS : x ∈ ⋂ i ∈ S, (closure[inst✝] {i})ᶜ
⊢ ¬x ⤳ p → x ∉ s
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
A : {x} ⊆ s
B : IsClosed[inst✝¹] (s \ {x})
C : (s \ {x})ᶜ ∈ 𝓝 x
D : x ∈ interior {x}
⊢ IsOpen[inst✝¹] {x}

Tactic:
← singleton_subset_iff,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
A : {x} ⊆ s
B : IsClosed[inst✝¹] (s \ {x})
C : (s \ {x})ᶜ ∈ 𝓝 x
D : {x} ⊆ interior {x}
⊢ IsOpen[inst✝¹] {x}
Module: Mathlib.Topology.Clopen

Goal state before:
pp: case refine_1
X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hab : s ∩ a ∩ b = ∅
⊢ s ⊆ s ∩ a ∪ s ∩ b

pp: case refine_2
X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hab : s ∩ a ∩ b = ∅
⊢ Disjoint (s ∩ a) (s ∩ b)

Tactic:
· rw [← inter_union_distrib_left]
    exact subset_inter .rfl cover

Goal state after:
case refine_2
X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hab : s ∩ a ∩ b = ∅
⊢ Disjoint (s ∩ a) (s ∩ b)