mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ Epi (imageToKernel' S.f S.g ⋯) ↔ Epi (imageToKernel S.f S.g ⋯)

Tactic:
apply (MorphismProperty.epimorphisms C).arrow_mk_iso_iff

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ Arrow.mk (imageToKernel' S.f S.g ⋯) ≅ Arrow.mk (imageToKernel S.f S.g ⋯)
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesMonomorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
φ : { X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := ⋯ }.map L ⟶ S.map L := ⋯
⊢ ({ X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := ⋯ }.map L).Exact

Tactic:
apply ShortComplex.exact_of_g_is_cokernel

Goal state after:
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesMonomorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
φ : { X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := ⋯ }.map L ⟶ S.map L := ⋯
⊢ IsColimit
    (CokernelCofork.ofπ
      ({ X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := ⋯ }.map L).g ⋯)
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteCoproducts C
f : α → C
inst✝¹ : HasColimitsOfShape (Finset (Discrete α)) C
inst✝ : HasCoproduct f
⊢ ∀ (j : Finset (Discrete α)),
    (colimit.cocone (liftToFinsetObj (Discrete.functor f))).ι.app j ≫
        ((liftToFinsetColimitCocone (Discrete.functor f)).isColimit.coconePointUniqueUpToIso
            (colimit.isColimit (Discrete.functor f))).hom =
      (finiteSubcoproductsCocone f).ι.app j

Tactic:
by
    intro S
    simp only [liftToFinsetObj_obj, Discrete.functor_obj_eq_as, finiteSubcoproductsCocone_pt,
      colimit.cocone_x, colimit.cocone_ι, finiteSubcoproductsCocone_ι_app]
    ext j
    rw [← Category.assoc]
    convert!
      IsColimit.comp_coconePointUniqueUpToIso_hom
        (liftToFinsetColimitCocone (Discrete.functor f)).isColimit (colimit.isColimit _) j
    · simp [← colimit.w (liftToFinsetObj _) (homOfLE (x := {j.1}) (y := S) (by simp))]
    · simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
X : StructuredArrow Y L
eq₁ : f₁.left.app (L.obj X.right) ≫ (CostructuredArrow.hom E).app X.right = (CostructuredArrow.hom G).app X.right
eq₂ : f₂.left.app (L.obj X.right) ≫ (CostructuredArrow.hom E).app X.right = (CostructuredArrow.hom G).app X.right
⊢ f₁.left.app Y ≫ (CostructuredArrow.left E).map X.hom ≫ (CostructuredArrow.hom E).app X.right =
    f₂.left.app Y ≫ (CostructuredArrow.left E).map X.hom ≫ (CostructuredArrow.hom E).app X.right

Tactic:
simp only [← NatTrans.naturality_assoc, eq₁, eq₂]

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : ObjectProperty C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
this : IsIso (P.ofLE Q h₁)
⊢ P = Q

Tactic:
by exact le_antisymm h₁ (le_of_comm (inv (ofLE _ _ h₁)) (by simp))

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : Cᵒᵖ
⊢ IsDetector (unop G) ↔ IsCodetector G

Tactic:
rw [IsDetector, IsCodetector, ← isDetecting_unop_iff, unop_singleton]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: X : Type u
Y : AddCommGrpCat
⊢ (free.obj X ⟶ Y) ≃ (X ⟶ (forget AddCommGrpCat).obj Y)

Tactic:
refine ConcreteCategory.homEquiv.trans (Equiv.trans ?_ TypeCat.homEquiv.symm)
        exact FreeAbelianGroup.lift.symm

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: case inl
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : x < y
⊢ Nonempty ↑(Ico x (x + dx) \ Ico y (y + dy))

pp: case inr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : y ≤ x
⊢ Nonempty ↑(Ico x (x + dx) \ Ico y (y + dy))

Tactic:
· use x
    simp [*, not_le.2 h']

Goal state after:
case inr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : y ≤ x
⊢ Nonempty ↑(Ico x (x + dx) \ Ico y (y + dy))
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
a b : ↥(supExtensionOfMaxSingleton i f y)
eq1 :
  ↑a + ↑b =
    ↑(ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) +
      (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) • y
⊢ ↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) +
      (ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) =
    ExtensionOfMaxAdjoin.extensionToFun i f h a + ExtensionOfMaxAdjoin.extensionToFun i f h b

Tactic:
LinearPMap.map_add,

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
a b : ↥(supExtensionOfMaxSingleton i f y)
eq1 :
  ↑a + ↑b =
    ↑(ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) +
      (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) • y
⊢ ↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i a) +
        ↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i b) +
      (ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) =
    ExtensionOfMaxAdjoin.extensionToFun i f h a + ExtensionOfMaxAdjoin.extensionToFun i f h b
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ ∀ {n : ℕ}, n ≠ 0 → f n = n.factorization.prod fun p k ↦ f (p ^ k)

