mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case mp
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ ⇑(ConcreteCategory.hom (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) '' Set.range Sum.inl =
    (⇑(ConcreteCategory.hom (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) '' Set.range Sum.inr)ᶜ

Tactic:
← dsimp% [Iso.toEquiv] Set.image_compl_eq
          (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).symm.toEquiv.bijective

Goal state after:
case mp
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ ⇑(ConcreteCategory.hom (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) '' Set.range Sum.inl =
    ⇑(ConcreteCategory.hom (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) '' (Set.range Sum.inr)ᶜ
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
inst✝ : HasColimitsOfShape F.Elementsᵒᵖ (Type w)
u : F.Elements
⊢ (ConcreteCategory.hom ((shrinkYonedaCompWhiskeringLeftObjπCompColimIso F).inv.app u.fst)) u.snd =
    (ConcreteCategory.hom (colimit.ι ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj u.fst) (op u)))
      (shrinkYonedaObjObjEquiv.symm (𝟙 (unop ((CategoryOfElements.π F).op.obj (op u)))))

Tactic:
have :
      (coconeπOpCompShrinkYonedaObj F u.fst).ι.app (op u) ≫
        (shrinkYonedaCompWhiskeringLeftObjπCompColimIso F).inv.app u.fst =
      colimit.ι ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w}.obj u.fst) (op u) :=
    IsColimit.comp_coconePointUniqueUpToIso_inv (colimit.isColimit _) _ (op u)
  simpa using ConcreteCategory.congr_hom this (shrinkYonedaObjObjEquiv.symm (𝟙 _))

Goal state after:
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
⊢ Periodic f (n • 2 • c)

Tactic:
two_zsmul,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
⊢ Periodic f (n • (c + c))
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddMonoid α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
k : ℕ
⊢ f (x + (2 * k + 1) • c) = (-1) ^ (2 * k + 1) • f x

Tactic:
rw [h.odd_nsmul_antiperiodic]

Goal state after:
case inr
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddMonoid α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
k : ℕ
⊢ -f x = (-1) ^ (2 * k + 1) • f x
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: case neg.refine_1
a✝ b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
ha1 : ¬a = 1
⊢ 1 < a

Tactic:
contrapose! hpa
      simp [lt_one_iff.1 (lt_of_le_of_ne hpa ha1)]

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

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

Tactic:
exact prime_mul _ _ hp ih

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

Goal state before:
pp: R✝ : Type u
inst✝⁷ : Ring R✝
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R✝ Q
R : Type u
inst✝⁴ : Ring R
ι : Type w
M : ι → Type v
inst✝³ : Small.{v, u} R
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), Injective R (M i)
X Y : Type (max v w)
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
g : X →ₗ[R] (i : ι) → M i
l : (i : ι) → Y →ₗ[R] M i
hl : ∀ (i : ι), l i ∘ₗ f = LinearMap.proj i ∘ₗ g
⊢ ∃ h, ∀ (x : X), h (f x) = g x

Tactic:
refine ⟨LinearMap.pi l, fun x ↦ ?_⟩

Goal state after:
R✝ : Type u
inst✝⁷ : Ring R✝
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R✝ Q
R : Type u
inst✝⁴ : Ring R
ι : Type w
M : ι → Type v
inst✝³ : Small.{v, u} R
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), Injective R (M i)
X Y : Type (max v w)
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
g : X →ₗ[R] (i : ι) → M i
l : (i : ι) → Y →ₗ[R] M i
hl : ∀ (i : ι), l i ∘ₗ f = LinearMap.proj i ∘ₗ g
x : X
⊢ (LinearMap.pi l) (f x) = g x
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R✝ : Type u
inst✝⁷ : Ring R✝
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R✝ Q
R : Type u
inst✝⁴ : Ring R
ι : Type w
M : ι → Type v
inst✝³ : Small.{v, u} R
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), Injective R (M i)
X Y : Type (max v w)
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
g : X →ₗ[R] (i : ι) → M i
l : (i : ι) → Y →ₗ[R] M i
hl : ∀ (i : ι), l i ∘ₗ f = LinearMap.proj i ∘ₗ g
x : X
i : ι
⊢ (LinearMap.pi l) (f x) i = g x i

Tactic:
exact DFunLike.congr_fun (hl i) x

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

Goal state before:
pp: case pos
n : ℕ
hn : n = 0
⊢ φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)

Tactic:
simp [hn]

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

Goal state before:
pp: case pos
n : ℕ
hn : n = 0
⊢ ↑(φ n) = ↑n * ∏ p ∈ n.primeFactors, (1 - (↑p)⁻¹)

Tactic:
simp [hn]

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

Goal state before:
pp: n : ℕ
hn : ¬n = 0
⊢ ↑n ≠ 0

