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
⊢ Injective
      ⇑(ConcreteCategory.hom
          ((binaryCoproductCocone X Y).ι.app { as := left } ≫
            (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) ∧
    Injective
        ⇑(ConcreteCategory.hom
            ((binaryCoproductCocone X Y).ι.app { as := right } ≫
              (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) ∧
      IsCompl
        (Set.range
          ⇑(ConcreteCategory.hom
              ((binaryCoproductCocone X Y).ι.app { as := left } ≫
                (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)))
        (Set.range
          ⇑(ConcreteCategory.hom
              ((binaryCoproductCocone X Y).ι.app { as := right } ≫
                (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)))

Tactic:
dsimp [binaryCoproductCocone]

Goal state after:
case mp
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ Injective ⇑(ConcreteCategory.hom (↾Sum.inl ≫ (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) ∧
    Injective ⇑(ConcreteCategory.hom (↾Sum.inr ≫ (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) ∧
      IsCompl
        (Set.range ⇑(ConcreteCategory.hom (↾Sum.inl ≫ (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)))
        (Set.range ⇑(ConcreteCategory.hom (↾Sum.inr ≫ (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)))
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: A : Type u_1
inst✝ : AddCommGroup A
H : ∀ {n : ℤ}, n ≠ 0 → n • ⊤ = ⊤
a : A
n : ℤ
hn : ¬n = 0
⊢ a ∈ n • ⊤

Tactic:
rw [H hn]; trivial

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℤ
⊢ ↑↑n.negOnePow = (-1) ^ n.natAbs

Tactic:
cases n with

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b c d : α
⊢ a < b ∧ b < c ∨ b < c ∧ c < a ∨ c < a ∧ a < b →
    b < d ∧ d < c ∨ d < c ∧ c < b ∨ c < b ∧ b < d → a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

Tactic:
rintro (⟨hab, hbc⟩ | ⟨hbc, hca⟩ | ⟨hca, hab⟩) (⟨hbd, hdc⟩ | ⟨hdc, hcb⟩ | ⟨hcb, hbd⟩)

Goal state after:
case inl.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hbd : b < d
hdc : d < c
⊢ a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

case inl.inr.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hdc : d < c
hcb : c < b
⊢ a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

case inl.inr.inr
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hcb : c < b
hbd : b < d
⊢ a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

case inr.inl.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hbd : b < d
hdc : d < c
⊢ a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

case inr.inl.inr.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hdc : d < c
hcb : c < b
⊢ a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

case inr.inl.inr.inr
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hcb : c < b
hbd : b < d
⊢ a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

case inr.inr.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hbd : b < d
hdc : d < c
⊢ a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

case inr.inr.inr.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hdc : d < c
hcb : c < b
⊢ a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

case inr.inr.inr.inr
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst✝ : AddGroup α
h1 : Periodic f c₁
h2 : Periodic f c₂
x : α
⊢ f (x + (c₁ + -c₂)) = f x

Tactic:
← add_assoc,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst✝ : AddGroup α
h1 : Periodic f c₁
h2 : Periodic f c₂
x : α
⊢ f (x + c₁ + -c₂) = f x
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddMonoid α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℕ
x : α
⊢ f (x + ((2 * n) • c + c)) = -f x

Tactic:
← add_assoc,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddMonoid α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℕ
x : α
⊢ f (x + (2 * n) • c + c) = -f x
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : NonAssocSemiring α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℕ
x : α
⊢ f (x + (↑n * (2 * c) + c)) = -f x

Tactic:
← add_assoc,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : NonAssocSemiring α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℕ
x : α
⊢ f (x + ↑n * (2 * c) + c) = -f x
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 : ℤ
x : α
⊢ f (x + ((2 * n) • c + c)) = -f x

Tactic:
← add_assoc,

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : NonAssocRing α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
x : α
⊢ f (x + (↑n * (2 * c) + c)) = -f x

Tactic:
← add_assoc,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : NonAssocRing α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
x : α
⊢ f (x + ↑n * (2 * c) + c) = -f 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
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
a b : ExtensionOf i f
domain_eq : a.domain = b.domain
to_fun_eq : ∀ ⦃x : N⦄ ⦃ha : x ∈ a.domain⦄ ⦃hb : x ∈ b.domain⦄, ↑a.toLinearPMap ⟨x, ha⟩ = ↑b.toLinearPMap ⟨x, hb⟩
⊢ a = b

Tactic:
by
  rcases a with ⟨a, a_le, e1⟩
  congr
  exact LinearPMap.ext domain_eq to_fun_eq

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
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑x = ↑⟨a, ha⟩ + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 :
  (extendIdealTo i f h y) r =
    ↑(extensionOfMax i f).toLinearPMap ⟨r • y - snd i x • y, ⋯⟩ + (extendIdealTo i f h y) (snd i x)
⊢ ↑(extensionOfMax i f).toLinearPMap (fst i x) + (extendIdealTo i f h y) (snd i x) =
    ↑(extensionOfMax i f).toLinearPMap ⟨a, ha⟩ +
      (↑(extensionOfMax i f).toLinearPMap ⟨r • y - snd i x • y, ⋯⟩ + (extendIdealTo i f h y) (snd i x))

Tactic:
← add_assoc,

Goal state after:
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑x = ↑⟨a, ha⟩ + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 :
  (extendIdealTo i f h y) r =
    ↑(extensionOfMax i f).toLinearPMap ⟨r • y - snd i x • y, ⋯⟩ + (extendIdealTo i f h y) (snd i x)
⊢ ↑(extensionOfMax i f).toLinearPMap (fst i x) + (extendIdealTo i f h y) (snd i x) =
    ↑(extensionOfMax i f).toLinearPMap ⟨a, ha⟩ + ↑(extensionOfMax i f).toLinearPMap ⟨r • y - snd i x • y, ⋯⟩ +
      (extendIdealTo i f h y) (snd i x)
Module: Mathlib.Data.Nat.Cast.Field

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : DivisionSemiring K
d m n : ℕ
inst✝ : CharZero K
hn : d ∣ n
hm : d ∣ m
hd : ↑d ≠ 0
⊢ ↑m / ↑d / ↑(n / d) = ↑m / ↑n

pp: case inr
K : Type u_1
inst✝¹ : DivisionSemiring K
d m n : ℕ
inst✝ : CharZero K
hn : d ∣ n
hm : d ∣ m
hd : ↑d ≠ 0
⊢ ↑d ≠ 0

Tactic:
cast_div hn,

Goal state after:
case inr
K : Type u_1
inst✝¹ : DivisionSemiring K
d m n : ℕ
inst✝ : CharZero K
hn : d ∣ n
hm : d ∣ m
hd : ↑d ≠ 0
⊢ ↑m / ↑d / (↑n / ↑d) = ↑m / ↑n

case inr
K : Type u_1
inst✝¹ : DivisionSemiring K
d m n : ℕ
inst✝ : CharZero K
hn : d ∣ n
hm : d ∣ m
hd : ↑d ≠ 0
⊢ ↑d ≠ 0

case inr
K : Type u_1
inst✝¹ : DivisionSemiring K
d m n : ℕ
inst✝ : CharZero K
hn : d ∣ n
hm : d ∣ m
hd : ↑d ≠ 0
⊢ ↑d ≠ 0
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case a
hp : 0 < 1
h : 1 = 1 - 1
⊢ False

Tactic:
tsub_self

Goal state after:
case a
hp : 0 < 1
h : 1 = 0
⊢ False
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 - 0 • p ∈ Set.Ico a (a + p)

Tactic:
by simp [hp]

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 - -1 • p ∈ Set.Ioc a (a + p)

Tactic:
by simp [hp]

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 - 1 • p ∈ Set.Ico a (a + p)

Tactic:
by simp [hp]

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 - 0 • p ∈ Set.Ioc a (a + p)

Tactic:
by simp [hp]

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]

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

Tactic:
add_neg_cancel,

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 + toIcoDiv hp a b • p + 0
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsCoinducing g
hf : IsCoinducing f
⊢ inst✝ = coinduced (g ∘ f) inst✝²

Tactic:
hg.eq_coinduced,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsCoinducing g
hf : IsCoinducing f
⊢ coinduced g inst✝¹ = coinduced (g ∘ f) inst✝²
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 : IsCoinducing f
hf' : Injective f
⊢ IsOpenMap f

Tactic:
intro s hs
  rwa [← hf.isOpen_preimage, preimage_image_eq _ hf']

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 : IsOpenEmbedding f
x : X
l : Filter Y
⊢ ClusterPt x (𝓟 (f ⁻¹' {f x})ᶜ ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)

Tactic:
← preimage_compl,

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenEmbedding f
x : X
l : Filter Y
⊢ ClusterPt x (𝓟 (f ⁻¹' {f x}ᶜ) ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x : α
s t : Set α
hs : s ∈ 𝓝[t] x
t' : Set α
⊢ s ∩ t'ᶜ ∈ 𝓝 x ⊓ (𝓟 t ⊓ 𝓟 t'ᶜ)

Tactic:
← inf_assoc

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
s t : Set α
hs : s ∈ 𝓝[t] x
t' : Set α
⊢ s ∩ t'ᶜ ∈ 𝓝 x ⊓ 𝓟 t ⊓ 𝓟 t'ᶜ
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
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : DiscreteTopology X
hY : DiscreteTopology Y
⊢ coinduced inl inst✝¹ = ⊥ ∧ coinduced inr inst✝ = ⊥

Tactic:
by simp [h.eq_bot, hY.eq_bot]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
this :
  ∀ (t : Set β),
    IsOpen[instTopologicalSpaceSubtype] (s.domRestrict f ⁻¹' t) ↔ ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ Continuous[instTopologicalSpaceSubtype, inst✝] (s.domRestrict f) ↔
    ∀ (t : Set β), IsOpen[inst✝] t → ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
continuous_def

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
this :
  ∀ (t : Set β),
    IsOpen[instTopologicalSpaceSubtype] (s.domRestrict f ⁻¹' t) ↔ ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ (∀ (s_1 : Set β), IsOpen[inst✝] s_1 → IsOpen[instTopologicalSpaceSubtype] (s.domRestrict f ⁻¹' s_1)) ↔
    ∀ (t : Set β), IsOpen[inst✝] t → ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
α : Type u_5
β : Type u_6
f : α → X
g : β → Y
la : Filter α
lb : Filter β
x : X
y : Y
hf : ∀ s ∈ 𝓝 x, ∃ᶠ (a : α) in la, f a ∈ s
hg : ∀ s ∈ 𝓝 y, ∃ᶠ (a : β) in lb, g a ∈ s
⊢ MapClusterPt (x, y) (la.curry lb) (Prod.map f g)

Tactic:
((𝓝 x).basis_sets.prod_nhds (𝓝 y).basis_sets).mapClusterPt_iff_frequently

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
α : Type u_5
β : Type u_6
f : α → X
g : β → Y
la : Filter α
lb : Filter β
x : X
y : Y
hf : ∀ s ∈ 𝓝 x, ∃ᶠ (a : α) in la, f a ∈ s
hg : ∀ s ∈ 𝓝 y, ∃ᶠ (a : β) in lb, g a ∈ s
⊢ ∀ (i : Set X × Set Y), i.1 ∈ 𝓝 x ∧ i.2 ∈ 𝓝 y → ∃ᶠ (a : α × β) in la.curry lb, Prod.map f g a ∈ id i.1 ×ˢ id i.2
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsInducing f
hg : IsInducing g
x✝ : X × Z
x : X
z : Z
⊢ comap f (𝓝 (f x)) ×ˢ comap g (𝓝 (g z)) = comap (fun p ↦ (f p.1, g p.2)) (𝓝 (f x) ×ˢ 𝓝 (g z))

Tactic:
prod_comap_comap_eq

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
f : X → Bool
b : Bool
⊢ IsOpen[inst✝] (f ⁻¹' {b}) ∧ IsOpen[inst✝] (f ⁻¹' {!b}) ↔ IsOpen[inst✝] (f ⁻¹' {b})ᶜ ∧ IsOpen[inst✝] (f ⁻¹' {b})

Tactic:
← preimage_compl,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
f : X → Bool
b : Bool
⊢ IsOpen[inst✝] (f ⁻¹' {b}) ∧ IsOpen[inst✝] (f ⁻¹' {!b}) ↔ IsOpen[inst✝] (f ⁻¹' {b}ᶜ) ∧ IsOpen[inst✝] (f ⁻¹' {b})
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → β
s s₁ : Set α
h : ContinuousOn f s
h' : EqOn g f s₁
h₁ : s₁ ⊆ s
⊢ ContinuousOn g s₁

Tactic:
intro x hx
  unfold ContinuousWithinAt
  have A := (h x (h₁ hx)).mono h₁
  unfold ContinuousWithinAt at A
  rw [← h' hx] at A
  exact A.congr' h'.eventuallyEq_nhdsWithin.symm

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
⊢ Continuous[inst✝¹, instTopologicalSpaceSubtype] (codRestrict f s hs) → Continuous[inst✝¹, inst✝] f

Tactic:
continuous_def

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
⊢ (∀ (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)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hst : s ⊆ t
hs : IsOpen[instTopologicalSpaceSubtype] (t ↓∩ s)
⊢ IsOpen[instTopologicalSpaceSubtype] (range (inclusion hst))

Tactic:
range_inclusion

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hst : s ⊆ t
hs : IsOpen[instTopologicalSpaceSubtype] (t ↓∩ s)
⊢ IsOpen[instTopologicalSpaceSubtype] {x | ↑x ∈ s}
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hst : s ⊆ t
hs : IsClosed[instTopologicalSpaceSubtype] (t ↓∩ s)
⊢ IsClosed[instTopologicalSpaceSubtype] (range (inclusion hst))

Tactic:
range_inclusion

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hst : s ⊆ t
hs : IsClosed[instTopologicalSpaceSubtype] (t ↓∩ s)
⊢ IsClosed[instTopologicalSpaceSubtype] {x | ↑x ∈ s}
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hfs : ContinuousOn f s
hft : ContinuousOn f t
hs : IsClosed[inst✝¹] s
ht : IsClosed[inst✝¹] t
x : α
hx : x ∈ s ∪ t
⊢ ContinuousWithinAt f s x

Tactic:
refine if hx : x ∈ s then hfs x hx else continuousWithinAt_of_notMem_closure ?_
    rwa [hs.closure_eq]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
⊢ IsInducing f ↔
    (∀ (i : ι), IsInducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i

Tactic:
refine ⟨fun h ↦ ⟨fun i ↦ h.comp IsEmbedding.sigmaMk.1, fun i ↦ ?_⟩, ?_⟩
  · rcases h.isOpen_iff.1 (isOpen_range_sigmaMk (i := i)) with ⟨U, hUo, hU⟩
    refine ⟨U, hUo, ?_⟩
    simpa [Set.ext_iff] using hU
  · refine fun ⟨h₁, h₂⟩ ↦ isInducing_iff_nhds.2 fun ⟨i, x⟩ ↦ ?_
    rw [Sigma.nhds_mk, (h₁ i).nhds_eq_comap, comp_apply, ← comap_comap, map_comap_of_mem]
    rcases h₂ i with ⟨U, hUo, hU⟩
    filter_upwards [preimage_mem_comap <| hUo.mem_nhds <| (hU _).2 rfl] with y hy
    simpa [hU] using hy

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t✝] u
a : α → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
⊢ ∃ T, T.Countable ∧ ⋃ i ∈ T, a ↑i = ⋃ i, a ↑i

Tactic:
apply isOpen_iUnion_countable _

Goal state after:
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t✝] u
a : α → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
⊢ ∀ (i : ↑u), IsOpen[t✝] (a ↑i)
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: X : Type u_4
inst✝ : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), {i | ((fun n ↦ {x | f (n + 1) x ≠ f n x}) i ∩ U x).Nonempty}.Finite
N : X → ℕ
hN : ∀ (x : X), ∀ n ≥ N x + 1, ∀ y ∈ U x, f n y = f (N x + 1) y
⊢ ∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.1 p.2 = F p.2

Tactic:
refine ⟨fun x => f (N x + 1) x, fun x => ?_⟩

Goal state after:
X : Type u_4
inst✝ : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), {i | ((fun n ↦ {x | f (n + 1) x ≠ f n x}) i ∩ U x).Nonempty}.Finite
N : X → ℕ
hN : ∀ (x : X), ∀ n ≥ N x + 1, ∀ y ∈ U x, f n y = f (N x + 1) y
x : X
⊢ ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.1 p.2 = (fun x ↦ f (N x + 1) x) p.2
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : UpperSet α
a : α
ha : a ∈ s
has : ∀ b ∈ s, b ≤ a → b = a
⊢ s.erase a ⊓ Ici a = s

Tactic:
rw [← upperClosure_singleton, ← sdiff_singleton, sdiff_inf_upperClosure] <;> simpa

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
f : Filter Y
hs : IsCompact s
hf : Disjoint f (cocompact Y)
⊢ 𝓝ˢ s ×ˢ f ≤ 𝓝ˢ (s ×ˢ univ)

Tactic:
obtain ⟨K, hKf, hK⟩ := (disjoint_cocompact_right f).mp hf

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : Filter Y
hs : IsCompact s
hf : Disjoint f (cocompact Y)
K : Set Y
hKf : K ∈ f
hK : IsCompact K
⊢ 𝓝ˢ s ×ˢ f ≤ 𝓝ˢ (s ×ˢ univ)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
t : Set Y
f : Filter X
ht : IsCompact t
hf : Disjoint f (cocompact X)
⊢ f ×ˢ 𝓝ˢ t ≤ 𝓝ˢ (univ ×ˢ t)

Tactic:
obtain ⟨K, hKf, hK⟩ := (disjoint_cocompact_right f).mp hf

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
t : Set Y
f : Filter X
ht : IsCompact t
hf : Disjoint f (cocompact X)
K : Set X
hKf : K ∈ f
hK : IsCompact K
⊢ f ×ˢ 𝓝ˢ t ≤ 𝓝ˢ (univ ×ˢ t)
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ ¬x ⤳ y ↔ ∃ S, IsOpen[inst✝] S ∧ y ∈ S ∧ x ∉ S

Tactic:
by
  rw [specializes_iff_forall_open]
  push Not
  rfl

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s : Set X
f g : X → Y
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : IsOpen[inst✝²] s
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝², inst✝¹] g
hspec : ∀ (x : X), f x ⤳ g x
this : ∀ (U : Set Y), IsOpen[inst✝¹] U → g ⁻¹' U ⊆ f ⁻¹' U
⊢ Continuous[inst✝², inst✝¹] (s.piecewise f g)

Tactic:
continuous_def

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s : Set X
f g : X → Y
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : IsOpen[inst✝²] s
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝², inst✝¹] g
hspec : ∀ (x : X), f x ⤳ g x
this : ∀ (U : Set Y), IsOpen[inst✝¹] U → g ⁻¹' U ⊆ f ⁻¹' U
⊢ ∀ (s_1 : Set Y), IsOpen[inst✝¹] s_1 → IsOpen[inst✝²] (s.piecewise f g ⁻¹' s_1)
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
⊢ T0Space X ↔ Pairwise fun x y ↦ ¬Inseparable x y

Tactic:
by
  simp only [t0Space_iff_inseparable, Ne, not_imp_not, Pairwise]

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

Goal state before:
pp: case inl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
p : X → Prop
a : X
ha : a ∈ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}
hb : ∀ᶠ (x : X) in 𝓝[≠] a, p x
⊢ ∀ᶠ (y : X) in 𝓝[≠] a, p y

Tactic:
exact hb

Goal state after: