mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Constructions

Goal state before:
pp: case basic.inr
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P s✝ : Set α
h✝ : s✝ ∈ S
⊢ s✝ ∈ S ∨ ∃ Q ∈ S, s✝ = A ∩ Q

Tactic:
exact Or.inl (by assumption)

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

Goal state before:
pp: case e'_2
n : ℕ
⊢ ∑ m ∈ range n.succ with m ∣ n, φ m = n.divisors.sum φ

Tactic:
simp only [Nat.divisors, sum_filter, range_eq_Ico]

Goal state after:
case e'_2
n : ℕ
⊢ (∑ a ∈ Ico 0 n.succ, if a ∣ n then φ a else 0) = ∑ a ∈ Ico 1 (n + 1), if a ∣ n then φ a else 0
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
⊢ #(range (p ^ (n + 1)) \ image (fun x ↦ x * p) (range (p ^ n))) = p ^ n * (p - 1)

Tactic:
have h1 : Function.Injective (· * p) := mul_left_injective₀ hp.ne_zero
      have h2 : (range (p ^ n)).image (· * p) ⊆ range (p ^ (n + 1)) := fun a => by
        simp only [mem_image, mem_range, exists_imp]
        rintro b ⟨h, rfl⟩
        rw [Nat.pow_succ]
        exact (mul_lt_mul_iff_left₀ hp.pos).2 h
      rw [card_sdiff_of_subset h2, Finset.card_image_of_injective _ h1, card_range, card_range, ←
        one_mul (p ^ n), pow_succ', ← tsub_mul, one_mul, mul_comm]

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

Goal state before:
pp: ⊢ φ 0 = 1 ↔ 0 = 1 ∨ 0 = 2

Tactic:
by simp

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

Goal state before:
pp: ⊢ φ 1 = 1 ↔ 1 = 1 ∨ 1 = 2

Tactic:
by simp

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

Goal state before:
pp: ⊢ φ 2 = 1 ↔ 2 = 1 ∨ 2 = 2

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder γ
f g : α → γ
hf : Tendsto f atBot atBot
hg : Tendsto g atBot atBot
⊢ Tendsto (Prod.map f g) atBot atBot

Tactic:
by
  rw [← prod_atBot_atBot_eq]
  exact hf.prod_map_prod_atBot hg

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

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
p : ℕ
hp : 0 < n.factorization p
⊢ p * p ^ (n.factorization p - 1) * (p - 1) = p ^ n.factorization p * (p - 1)

Tactic:
← pow_succ',

Goal state after:
case neg
n : ℕ
hn : ¬n = 0
p : ℕ
hp : 0 < n.factorization p
⊢ p ^ (n.factorization p - 1).succ * (p - 1) = p ^ n.factorization p * (p - 1)
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : atBot.IsCountablyGenerated
inst✝¹ : Preorder β
inst✝ : atBot.IsCountablyGenerated
⊢ atBot.IsCountablyGenerated

Tactic:
rw [← prod_atBot_atBot_eq]
  infer_instance

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

Goal state before:
pp: p n : ℕ
hp : Prime p
h : p ∣ n
⊢ φ (p * n) = p * φ n

Tactic:
have h1 := totient_gcd_mul_totient_mul p n

Goal state after:
p n : ℕ
hp : Prime p
h : p ∣ n
h1 : φ (p.gcd n) * φ (p * n) = φ p * φ n * p.gcd n
⊢ φ (p * n) = p * φ n
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case pos
a b : ℕ
h : a ∣ b
h' : φ b = 0
ha : a = 0
⊢ a = b ∨ 2 * a = b

Tactic:
totient_eq_zero

Goal state after:
case pos
a b : ℕ
h : a ∣ b
h' : b = 0
ha : a = 0
⊢ a = b ∨ 2 * a = b
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case pos
a b : ℕ
h : a ∣ b
h' : φ a = 0
ha : ¬a = 0
hb : b = 0
⊢ a = b ∨ 2 * a = b

Tactic:
totient_eq_zero

Goal state after:
case pos
a b : ℕ
h : a ∣ b
h' : a = 0
ha : ¬a = 0
hb : b = 0
⊢ a = b ∨ 2 * a = b
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case pos
a b : ℕ
h : a ∣ b
ha : Even a
h' : φ b = 0
ha' : a = 0
⊢ a = b

Tactic:
totient_eq_zero

Goal state after:
case pos
a b : ℕ
h : a ∣ b
ha : Even a
h' : b = 0
ha' : a = 0
⊢ a = b
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a b : ℕ
h : a ∣ b
ha : Even a
h' : φ a = φ b
⊢ a = b

Tactic:
by
  by_cases ha' : a = 0
  · rw [ha', totient_zero, eq_comm, totient_eq_zero] at h'
    rw [h', ha']
  refine (eq_or_eq_of_totient_eq_totient h h').resolve_right fun h ↦ ?_
  rw [← h, totient_mul_of_prime_of_dvd (prime_two) (even_iff_two_dvd.mp ha), eq_comm,
    mul_eq_right (totient_eq_zero.not.mpr ha')] at h'
  lia

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 : α
⊢ a = a + 0 • p

Tactic:
by simp

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 : α
⊢ a = a + p + -1 • p

Tactic:
by simp

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 : α
⊢ a + p = a + 1 • p

Tactic:
by simp

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 : α
⊢ a + p = a + p + 0 • p

Tactic:
by simp

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

Goal state before:
pp: case refine_1
α : Type u_1
γ : Type u_3
ι : Sort u_6
p : ι → Prop
s✝ : ι → Set α
f : Filter α
hf : f.HasBasis p s✝
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), (g (s✝ i)).HasBasis (pg i) (sg i)
gm : Monotone g
s : Set γ
⊢ DirectedOn (g ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) f.sets

pp: case refine_2
α : Type u_1
γ : Type u_3
ι : Sort u_6
p : ι → Prop
s✝ : ι → Set α
f : Filter α
hf : f.HasBasis p s✝
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), (g (s✝ i)).HasBasis (pg i) (sg i)
gm : Monotone g
s : Set γ
⊢ (∃ i ∈ f.sets, s ∈ g i) ↔ ∃ i, p i ∧ ∃ x, pg i x ∧ sg i x ⊆ s

Tactic:
· intro t₁ ht₁ t₂ ht₂
    exact ⟨t₁ ∩ t₂, inter_mem ht₁ ht₂, gm inter_subset_left, gm inter_subset_right⟩

Goal state after:
case refine_2
α : Type u_1
γ : Type u_3
ι : Sort u_6
p : ι → Prop
s✝ : ι → Set α
f : Filter α
hf : f.HasBasis p s✝
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), (g (s✝ i)).HasBasis (pg i) (sg i)
gm : Monotone g
s : Set γ
⊢ (∃ i ∈ f.sets, s ∈ g i) ↔ ∃ i, p i ∧ ∃ x, pg i x ∧ sg i x ⊆ s
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ interior s = (closure sᶜ)ᶜ

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
p : X → Prop
⊢ (∀ (i : Set X), x ∈ i ∧ IsOpen[inst✝] i → ∃ x ∈ i, p x) ↔ ∀ (U : Set X), x ∈ U → IsOpen[inst✝] U → ∃ y ∈ U, p y

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
p : X → Prop
⊢ (∃ᶠ (x' : X) in 𝓝 x, ∃ᶠ (x'' : X) in 𝓝 x', p x'') ↔ ∃ᶠ (x : X) in 𝓝 x, p x

Tactic:
rw [← not_iff_not]
  simp only [not_frequently, eventually_eventually_nhds]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ s \ (closure s \ interior s) = interior s

Tactic:
sdiff_sdiff_right,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ s \ closure s ∪ s ∩ interior s = interior s
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)
⊢ l ≤ comap f (𝓝 x)

Tactic:
have := sup_le h' h

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)
this : l ⊓ 𝓟 s ⊔ 𝓟 sᶜ ≤ comap f (𝓝 x)
⊢ l ≤ comap f (𝓝 x)
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 : α
⊢ toIocDiv hp a b • p ≤ toIcoDiv hp a b • p

Tactic:
exact zsmul_left_mono hp.le (toIocDiv_wcovBy_toIcoDiv _ _ _).le

Goal state after:
Module: Mathlib.Topology.Continuous

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : X ≃ Y
⊢ Continuous[inst✝, inst✝¹] ⇑e.symm ↔ IsOpenMap ⇑e

Tactic:
by
  simp_rw [continuous_def, ← Equiv.image_eq_preimage_symm, IsOpenMap]

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 : α
⊢ b = b + 0 • p

Tactic:
by simp

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
x₁ x₂ x₃ : α
h✝ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
h₃₁ : x₃' ≤ x₁ + p
⊢ x₁ = x₁ + p + -1 • p

Tactic:
by simp

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
x₁ x₂ x₃ : α
h✝ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
h₁₃ : x₁ + p < x₃'
⊢ x₃' = x₃' - p + 1 • p

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
U : Set X
hU : U ∈ F.lift' closure[inst✝]
h : ∀ (s : Set X), (∃ t₁ ∈ pure x, ∃ t₂ ∈ F.lift' closure[inst✝], s = t₁ ∩ t₂) → s.Nonempty
⊢ {x} ∈ pure x

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ a < b - -↑⌊(a + p - b) / p⌋ * p ∧ b - -↑⌊(a + p - b) / p⌋ * p ≤ a + p

Tactic:
neg_mul,

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ a < b - -(↑⌊(a + p - b) / p⌋ * p) ∧ b - -(↑⌊(a + p - b) / p⌋ * p) ≤ a + p
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
⊢ s ∈ 𝓝ˢ ∅

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ a + p - b < p + ↑⌊(a + p - b) / p⌋ * p

Tactic:
←
    sub_lt_iff_lt_add

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ a + p - b - ↑⌊(a + p - b) / p⌋ * p < p
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
h : IsClosed[inst✝] t
⊢ 𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ (s ∩ tᶜ) ≤ 𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ tᶜ

Tactic:
by nth_grw 2 [inter_subset_right]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
s : Set α
f : α → β
⊢ IsClosed[TopologicalSpace.induced f t] s ↔ ∃ t_1, IsClosed[t] t_1 ∧ f ⁻¹' t_1 = s

Tactic:
let := t.induced f
  simp only [← isOpen_compl_iff, isOpen_induced_iff]
  exact compl_surjective.exists.trans (by simp only [preimage_compl, compl_inj_iff])

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
⊢ range ⇑h = univ

Tactic:
by simp

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ (∀ (x : Set Y), IsOpen[inst✝¹] (f ⁻¹' xᶜ) ↔ IsOpen[inst✝] xᶜ) ↔
    ∀ (s : Set Y), IsClosed[inst✝¹] (f ⁻¹' s) ↔ IsClosed[inst✝] s

Tactic:
by simp

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 : Y → Z
x : X
⊢ range ⇑h ∈ 𝓝 (h x)

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Order

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

Tactic:
rw [continuous_iff_coinduced_le] at h₂ ⊢
  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
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
x : X
⊢ range ⇑h ∈ 𝓝 (h x)

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
l : Filter α
p : α → Prop
⊢ Tendsto p l (𝓝 True) ↔ ∀ᶠ (x : α) in l, p x

Tactic:
by simp

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
W : Type u_3
Z✝ : Type u_4
Z : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : DiscreteTopology X
inst✝ : DiscreteTopology Y
e : X ≃ Y
⊢ ∀ (s : Set Y), IsOpen[inst✝⁴] (⇑e ⁻¹' s) ↔ IsOpen[inst✝³] s

Tactic:
by simp

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenMap f
x : X
l : Filter Y
h : ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
⊢ 𝓟 (f ⁻¹' {f x})ᶜ ≤ 𝓟 {x}ᶜ

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X✝ : Type u
Y✝ : Type v
W : Type u_1
Z✝ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z✝
inst✝² : TopologicalSpace W
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
X : Type ?u.28
Y : Type ?u.32
Z : Type ?u.36
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
⊢ Sort ?u.37

Tactic:
by haveI := ta2; haveI := tb2; exact Continuous fun p : X × Y => f p.1 p.2

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsClosedEmbedding f
s : Set X
h : IsClosed[inst✝] (f '' s)
⊢ IsClosed[inst✝¹] (f ⁻¹' f '' s)

Tactic:
exact h.preimage hf.continuous

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
b : α
I₁ I₂ : Set α
h : univ = I₁ ∪ I₂
L : Set α
hL : L ∈ 𝓝[I₁] b
R : Set α
hR : R ∈ 𝓝[I₂] b
⊢ L ⊆ L ∪ R

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
b : α
I₁ I₂ : Set α
h : univ = I₁ ∪ I₂
L : Set α
hL : L ∈ 𝓝[I₁] b
R : Set α
hR : R ∈ 𝓝[I₂] b
⊢ R ⊆ L ∪ R

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X✝ : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
X : Type u_5
⊢ univ.Nonempty → univᶜ.Finite

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst✝¹] s
h : ∀ (t : Set β), IsOpen[inst✝] t → ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ ∀ (t : Set β), IsOpen[inst✝] t → IsOpen[inst✝¹] (s ∩ f ⁻¹' t)

Tactic:
t

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst✝¹] s
h : ∀ (t : Set β), IsOpen[inst✝] t → ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s
t : Set β
⊢ IsOpen[inst✝] t → IsOpen[inst✝¹] (s ∩ f ⁻¹' t)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst✝¹] s
h : ∀ (t : Set β), IsOpen[inst✝] t → IsOpen[inst✝¹] (s ∩ f ⁻¹' t)
⊢ ∀ (t : Set β), IsOpen[inst✝] t → ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
t

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst✝¹] s
h : ∀ (t : Set β), IsOpen[inst✝] t → IsOpen[inst✝¹] (s ∩ f ⁻¹' t)
t : Set β
⊢ IsOpen[inst✝] t → ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
x : α
h : ¬AccPt x ⊤
hh : AccPt x (𝓟 {x}ᶜ)
⊢ 𝓟 {x}ᶜ ≤ ⊤

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hs : ∀ (a : X), f a ∈ s
hf : ∀ (s_1 : Set ↑s), IsOpen[instTopologicalSpaceSubtype] s_1 → IsOpen[inst✝¹] (codRestrict f s hs ⁻¹' s_1)
⊢ ∀ (s : Set Y), IsOpen[inst✝] s → IsOpen[inst✝¹] (f ⁻¹' s)

Tactic:
t

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hs : ∀ (a : X), f a ∈ s
hf : ∀ (s_1 : Set ↑s), IsOpen[instTopologicalSpaceSubtype] s_1 → IsOpen[inst✝¹] (codRestrict f s hs ⁻¹' s_1)
t : Set Y
⊢ IsOpen[inst✝] t → IsOpen[inst✝¹] (f ⁻¹' t)
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t : TopologicalSpace α
s : Set α
inst✝ : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
h : ∀ t_1 ∈ B, ∃ u, IsOpen[t] u ∧ f ⁻¹' t_1 ∩ s = u ∩ s
ι : Type u_1
g : ι → Set β
hg : ∀ (i : ι), g i ∈ B
ht : IsOpen[inst✝] (⋃ i, g i)
v : ι → Set α
hv : ∀ (i : ι), IsOpen[t] (v i)
he : ∀ (i : ι), f ⁻¹' g i ∩ s = v i ∩ s
⊢ (f ⁻¹' ⋃ i, g i) ∩ s = (⋃ i, v i) ∩ s

Tactic:
simp_all [iUnion_inter]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : β → γ
hg : IsInducing g
s : Set α
⊢ (∀ x ∈ s, ContinuousWithinAt f s x) ↔ ∀ x ∈ s, ContinuousWithinAt (g ∘ f) s x

Tactic:
hg.continuousWithinAt_iff

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
h : IsEmpty α
⊢ ∀ t₁ ∈ ∅, ∀ t₂ ∈ ∅, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ ∅, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
h : IsEmpty α
⊢ ∀ t₁ ∈ {∅}, ∀ t₂ ∈ {∅}, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ {∅}, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: case succ
α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
n m : ℕ
hm : accumulate s n ⊆ s m
k : ℕ
hk : s m ⊆ s k ∧ s (n + 1) ⊆ s k
⊢ ∃ m, accumulate s (n + 1) ⊆ s m

Tactic:
exact ⟨k, by simp; grind⟩

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_2.refine_1
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I).pi t ⊆ s
i : ι
⊢ ∃ t_1 ⊆ (fun a ↦ if a ∈ I then t a else univ) i, IsOpen[T i] t_1 ∧ a i ∈ t_1

Tactic:
by_cases hi : i ∈ I

Goal state after:
case pos
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I).pi t ⊆ s
i : ι
hi : i ∈ I
⊢ ∃ t_1 ⊆ (fun a ↦ if a ∈ I then t a else univ) i, IsOpen[T i] t_1 ∧ a i ∈ t_1

case neg
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I).pi t ⊆ s
i : ι
hi : i ∉ I
⊢ ∃ t_1 ⊆ (fun a ↦ if a ∈ I then t a else univ) i, IsOpen[T i] t_1 ∧ a i ∈ t_1
Module: Mathlib.Topology.Bornology.Basic

Goal state before:
pp: α : Type u_2
t t' : Bornology α
h_cobounded : cobounded α = cobounded α
⊢ t = t'

Tactic:
cases t

Goal state after:
case mk
α : Type u_2
t' : Bornology α
cobounded✝ : Filter α
le_cofinite✝ : cobounded✝ ≤ cofinite
h_cobounded : cobounded α = cobounded α
⊢ { cobounded := cobounded✝, le_cofinite := le_cofinite✝ } = t'
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s s' : Set α
t : Set β
hf : ContinuousOn f s'
hs' : s' ∈ 𝓝ˢ s
hst : MapsTo f s t
V : Set α
hV : IsOpen[inst✝¹] V
hsV : s ⊆ V
hVs' : V ⊆ s'
U : Set β
hU : IsOpen[inst✝] U ∧ t ⊆ U
x✝ : α
⊢ x✝ ∈ V ∩ f ⁻¹' U → f x✝ ∈ U

Tactic:
intro h
    rw [← mem_preimage]
    exact mem_of_mem_inter_right h

Goal state after:
Module: Mathlib.Topology.Constructions

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

Tactic:
rw [pi_def, biInter_mem hi]
  exact fun a ha => (continuous_apply a).continuousAt (hs a ha)

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst✝ i] (c i)
this : ∀ (i : ι), Countable ↑(c i)
g : (I : Finset ι) × ((i : ↥I) → ↑(c ↑i)) → (i : ι) → X i :=
  fun x i ↦
    match x with
    | ⟨I, f⟩ => if hi : i ∈ I then ↑(f ⟨i, hi⟩) else f₀ i
f : (i : ι) → X i
hf : f ∈ univ.pi s
o : Set ((i : ι) → X i)
ho : IsOpen[Pi.topologicalSpace] o
hfo : f ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst✝ a] (u a) ∧ f a ∈ u a
hI : (↑I).pi u ⊆ o
H : ∀ i ∈ I, (u i ∩ c i).Nonempty
⊢ ∃ f, g ⟨I, f⟩ ∈ (↑I).pi u

Tactic:
choose f hfu hfc using H
      refine ⟨fun i ↦ ⟨f i i.2, hfc i i.2⟩, fun i (hi : i ∈ I) ↦ ?_⟩
      simpa only [g, dif_pos hi] using hfu i hi

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
hs : IsSeparable s
f : α → β
hf : Continuous[t, inst✝] f
⊢ IsSeparable (f '' s)

Tactic:
by
  rcases hs with ⟨c, c_count, hc⟩
  refine ⟨f '' c, c_count.image _, ?_⟩
  rw [image_subset_iff]
  exact hc.trans (closure_subset_preimage_closure_image hf)

Goal state after:
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
f g : Ultrafilter α
s✝ t : Set α
p q : α → Prop
α✝ : Type ?u.21
a : α✝
s : Set α✝
⊢ sᶜ ∉ pure a ↔ s ∈ pure a

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case intro.refine_2
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
⊢ ∀ s ∈ {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s},
    IsOpen[generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}] s

Tactic:
· rintro s ⟨t, i, ht, rfl⟩
    let := generateFrom { t | ∃ s : ∀ a, Set (X a), (∀ a, s a ∈ g a) ∧ t = pi univ s }
    refine isOpen_iff_forall_mem_open.2 fun f hf => ?_
    choose c hcg hfc using fun a => sUnion_eq_univ_iff.1 (hg a) (f a)
    refine ⟨pi i t ∩ pi ((↑i)ᶜ : Set ι) c, inter_subset_left, ?_, ⟨hf, fun a _ => hfc a⟩⟩
    classical
    rw [← univ_pi_piecewise]
    refine GenerateOpen.basic _ ⟨_, fun a => ?_, rfl⟩
    by_cases a ∈ i <;> simp [*]

Goal state after: