mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝ : L.HasPointwiseRightKanExtension F
G : D ⥤ H
α : L ⋙ G ⟶ F
Y : D
β : G ⟶ L.pointwiseRightKanExtension F :=
  { app := fun Y ↦ limit.lift (StructuredArrow.proj Y L ⋙ F) (L.structuredArrowMapCone F G α Y), naturality := ⋯ }
⊢ ((L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α).app Y =
    limit.lift (StructuredArrow.proj Y L ⋙ F) (L.structuredArrowMapCone F G α Y)

Tactic:
have h : (pointwiseRightKanExtension L F).liftOfIsRightKanExtension
      (pointwiseRightKanExtensionCounit L F) G α = β := by
    apply hom_ext_of_isRightKanExtension (α := pointwiseRightKanExtensionCounit L F)
    aesop

Goal state after:
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
inst✝ : L.HasPointwiseRightKanExtension F
G : D ⥤ H
α : L ⋙ G ⟶ F
Y : D
β : G ⟶ L.pointwiseRightKanExtension F :=
  { app := fun Y ↦ limit.lift (StructuredArrow.proj Y L ⋙ F) (L.structuredArrowMapCone F G α Y), naturality := ⋯ }
h : (L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α = β
⊢ ((L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α).app Y =
    limit.lift (StructuredArrow.proj Y L ⋙ F) (L.structuredArrowMapCone F G α Y)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mpr
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
L : C ⥤ D
F : C ⥤ H
F' : D ⥤ H
G : C' ⥤ C
inst✝ : G.IsEquivalence
α : F ⟶ L ⋙ F'
eq : StructuredArrow.IsUniversal (LeftExtension.mk F' α) ≃
  StructuredArrow.IsUniversal (LeftExtension.mk F' (G.whiskerLeft α ≫ (G.associator L F').inv)) := ⋯
⊢ F'.IsLeftKanExtension (G.whiskerLeft α ≫ (G.associator L F').inv) → F'.IsLeftKanExtension α

Tactic:
exact fun _ => ⟨⟨eq.symm (isUniversalOfIsLeftKanExtension _ _)⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v₁, u} C
D : Type u₂
inst✝⁴ : Category.{u, u₂} D
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : ∀ (X : D), PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
this : IsColimit (((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).mapCocone c) := ⋯
⊢ ∀ {X Y : C ⥤ D} (f : X ⟶ Y),
    (prod.functor.obj F ⋙ (evaluation C D).obj k).map f ≫ (asIso (prodComparison ((evaluation C D).obj k) F Y)).hom =
      (asIso (prodComparison ((evaluation C D).obj k) F X)).hom ≫
        ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).map f

Tactic:
intro G G'
              apply prodComparison_natural ((evaluation C D).obj k) (𝟙 F)

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Subobject

Goal state before:
pp: case refine_1.refine_3
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ cokernel.π (kernel.ι f.unop) ≫
      ((epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯).op ≫ (cokernel.desc (kernel.ι f.unop) f.unop ⋯).op).unop =
    cokernel.π (kernel.ι f.unop) ≫ (𝟙 (op (cokernel (kernel.ι f.unop)))).unop

Tactic:
simp only [unop_comp, Quiver.Hom.unop_op, unop_id_op, cokernel.π_desc_assoc,
        comp_epiDesc, Category.comp_id]

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

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsDetecting
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : IsIso f
⊢ ∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((coyoneda.obj (op G)).map f))

Tactic:
isIso_iff_yoneda_map_bijective

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsDetecting
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : ∀ (T : C), Function.Bijective fun x ↦ x ≫ f
⊢ ∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((coyoneda.obj (op G)).map f))
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ ∀ (X : WalkingParallelFamily (ULift.{w, 0} Bool)),
    (parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
          ((NatIso.ofComponents (fun X ↦ eqToIso ⋯) @walkingParallelFamilyEquivWalkingParallelPair._proof_3).hom.app
            X) ≫
        (NatIso.ofComponents (fun X ↦ eqToIso ⋯) @walkingParallelFamilyEquivWalkingParallelPair._proof_6).hom.app
          ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
            X) =
      𝟙 ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj X)

Tactic:
rintro (_ | _) <;> cat_disch

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

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
hf : Epi f
iX : limit X ≅ AddCommGrpCat.of ((i : J) → ↑(X.obj { as := i })) :=
  (Pi.isoLimit X).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ X.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ X.obj { as := j }).isLimit
iY : limit Y ≅ AddCommGrpCat.of ((i : J) → ↑(Y.obj { as := i })) :=
  (Pi.isoLimit Y).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ Y.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ Y.obj { as := j }).isLimit
this :
  (Pi.map fun i ↦ ⇑(ConcreteCategory.hom (f.app { as := i }))) = ⇑(ConcreteCategory.hom (iX.inv ≫ lim.map f ≫ iY.hom))
⊢ Epi (iX.inv ≫ lim.map f ≫ iY.hom)

Tactic:
AddCommGrpCat.epi_iff_surjective,

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
hf : Epi f
iX : limit X ≅ AddCommGrpCat.of ((i : J) → ↑(X.obj { as := i })) :=
  (Pi.isoLimit X).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ X.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ X.obj { as := j }).isLimit
iY : limit Y ≅ AddCommGrpCat.of ((i : J) → ↑(Y.obj { as := i })) :=
  (Pi.isoLimit Y).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ Y.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ Y.obj { as := j }).isLimit
this :
  (Pi.map fun i ↦ ⇑(ConcreteCategory.hom (f.app { as := i }))) = ⇑(ConcreteCategory.hom (iX.inv ≫ lim.map f ≫ iY.hom))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (iX.inv ≫ lim.map f ≫ iY.hom))
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
X₁ X₂ : C
f : X₁ ⟶ X₂
u : F.Elements
⊢ ((shrinkYoneda.{w, v₁, u₁}.map f).app (op u.fst) ≫
      ↾fun t ↦ (ConcreteCategory.hom (F.map (shrinkYonedaObjObjEquiv t))) u.snd) =
    (↾fun t ↦ (ConcreteCategory.hom (F.map (shrinkYonedaObjObjEquiv t))) u.snd) ≫ F.map f

Tactic:
ext g

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X₁ X₂ : C
f : X₁ ⟶ X₂
u : F.Elements
g : (shrinkYoneda.{w, v₁, u₁}.obj X₁).obj (op u.fst)
⊢ (ConcreteCategory.hom
          ((shrinkYoneda.{w, v₁, u₁}.map f).app (op u.fst) ≫
            ↾fun t ↦ (ConcreteCategory.hom (F.map (shrinkYonedaObjObjEquiv t))) u.snd)).toFun
      g =
    (ConcreteCategory.hom ((↾fun t ↦ (ConcreteCategory.hom (F.map (shrinkYonedaObjObjEquiv t))) u.snd) ≫ F.map f)).toFun
      g
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
r : R
eq1 : r • y = 0
⊢ 0 ∈ (extensionOfMax i f).domain

Tactic:
apply Submodule.zero_mem _

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Range

Goal state before:
pp: a : ℕ
s : Finset ℕ
⊢ ∀ ⦃a_1 : ℕ⦄, a_1 ∈ range a → a_1 ∉ map (addLeftEmbedding a) s

Tactic:
mem_map,

Goal state after:
a : ℕ
s : Finset ℕ
⊢ ∀ ⦃a_1 : ℕ⦄, a_1 ∈ range a → ¬∃ a_3 ∈ s, (addLeftEmbedding a) a_3 = a_1
Module: Mathlib.Algebra.Group.Nat.Range

Goal state before:
pp: a : ℕ
s : Finset ℕ
⊢ Disjoint (range a) (map (addRightEmbedding a) s)

Tactic:
rw [← addLeftEmbedding_eq_addRightEmbedding]

Goal state after:
a : ℕ
s : Finset ℕ
⊢ Disjoint (range a) (map (addLeftEmbedding a) s)
Module: Mathlib.Data.Nat.Count

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ count p (a + b) = count p a + count (fun k ↦ p (a + k)) b