Tactic:
simp [hn]

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

Goal state before:
pp: case refine_2
α : 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✝ : ι
s₁✝ s₂✝ : Set α
hs : s₁✝ ∈ f i✝
ht : ⨅ i, (f i).lift g ≤ g s₂✝
⊢ ⨅ i, (f i).lift g ≤ g s₁✝ ⊓ g s₂✝

Tactic:
exact le_inf (iInf₂_le_of_le _ _ <| iInf_le _ hs) ht

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
⊢ toIcoMod hp a c + toIcoDiv hp a c • p - (toIcoMod hp a b + toIcoDiv hp a b • p) =
    (toIcoDiv hp a c - toIcoDiv hp a b) • p

Tactic:
rw [h, sub_smul]

Goal state after:
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
⊢ toIcoMod hp a c + toIcoDiv hp a c • p - (toIcoMod hp a c + toIcoDiv hp a b • p) =
    toIcoDiv hp a c • p - toIcoDiv hp a b • p
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 : toIocMod hp a b = toIocMod hp a c
⊢ toIocMod hp a c + toIocDiv hp a c • p - (toIocMod hp a b + toIocDiv hp a b • p) =
    (toIocDiv hp a c - toIocDiv hp a b) • p

Tactic:
rw [h, sub_smul]

Goal state after:
case refine_1
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : toIocMod hp a b = toIocMod hp a c
⊢ toIocMod hp a c + toIocDiv hp a c • p - (toIocMod hp a c + toIocDiv hp a b • p) =
    toIocDiv hp a c • p - toIocDiv hp a b • p
Module: Mathlib.Topology.Closure

Goal state before:
pp: case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ Dense {x}ᶜ → ¬IsOpen {x}

pp: case mpr
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ ¬IsOpen {x} → Dense {x}ᶜ

Tactic:
· intro hd ho
    exact (hd.inter_open_nonempty _ ho (singleton_nonempty _)).ne_empty (inter_compl_self _)