Tactic:
apply Nat.recOnPosPrimePosCoprime

Goal state after:
case prime_pow
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ ∀ (p n : ℕ), Prime p → 0 < n → p ^ n ≠ 0 → f (p ^ n) = (p ^ n).factorization.prod fun p k ↦ f (p ^ k)

case zero
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ 0 ≠ 0 → f 0 = (factorization 0).prod fun p k ↦ f (p ^ k)

case one
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ 1 ≠ 0 → f 1 = (factorization 1).prod fun p k ↦ f (p ^ k)

case coprime
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ ∀ (a b : ℕ),
    1 < a →
      1 < b →
        a.Coprime b →
          (a ≠ 0 → f a = a.factorization.prod fun p k ↦ f (p ^ k)) →
            (b ≠ 0 → f b = b.factorization.prod fun p k ↦ f (p ^ k)) →
              a * b ≠ 0 → f (a * b) = (a * b).factorization.prod fun p k ↦ f (p ^ k)
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
h : Baer R Q
X Y : Type v
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
i : X →ₗ[R] Y
hi : Function.Injective ⇑i
f : X →ₗ[R] Q
⊢ ∃ h, ∀ (x : X), h (i x) = f x

Tactic:
obtain ⟨h, H⟩ := Module.Baer.extension_property h i hi f
    exact ⟨h, DFunLike.congr_fun H⟩

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
⊢ ∃ h, ∀ (x : X), h (f x) = g x

Tactic:
choose l hl using fun i ↦ extension_property R _ _ _ f hf ((LinearMap.proj i).comp g)
    refine ⟨LinearMap.pi l, fun x ↦ ?_⟩
    ext i
    exact DFunLike.congr_fun (hl i) x

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

Goal state before:
pp: α : Type u_3
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
p : α × α → Prop
⊢ (∀ᶠ (x : α × α) in atTop, p x) ↔ ∃ a, ∀ k ≥ a, ∀ l ≥ a, p (k, l)

Tactic:
simp only [eventually_atTop_prod_self, forall_cond_comm]

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