Tactic:
by
  simp [count, List.range_add, Function.comp_def]

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

Goal state before:
pp: case convert_1
a b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
p : ℕ := (k + 2).minFac
hp : Prime p
t : ℕ := (k + 2).factorization p
hpt : p ^ t ∣ k + 2
htp : 0 < t
⊢ ¬p ∣ (k + 2) / p ^ t

pp: case convert_2
a b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
p : ℕ := (k + 2).minFac
hp : Prime p
t : ℕ := (k + 2).factorization p
hpt : p ^ t ∣ k + 2
htp : 0 < t
⊢ k + 2 < p ^ t * (k + 2)

Tactic:
· rw [Nat.dvd_div_iff_mul_dvd hpt, ← Nat.pow_succ]
        exact pow_succ_factorization_not_dvd (k + 1).succ_ne_zero hp

Goal state after:
case convert_2
a b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
p : ℕ := (k + 2).minFac
hp : Prime p
t : ℕ := (k + 2).factorization p
hpt : p ^ t ∣ k + 2
htp : 0 < t
⊢ k + 2 < p ^ t * (k + 2)
Module: Mathlib.Data.Nat.Periodic

Goal state before:
pp: α : Type u_1
f : ℕ → α
a : ℕ
hf : Periodic f a
n : ℕ
| f n

Tactic:
← n.mod_add_div a,

Goal state after:
α : Type u_1
f : ℕ → α
a : ℕ
hf : Periodic f a
n : ℕ
| f (n % a + a * (n / a))
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case zero
a k n : ℕ
a_ne_zero : a ≠ 0
⊢ #({x ∈ Ico k (k + (n % a + a * 0)) | a.Coprime x}) ≤ φ a * (0 + 1)

Tactic:
rw [← filter_coprime_Ico_eq_totient a k]
    simp only [add_zero, mul_one, mul_zero, zero_add]
    gcongr
    exact le_of_lt (mod_lt n (pos_iff_ne_zero.mpr a_ne_zero))

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

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ φ p = p - 1

Tactic:
rw [← pow_one p, totient_prime_pow hp] <;> 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 : α
⊢ toIcoDiv hp a b • p - b = -toIcoMod hp a b

Tactic:
by
  rw [toIcoMod, neg_sub]

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

Goal state before:
pp: n : ℕ
hn : 0 < n
⊢ ∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1)) ∣ n ^ φ n