Goal state after:
case mpr
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ ¬IsOpen {x} → Dense {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 : α
⊢ toIocMod hp a b = b ↔ b ∈ Set.Ioc a (a + p)

Tactic:
by
  rw [toIocMod_eq_iff, and_iff_left]
  exact ⟨0, 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₃
⊢ toIcoMod hp x₂ x₃ ≤ toIocMod hp x₂ x₁

Tactic:
let x₂' := toIcoMod hp x₁ x₂

Goal state after:
α : 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₂
⊢ toIcoMod hp x₂ x₃ ≤ toIocMod hp x₂ x₁
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
f : Filter X
⊢ IsClosed[inst✝] {x | ClusterPt x f}

Tactic:
by
  simp only [clusterPt_iff_forall_mem_closure, ofPred_forall]
  exact isClosed_biInter fun _ _ ↦ isClosed_closure

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 c : α
n : ℤ
hp' : Fact (0 < p)
x₁ x₂ x₃ : α ⧸ AddSubgroup.zmultiples p
h : btw x₁ x₂ x₃
⊢ btw x₂ x₃ x₁

Tactic:
induction x₁ using QuotientAddGroup.induction_on

Goal state after:
case H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
x₂ x₃ : α ⧸ AddSubgroup.zmultiples p
z✝ : α
h : btw (↑z✝) x₂ x₃
⊢ btw x₂ x₃ ↑z✝
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 c : α
n : ℤ
hp' : Fact (0 < p)
x₁ x₂ x₃ x₄ : α ⧸ AddSubgroup.zmultiples p
h₁₂₃ : btw x₁ x₂ x₃ ∧ ¬btw x₃ x₂ x₁
h₂₃₄ : btw x₂ x₄ x₃ ∧ ¬btw x₃ x₄ x₂
⊢ btw x₁ x₄ x₃ ∧ ¬btw x₃ x₄ x₁

Tactic:
induction x₁ using QuotientAddGroup.induction_on

Goal state after:
case H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
x₂ x₃ x₄ : α ⧸ AddSubgroup.zmultiples p
h₂₃₄ : btw x₂ x₄ x₃ ∧ ¬btw x₃ x₄ x₂
z✝ : α
h₁₂₃ : btw (↑z✝) x₂ x₃ ∧ ¬btw x₃ x₂ ↑z✝
⊢ btw (↑z✝) x₄ x₃ ∧ ¬btw x₃ x₄ ↑z✝
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 c : α
n : ℤ
hp' : Fact (0 < p)
x₁ x₂ x₃ : α ⧸ AddSubgroup.zmultiples p
h₁₂₃ : btw x₁ x₂ x₃
h₃₂₁ : btw x₃ x₂ x₁
⊢ x₁ = x₂ ∨ x₂ = x₃ ∨ x₃ = x₁

Tactic:
induction x₁ using QuotientAddGroup.induction_on

Goal state after:
case H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
x₂ x₃ : α ⧸ AddSubgroup.zmultiples p
z✝ : α
h₁₂₃ : btw (↑z✝) x₂ x₃
h₃₂₁ : btw x₃ x₂ ↑z✝
⊢ ↑z✝ = x₂ ∨ x₂ = x₃ ∨ x₃ = ↑z✝
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 c : α
n : ℤ
hp' : Fact (0 < p)
x₁ x₂ x₃ : α ⧸ AddSubgroup.zmultiples p
⊢ btw x₁ x₂ x₃ ∨ btw x₃ x₂ x₁

Tactic:
induction x₁ using QuotientAddGroup.induction_on

Goal state after:
case H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
x₂ x₃ : α ⧸ AddSubgroup.zmultiples p
z✝ : α
⊢ btw (↑z✝) x₂ x₃ ∨ btw x₃ x₂ ↑z✝
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
V : Set B
hV : IsOpen[inst✝¹] (q ⁻¹' q '' V)
⊢ f ⁻¹' q ⁻¹' q '' V = p ⁻¹' g ⁻¹' q '' V

Tactic:
← Set.preimage_comp,

Goal state after:
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
V : Set B
hV : IsOpen[inst✝¹] (q ⁻¹' q '' V)
⊢ q ∘ f ⁻¹' q '' V = g ∘ p ⁻¹' q '' V
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ n, u n
u_props : ∀ (n : ℕ), IsOpen[inst✝] (u n) ∧ Disjoint (closure[inst✝] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ n, v n
v_props : ∀ (n : ℕ), IsOpen[inst✝] (v n) ∧ Disjoint (closure[inst✝] (v n)) s
open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst✝] (u₀ n)) → IsOpen[inst✝] (⋃ n, u₀ n \ closure[inst✝] (a n))
⊢ SeparatedNhds s t

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

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ n, u n
u_props : ∀ (n : ℕ), IsOpen[inst✝] (u n) ∧ Disjoint (closure[inst✝] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ n, v n
v_props : ∀ (n : ℕ), IsOpen[inst✝] (v n) ∧ Disjoint (closure[inst✝] (v n)) s
open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst✝] (u₀ n)) → IsOpen[inst✝] (⋃ n, u₀ n \ closure[inst✝] (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ n, u₀ n →
      (∀ (n : ℕ), Disjoint (closure[inst✝] (v₀ n)) h₀) → h₀ ⊆ ⋃ n, u₀ n \ closure[inst✝] (⋃ m, ⋃ (_ : m ≤ n), v₀ m)
⊢ SeparatedNhds s t
Module: Mathlib.Topology.Order

Goal state before:
pp: case inl
α : Type u
inst✝ : DecidableEq α
l : Filter α
b a : α
s : Set α
h : pure a ≤ l
hs : s ∈ update pure a l a
⊢ ∀ᶠ (y : α) in update pure a l a, s ∈ update pure a l y

pp: case inr
α : Type u
inst✝ : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b a : α
s : Set α
hs : s ∈ update pure a₀ l a
ha : a ≠ a₀
⊢ ∀ᶠ (y : α) in update pure a₀ l a, s ∈ update pure a₀ l y

Tactic:
· filter_upwards [hs] with b hb
    rcases eq_or_ne b a with (rfl | hb)
    · exact hs
    · rwa [update_of_ne hb]

Goal state after:
case inr
α : Type u
inst✝ : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b a : α
s : Set α
hs : s ∈ update pure a₀ l a
ha : a ≠ a₀
⊢ ∀ᶠ (y : α) in update pure a₀ l a, s ∈ update pure a₀ l y
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
s : Set X
⊢ ⇑h '' frontier s = frontier (⇑h '' s)

Tactic:
by
  rw [← preimage_symm, preimage_frontier]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝[univ] a = 𝓝 a

Tactic:
by
  rw [nhdsWithin, principal_univ, inf_top_eq]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
p : X × Y → Prop
x : X
y : Y
h : ∀ᶠ (x : X × Y) in 𝓝 (x, y), p x
⊢ ∀ᶠ (x' : X) in 𝓝 x, ∀ᶠ (y' : Y) in 𝓝 y, p (x', y')

Tactic:
rw [nhds_prod_eq] at h
  exact h.curry

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
ι : Type u_5
Y : ι → Type v
inst✝ : (i : ι) → TopologicalSpace (Y i)
h : ∀ (i : ι), IndiscreteTopology (Y i)
x✝ : ι
⊢ induced (fun f ↦ f x✝) (inst✝ x✝) = ⊤

Tactic:
by simp only [(h _).eq_top, induced_top]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
s : Set (CofiniteTopology X)
⊢ (WithTopology.toTopology
            { IsOpen := fun s ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ } ⁻¹'
          s).Nonempty →
      (WithTopology.toTopology
              { IsOpen := fun s ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ } ⁻¹'
            s)ᶜ.Finite ↔
    s.Nonempty → sᶜ.Finite

Tactic:
← Set.preimage_compl,

Goal state after:
X : Type u
s : Set (CofiniteTopology X)
⊢ (WithTopology.toTopology
            { IsOpen := fun s ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ } ⁻¹'
          s).Nonempty →
      (WithTopology.toTopology
            { IsOpen := fun s ↦ s.Nonempty → sᶜ.Finite, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ } ⁻¹'
          sᶜ).Finite ↔
    s.Nonempty → sᶜ.Finite
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
s : Set (CofiniteTopology X)
⊢ (WithTopology.ofTopology '' s).Nonempty → (WithTopology.ofTopology '' sᶜ).Finite ↔ s.Nonempty → sᶜ.Finite

Tactic:
image_nonempty,

Goal state after:
X : Type u
s : Set (CofiniteTopology X)
⊢ s.Nonempty → (WithTopology.ofTopology '' sᶜ).Finite ↔ s.Nonempty → sᶜ.Finite
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case mpr
X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
⊢ U ∈ pure x ⊔ cofinite → ∃ t ⊆ U, (t.Nonempty → tᶜ.Finite) ∧ x ∈ t

Tactic:
rintro ⟨hU : x ∈ U, hU' : Uᶜ.Finite⟩
    exact ⟨U, Subset.rfl, fun _ => hU', hU⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set (Set α)
hsg : t = generateFrom s
hsi : FiniteInter s
g : Set (Set α)
hg : g.Finite
hgs : g ⊆ s
⊢ (fun f ↦ ⋂₀ f) g ∈ s

Tactic:
lift g to Finset (Set α) using hg

Goal state after:
α : Type u
t : TopologicalSpace α
s : Set (Set α)
hsg : t = generateFrom s
hsi : FiniteInter s
g : Finset (Set α)
hgs : ↑g ⊆ s
⊢ (fun f ↦ ⋂₀ f) ↑g ∈ s
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: case mp
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
hf₁ : IsInducing f
hg₁ : IsInducing g
hFg : Disjoint (closure[inst✝] (range f)) (range g)
hfG : Disjoint (range f) (closure[inst✝] (range g))
hf₂ : Injective f
hg₂ : Injective g
f_ne_g : ∀ (a : X) (b : Y), f a ≠ g b
⊢ (IsInducing f ∧ Injective f) ∧
    (IsInducing g ∧ Injective g) ∧
      Disjoint (closure[inst✝] (range f)) (range g) ∧ Disjoint (range f) (closure[inst✝] (range g))

Tactic:
exact ⟨⟨hf₁, hf₂⟩, ⟨hg₁, hg₂⟩, hFg, hfG⟩

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
⊢ (U ∩ range f).Nonempty

Tactic:
refine ⟨f ⟨I, y⟩, huU fun i (hi : i ∈ I) ↦ ?_, mem_range_self (f := f) ⟨I, y⟩⟩

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
⊢ f ⟨I, y⟩ i ∈ u i
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s u : Set α
hs : IsSeparable s
hu : u ⊆ s
⊢ IsSeparable u

Tactic:
rcases hs with ⟨c, c_count, hs⟩
  exact ⟨c, c_count, hu.trans hs⟩

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

Goal state before:
pp: α : Type u
g : Filter α
p : Filter α → Prop
hp : Monotone p
H : ∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f
f : Filter α
hf : f.NeBot
⊢ f ≤ g → p f

Tactic:
hfg

Goal state after:
α : Type u
g : Filter α
p : Filter α → Prop
hp : Monotone p
H : ∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f
f : Filter α
hf : f.NeBot
hfg : f ≤ g
⊢ p f
Module: Mathlib.Topology.Compactness.LocallyCompact

Goal state before:
pp: 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✝ : ∀ (i : ι), CompactSpace (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
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)
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s

Tactic:
refine ⟨s.pi n'', ?_, subset_trans (fun _ => ?_) hsub, ?_⟩

Goal state after:
case refine_1
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✝ : ∀ (i : ι), CompactSpace (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
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)
⊢ s.pi n'' ∈ 𝓝 t

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✝ : ∀ (i : ι), CompactSpace (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
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
⊢ x✝ ∈ s.pi n'' → x✝ ∈ s.pi n'

case refine_3
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✝ : ∀ (i : ι), CompactSpace (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
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)
⊢ IsCompact (s.pi n'')