Goal state before:
pp: case mp
m n : ℕ
⊢ (φ m).Coprime (φ n) → (m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2

Tactic:
rw [← not_imp_not]
    simp_rw [← odd_totient_iff, not_or, not_odd_iff_even, even_iff_two_dvd]
    exact fun h ↦ Nat.not_coprime_of_dvd_of_dvd one_lt_two h.1 h.2

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:
← mul_assoc,

Goal state after:
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)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ a.gcd b *
      (a * b / ((∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p) *
        ((∏ p ∈ a.primeFactors, (p - 1)) * ∏ p ∈ b.primeFactors, (p - 1))) =
    a.gcd b * (a * b) / ((∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p) *
      ((∏ p ∈ a.primeFactors, (p - 1)) * ∏ p ∈ b.primeFactors, (p - 1))

Tactic:
← mul_assoc,

Goal state after:
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ a.gcd b * (a * b / ((∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p)) *
      ((∏ p ∈ a.primeFactors, (p - 1)) * ∏ p ∈ b.primeFactors, (p - 1)) =
    a.gcd b * (a * b) / ((∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p) *
      ((∏ p ∈ a.primeFactors, (p - 1)) * ∏ p ∈ b.primeFactors, (p - 1))
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
this : φ a < φ (p * a * d)
⊢ False

Tactic:
← mul_assoc,

Goal state after:
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * p * d)
hb : ¬a * (p * d) = 0
this : φ a < φ (p * a * d)
⊢ 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 < a + p ∧ ∃ z, a = a + p + z • p

Tactic:
exact ⟨lt_add_of_pos_right _ hp, -1, 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 b : α
⊢ toIcoMod hp (a + p) b = toIcoMod hp a b + p

Tactic:
simpa only [one_zsmul] using toIcoMod_add_zsmul' hp a b 1

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
p : X → Prop
⊢ (∃ t ⊆ {x | (fun y ↦ p y) x}, IsOpen[inst✝] t ∧ x ∈ t) ↔ ∃ t, (∀ y ∈ t, p y) ∧ IsOpen[inst✝] t ∧ x ∈ t

Tactic:
simp only [subset_def, mem_ofPred_eq]

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 : α
⊢ toIcoMod hp a b = toIcoMod hp 0 (b - a) + a

Tactic:
toIcoMod_sub_eq_sub,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a b = toIcoMod hp (0 + a) b - a + a
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ (a : X), ClusterPt a (𝓟 s) → a ∈ s) ↔ ∀ (x : X) (F : Filter X), F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s

Tactic:
exact ⟨fun hs x F F_ne FS Fx ↦ hs _ <| NeBot.mono F_ne (le_inf Fx FS),
         fun hs x hx ↦ hs x (𝓝 x ⊓ 𝓟 s) hx inf_le_right inf_le_left⟩

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' : Fact (0 < p)
x₁ x₂ x₃ : α
⊢ toIcoMod ⋯ 0 (x₂ - x₁) ≤ toIocMod ⋯ (0 + x₁) x₃ - x₁ ↔ toIcoMod ⋯ x₁ x₂ ≤ toIocMod ⋯ x₁ x₃

Tactic:
toIcoMod_sub_eq_sub,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp' : Fact (0 < p)
x₁ x₂ x₃ : α
⊢ toIcoMod ⋯ (0 + x₁) x₂ - x₁ ≤ toIocMod ⋯ (0 + x₁) x₃ - x₁ ↔ toIcoMod ⋯ x₁ x₂ ≤ toIocMod ⋯ x₁ x₃
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
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, V, U_open, V_open, h_sub_U, k_sub_V, UV_dis⟩
    exact
      ⟨⟨fun _ ↦ U,
        h_sub_U.trans (iUnion_const U).symm.subset,
        fun _ ↦
          ⟨U_open, disjoint_of_subset (fun ⦃a⦄ a ↦ a) k_sub_V (UV_dis.closure_left V_open)⟩⟩,
       ⟨fun _ ↦ V,
        k_sub_V.trans (iUnion_const V).symm.subset,
        fun _ ↦
          ⟨V_open, disjoint_of_subset (fun ⦃a⦄ a ↦ a) h_sub_U (UV_dis.closure_right U_open).symm⟩⟩⟩

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst✝] (s ∪ t)
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
⊢ s = s ∩ u ∪ t ∩ u

Tactic:
(huv.symm.mono_left htv).inter_eq,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst✝] (s ∪ t)
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
⊢ s = s ∩ u ∪ ∅
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX✝ : tX ∈ tas
hY : tY ∈ tbs
hf : Continuous[instTopologicalSpaceProd, tc] fun p ↦ f p.1 p.2
hX : Continuous[sInf tas, tX] id
⊢ Continuous[instTopologicalSpaceProd, tc] fun p ↦ f p.1 p.2

Tactic:
have hY := continuous_sInf_dom hY continuous_id

Goal state after:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX✝ : tX ∈ tas
hY✝ : tY ∈ tbs
hf : Continuous[instTopologicalSpaceProd, tc] fun p ↦ f p.1 p.2
hX : Continuous[sInf tas, tX] id
hY : Continuous[sInf tbs, tY] id
⊢ Continuous[instTopologicalSpaceProd, tc] fun p ↦ f p.1 p.2
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set (X × Y)
⊢ (∀ x ∈ s, s ∈ 𝓝 x) ↔
    ∀ (a : X) (b : Y), (a, b) ∈ s → ∃ u v, IsOpen[inst✝¹] u ∧ IsOpen[inst✝] v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ s

Tactic:
by simp_rw [Prod.forall, mem_nhds_prod_iff', and_left_comm]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

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

Tactic:
constructor <;>
      · rintro ⟨u, ou, useq⟩
        exact ⟨u, ou, by simpa only [Set.inter_comm, eq_comm] using useq⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ u ∈ s, IsOpen[t] u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen[t] u → ∃ v ∈ s, a ∈ v ∧ v ⊆ u
a : α
⊢ ∀ (i : Set α), a ∈ i ∧ IsOpen[t] i → ∃ i', (i' ∈ s ∧ a ∈ i') ∧ id i' ⊆ i

Tactic:
by simpa [and_assoc] using h_nhds a

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: β : Type u_2
s : ℕ → Set β
n : ℕ
⊢ accumulate s n = ⋃ k, ⋃ (_ : k < n + 1), s k

Tactic:
simp_rw [Nat.lt_add_one_iff, accumulate]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace β
inst✝ : FirstCountableTopology β
f : α → β
hf : IsInducing f
⊢ FirstCountableTopology α

Tactic:
rw [hf.1]
  exact firstCountableTopology_induced α β f

Goal state after:
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✝ : Finite ι
t : (i : ι) → X i
n : Set ((i : ι) → X i)
hn : ∃ I, I.Finite ∧ ∃ t_1, (∀ (i : ι), t_1 i ∈ 𝓝 (t i)) ∧ I.pi t_1 ⊆ n
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s

Tactic:
obtain ⟨s, -, n', hn', hsub⟩ := hn

Goal state after:
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
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter β
f : α → β
⊢ (comap f l).smallSets = comap (image f) l.smallSets

Tactic:
refine (gc_map_comap _).u_comm_of_l_comm (gc_map_comap _) bind_smallSets_gc bind_smallSets_gc ?_
  simp [Function.comp_def, map_bind, bind_map]

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst✝¹] (f i), ContinuousWithinAt g (f i) x
x : X
⊢ ContinuousWithinAt g (⋃ i, f i) x