Tactic:
have := Nat.prod_primeFactors_dvd n
  rw [← Nat.pow_dvd_pow_iff (Nat.totient_pos.mpr hn).ne', ← Finset.prod_pow] at this
  refine dvd_trans (Finset.prod_dvd_prod_of_dvd _ _ fun p hp ↦ ?_) this
  exact Nat.pow_dvd_pow p <| Nat.div_le_self _ _

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 : α
⊢ b - c - toIcoDiv hp (a + c) b • p ∈ Set.Ico a (a + p)

Tactic:
← sub_right_comm,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ b - toIcoDiv hp (a + c) b • p - c ∈ Set.Ico a (a + 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 c : α
⊢ b - c - toIocDiv hp (a + c) b • p ∈ Set.Ioc a (a + p)

Tactic:
← sub_right_comm,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ b - toIocDiv hp (a + c) b • p - c ∈ Set.Ioc a (a + 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 c : α
⊢ toIcoDiv hp (a - c) b = toIcoDiv hp a (b + c)

Tactic:
← sub_neg_eq_add,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIcoDiv hp (a - c) b = toIcoDiv hp a (b - -c)
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 : α
⊢ toIocDiv hp (a - c) b = toIocDiv hp a (b + c)

Tactic:
← sub_neg_eq_add,

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set (Set X)
hs : s.Finite
h : ∀ t ∈ s, IsOpen[inst✝] t
⊢ IsOpen[inst✝] (⋂₀ s)

Tactic:
by
  induction s, hs using Set.Finite.induction_on with
  | empty => rw [sInter_empty]; exact isOpen_univ
  | insert _ _ ih =>
    simp only [sInter_insert, forall_mem_insert] at h ⊢
    exact h.1.inter (ih h.2)

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

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

Tactic:
rw [add_comm, toIocMod_add_right]

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_sub_zsmul' hp a b 1

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

Goal state before:
pp: α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
⊢ f₁.lift g₁ ×ˢ f₂.lift g₂ = f₁.lift fun s ↦ f₂.lift fun t ↦ g₁ s ×ˢ g₂ t

Tactic:
by
  simp only [prod_def, lift_assoc hg₁]
  apply congr_arg; funext x
  rw [lift_comm]
  apply congr_arg; funext y
  apply lift'_lift_assoc hg₂

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 : α
⊢ toIcoMod hp c a = toIcoMod hp c b ↔ a ≡ b [PMOD p]

Tactic:
by
  rw [toIcoMod_eq_toIcoMod, AddCommGroup.modEq_iff_zsmul']

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
F G : Filter X
⊢ AccPt x (F ⊔ G) ↔ AccPt x F ∨ AccPt x G

Tactic:
simp only [AccPt, inf_sup_left, sup_neBot]

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ AccPt x (𝓟 s) ↔ (𝓝[s \ {x}] x).NeBot

Tactic:
accPt_principal_iff_clusterPt,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ ClusterPt x (𝓟 (s \ {x})) ↔ (𝓝[s \ {x}] x).NeBot
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₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
⊢ toIcoMod hp x₁ x₄ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₁

Tactic:
constructor
  · suffices h : ¬x₃ ≡ x₂ [PMOD p] by
      have h₁₂₃' := toIxxMod_cyclic_left _ (toIxxMod_cyclic_left _ h₁₂₃.1)
      have h₂₃₄' := toIxxMod_cyclic_left _ (toIxxMod_cyclic_left _ h₂₃₄.1)
      rw [(not_modEq_iff_toIcoMod_eq_toIocMod hp).1 h] at h₂₃₄'
      exact toIxxMod_cyclic_left _ (h₁₂₃'.trans h₂₃₄')
    by_contra h
    rw [(modEq_iff_toIcoMod_eq_left hp).1 h] at h₁₂₃
    exact h₁₂₃.2 (left_lt_toIocMod _ _ _).le
  · rw [not_le] at h₁₂₃ h₂₃₄ ⊢
    exact (h₁₂₃.2.trans_le (toIcoMod_le_toIocMod _ x₃ x₂)).trans h₂₃₄.2

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

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

Tactic:
by
  rw [add_comm, toIocMod_add_toIocDiv_mul]

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
⊢ s ∈ sSup (𝓝 '' t) ↔ ∀ x ∈ t, s ∈ 𝓝 x

Tactic:
Filter.mem_sSup,

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
⊢ (∀ f ∈ 𝓝 '' t, s ∈ f) ↔ ∀ x ∈ t, s ∈ 𝓝 x
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
t₂ : TopologicalSpace α
β : Type u_2
inst✝¹ : TopologicalSpace β
inst✝ : IndiscreteTopology β
f : α → β
⊢ ∀ (s : Set β), IsOpen[inst✝¹] s → IsOpen[t₂] (f ⁻¹' s)

Tactic:
simp [IndiscreteTopology.isOpen_iff]

Goal state after:
Module: Mathlib.Topology.Order

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

Tactic:
simp only [continuous_iff_le_induced, sup_le_iff]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
inst✝ : TopologicalSpace β
f : α → β
a : α
l : Filter α
⊢ nhdsAdjoint a l ≤ induced f inst✝ ↔ Tendsto f l (𝓝 (f a))

Tactic:
gc_nhds _ _,

Goal state after:
α : Type u
β : Type v
inst✝ : TopologicalSpace β
f : α → β
a : α
l : Filter α
⊢ l ≤ 𝓝 a ↔ Tendsto f l (𝓝 (f a))
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
s : Set X
x : X
⊢ f '' s ∈ map f (𝓝 x) ↔ s ∈ 𝓝 x

Tactic:
mem_map,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
s : Set X
x : X
⊢ f ⁻¹' f '' s ∈ 𝓝 x ↔ s ∈ 𝓝 x
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
x : X
y : Y
hs : s ∈ map Prod.fst (𝓝[Prod.snd ⁻¹' {(x, y).2}] (x, y))
⊢ s ∈ 𝓝 (x, y).1

Tactic:
mem_map,

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
x : X
y : Y
hs : Prod.fst ⁻¹' s ∈ 𝓝[Prod.snd ⁻¹' {(x, y).2}] (x, y)
⊢ s ∈ 𝓝 (x, y).1
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
x : X
y : Y
hs : s ∈ map Prod.snd (𝓝[Prod.fst ⁻¹' {(x, y).1}] (x, y))
⊢ s ∈ 𝓝 (x, y).2

Tactic:
mem_map,

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
x : X
y : Y
hs : Prod.snd ⁻¹' s ∈ 𝓝[Prod.fst ⁻¹' {(x, y).1}] (x, y)
⊢ s ∈ 𝓝 (x, y).2
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s s' : Set α
t t' : Set β
⊢ 𝓝ˢ[s' ×ˢ t'] (s ×ˢ t) ≤ 𝓝ˢ[s'] s ×ˢ 𝓝ˢ[t'] t

Tactic:
simpa [nhdsSetWithin, ← prod_inf_prod] using inf_le_of_left_le <| nhdsSet_prod_le _ _

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

Goal state before:
pp: 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))
⊢ IsInducing (Sum.elim f g)

Tactic:
← disjoint_principal_nhdsSet

Goal state after:
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 (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (range f) (closure[inst✝] (range g))
⊢ IsInducing (Sum.elim f g)
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: 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
h : IsInducing (Sum.elim f g)
C : Set Z
C_closed : IsClosed[inst✝] C
hC : Sum.elim f g ⁻¹' C = range inl
⊢ range inl ⊆ Sum.elim f g ⁻¹' C

Tactic:
hC

Goal state after:
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
h : IsInducing (Sum.elim f g)
C : Set Z
C_closed : IsClosed[inst✝] C
hC : Sum.elim f g ⁻¹' C = range inl
⊢ range inl ⊆ range inl
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 : α → β
⊢ ContinuousOn f s ↔ ∀ t_1 ∈ B, ∃ u, IsOpen[t] u ∧ f ⁻¹' t_1 ∩ s = u ∩ s

Tactic:
by
  rw [continuousOn_iff']
  refine ⟨fun h t ht => h t (hB.isOpen ht), fun h t ht => ?_⟩
  obtain ⟨ι, g, rfl, hg⟩ := hB.open_eq_iUnion ht
  choose v hv he using (fun i => h (g i) (hg i))
  exact ⟨⋃ i, v i, isOpen_iUnion hv, by simp_all [iUnion_inter]⟩

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ∀ (x : β) (x_1 x_2 : α), x_2 ≤ x_1 ∧ x ∈ s x_2 → ∃ i, x ∈ s i

Tactic:
intro z

Goal state after:
case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
z : β
⊢ ∀ (x x_1 : α), x_1 ≤ x ∧ z ∈ s x_1 → ∃ i, z ∈ s i
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 ?_

Goal state after:
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
hx : x ∉ s
⊢ x ∉ closure[inst✝¹] s
Module: Mathlib.Topology.Bornology.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : Bornology α
inst✝ : Finite ι
s : ι → Set α
⊢ (∀ s_1 ∈ range s, IsBounded s_1) ↔ ∀ (i : ι), IsBounded (s i)

Tactic:
forall_mem_range

Goal state after:
ι : Type u_1
α : Type u_2
inst✝¹ : Bornology α
inst✝ : Finite ι
s : ι → Set α
⊢ (∀ (i : ι), IsBounded (s i)) ↔ ∀ (i : ι), IsBounded (s i)
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
f : Filter α
hf : f.NeBot
x : α
⊢ f ≤ pure x ↔ {x} ∈ f

Tactic:
le_pure_iff

Goal state after:
α : Type u
f : Filter α
hf : f.NeBot
x : α
⊢ {x} ∈ f ↔ {x} ∈ f