Tactic:
rw [ContinuousWithinAt, hf.nhdsWithin_iUnion, tendsto_iSup]

Goal state after:
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst✝¹] (f i), ContinuousWithinAt g (f i) x
x : X
⊢ ∀ (i : ι), Tendsto g (𝓝[f i] x) (𝓝 (g x))
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: case inr.refine_2
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y
s t : Set X✝
inst✝³ : SigmaCompactSpace X✝
inst✝² : Countable ι
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), SigmaCompactSpace (X i)
h✝ : Nonempty ι
f : ℕ → ι
hf : Function.Surjective f
k : ℕ
y : X (f k)
n : ℕ
hn : y ∈ compactCovering (X (f k)) n
⊢ y ∈ compactCovering (X (f k)) (max k n)

Tactic:
exact compactCovering_subset _ (le_max_right _ _) hn

Goal state after:
Module: Mathlib.Data.Set.Subset

Goal state before:
pp: α : Type u_2
A : Set α
S : Set (Set α)
⊢ A ↓∩ ⋂₀ S = ⋂₀ {x | ∃ B ∈ S, A ↓∩ B = x}

Tactic:
rw [← Set.image, sInter_image]

Goal state after:
α : Type u_2
A : Set α
S : Set (Set α)
⊢ A ↓∩ ⋂₀ S = ⋂ a ∈ S, A ↓∩ a
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ≃o β
⊢ upperClosure (⇑f.symm.symm '' s) = (UpperSet.map f.symm.symm) (upperClosure s)

Tactic:
← UpperSet.symm_map,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ≃o β
⊢ upperClosure (⇑f.symm.symm '' s) = (UpperSet.map f.symm).symm (upperClosure s)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s s' : Set X
hs : IsCompact s
t t' : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : n ∈ 𝓝ˢ[s'] s ×ˢ 𝓝ˢ[t'] t
⊢ ∃ u ∈ 𝓝ˢ[s'] s, ∃ v ∈ 𝓝ˢ[t'] t, u ×ˢ v ⊆ n

Tactic:
Filter.mem_prod_iff

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s s' : Set X
hs : IsCompact s
t t' : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : ∃ t₁ ∈ 𝓝ˢ[s'] s, ∃ t₂ ∈ 𝓝ˢ[t'] t, t₁ ×ˢ t₂ ⊆ n
⊢ ∃ u ∈ 𝓝ˢ[s'] s, ∃ v ∈ 𝓝ˢ[t'] t, u ×ˢ v ⊆ n
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
hs : IsCompact s
t t' : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : n ∈ 𝓟 s ×ˢ 𝓝ˢ[t'] t
⊢ ∃ u ∈ 𝓝ˢ[t'] t, s ×ˢ u ⊆ n

Tactic:
Filter.mem_prod_iff

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
hs : IsCompact s
t t' : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : ∃ t₁ ∈ 𝓟 s, ∃ t₂ ∈ 𝓝ˢ[t'] t, t₁ ×ˢ t₂ ⊆ n
⊢ ∃ u ∈ 𝓝ˢ[t'] t, s ×ˢ u ⊆ n
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
s : Set (SeparationQuotient X × SeparationQuotient Y)
l : Filter α
⊢ Tendsto (uncurry (lift₂ f hf)) (𝓝[s] (mk x, mk y)) l ↔ Tendsto (uncurry f) (𝓝[Prod.map mk mk ⁻¹' s] (x, y)) l

Tactic:
rw [nhdsWithin, ← map_prod_map_mk_nhds, ← Filter.push_pull, comap_principal]
  rfl

Goal state after:
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:
rw [← subtype_inseparable_iff] at hxy

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