mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
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
inst✝ : Category.{v_5, u_5} D'
L : C ≌ D
F₀ : C ⥤ H
F₁ : D ⥤ H
α : L.functor ⋙ F₁ ≅ F₀
⊢ F₁.IsRightKanExtension α.hom

Tactic:
by
  refine ⟨⟨?_⟩⟩
  apply RightExtension.isUniversalPostcomp₁Equiv
    (G := L.functor) L.functor.leftUnitor F₀ _ |>.invFun
  refine IsTerminal.ofUniqueHom
    (fun y ↦ CostructuredArrow.homMk <| y.left.leftUnitor.inv ≫ y.hom ≫ α.inv) ?_
  intro y m
  ext x
  simpa using congr_app m.w x =≫ α.inv.app x

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCodetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
G : C
hG : P G
h : unop Y ⟶ G
t : op G ⟶ X
ht : t ≫ f = h.op
ht' : ∀ (y : op G ⟶ X), (fun h' ↦ h' ≫ f = h.op) y → y = t
y : unop X ⟶ G
hy : (fun h' ↦ f.unop ≫ h' = h) y
⊢ (fun h' ↦ h' ≫ f = h.op) y.op

Tactic:
exact Quiver.Hom.unop_inj (by simpa only using! hy)

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsDetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
G : C
hG : P G
h : G ⟶ unop X
t : Y ⟶ op G
ht : f ≫ t = h.op
ht' : ∀ (y : Y ⟶ op G), (fun h' ↦ f ≫ h' = h.op) y → y = t
y : G ⟶ unop Y
hy : (fun h' ↦ h' ≫ f.unop = h) y
⊢ (fun h' ↦ f ≫ h' = h.op) y.op

Tactic:
exact Quiver.Hom.unop_inj (by simpa only using! hy)

Goal state after:
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)
F : WalkingParallelFamily J ⥤ C
j : WalkingParallelFamily J
⊢ F.obj j = (parallelFamily fun j ↦ F.map (line j)).obj j

Tactic:
cases j <;> cat_disch

Goal state after:
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)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j ↦ F.map (line j)
j : WalkingParallelFamily J
⊢ (parallelFamily fun j ↦ F.map (line j)).obj j = F.obj j

Tactic:
cases j <;> cat_disch

Goal state after:
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)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j ↦ F.map (line j)
j : WalkingParallelFamily J
⊢ F.obj j = (parallelFamily fun j ↦ F.map (line j)).obj j

Tactic:
cases j <;> cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
P : ObjectProperty C
X : C
inst✝ : HasCoproduct (P.coproductFromFamily X)
Y : C
f : Y ⟶ X
hY : P Y
⊢ P.ι.obj { obj := Y, property := hY } ⟶ X

Tactic:
by exact f

Goal state after:
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)
F : WalkingParallelFamily J ⥤ C
t : Cone F
j : WalkingParallelFamily J
⊢ F.obj j = (parallelFamily fun j ↦ F.map (line j)).obj j

Tactic:
cases j <;> cat_disch

Goal state after:
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)
F : WalkingParallelFamily J ⥤ C
t : Cocone F
j : WalkingParallelFamily J
⊢ (parallelFamily fun j ↦ F.map (line j)).obj j = F.obj j

Tactic:
cases j <;> cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
P : ObjectProperty C
X : C
inst✝ : HasProduct (P.productToFamily X)
Y : C
f : X ⟶ Y
hY : P Y
⊢ X ⟶ P.ι.obj { obj := Y, property := hY }

Tactic:
by exact f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
⊢ Function.Injective
    (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
        (coconeπOpCompShrinkYonedaObj F X)))

pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
x :
  (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
      (coconeπOpCompShrinkYonedaObj F X)).pt
⊢ ∃ a,
    ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
        (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
          (coconeπOpCompShrinkYonedaObj F X))
        a =
      x

Tactic:
· let G := (CategoryOfElements.π F).op ⋙ shrinkYoneda.{w}.obj X
    let c := G.coconeTypesEquiv.symm (coconeπOpCompShrinkYonedaObj F X)
    have (u : G.ColimitType) (x : F.obj X) (h : G.descColimitType c u = x) :
        G.ιColimitType (op (elementsMk _ _ x))
          (shrinkYonedaObjObjEquiv.symm (𝟙 X)) = u := by
      obtain ⟨⟨u⟩, v, rfl⟩ := Functor.ιColimitType_jointly_surjective _ u
      obtain ⟨v, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective v
      dsimp [c] at v h
      simp only [Equiv.apply_symm_apply] at h
      rw [← G.ιColimitType_map (show u ⟶ F.elementsMk _ x from ⟨v, h⟩).op]
      simp [G, shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm.{w}]
    intro u₁ u₂ hu
    generalize hx₁ : G.descColimitType c u₁ = x
    have hx₂ : G.descColimitType c u₂ = x := by rw [← hx₁]; exact hu.symm
    rw [← this _ _ hx₁, ← this _ _ hx₂]

Goal state after:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
x :
  (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
      (coconeπOpCompShrinkYonedaObj F X)).pt
⊢ ∃ a,
    ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
        (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
          (coconeπOpCompShrinkYonedaObj F X))
        a =
      x
Module: Mathlib.Algebra.Category.Grp.Injective

Goal state before:
pp: case inr
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : ↥(ℤ ∙ m) →ₗ[ℤ] A
h0 : m ≠ 0
gₘ : A := g ⟨m, ⋯⟩
n : ℤ
hn : n ∈ ℤ ∙ m
⊢ (LinearMap.toSpanSingleton ℤ A (DivisibleBy.div gₘ m)) n = g ⟨n, hn⟩

Tactic:
rcases Submodule.mem_span_singleton.mp hn with ⟨n, rfl⟩

Goal state after:
case inr
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : ↥(ℤ ∙ m) →ₗ[ℤ] A
h0 : m ≠ 0
gₘ : A := g ⟨m, ⋯⟩
n : ℤ
hn : n • m ∈ ℤ ∙ m
⊢ (LinearMap.toSpanSingleton ℤ A (DivisibleBy.div gₘ m)) (n • m) = g ⟨n • m, hn⟩
Module: Mathlib.Data.ZMod.IntUnitsPower

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R (Additive ℤˣ)
u : ℤˣ
n : ℕ
⊢ Additive.toMul (↑n • Additive.ofMul u) = u ^ n

Tactic:
Nat.cast_smul_eq_nsmul,

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R (Additive ℤˣ)
u : ℤˣ
n : ℕ
⊢ Additive.toMul (n • Additive.ofMul u) = u ^ n
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: case mp
n : ℤ
h : n.negOnePow = -1
⊢ Odd n

Tactic:
← Int.not_even_iff_odd

Goal state after:
case mp
n : ℤ
h : n.negOnePow = -1
⊢ ¬Even n
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⟩ + (extendIdealTo i f h y) r

Tactic:
rw [eq3, ← add_assoc, ← (extensionOfMax i f).toLinearPMap.map_add, AddMemClass.mk_add_mk]

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 + (r • y - snd i x • y), ⋯⟩ + (extendIdealTo i f h y) (snd i x)
Module: Mathlib.Algebra.Group.Nat.Range

Goal state before:
pp: a b : ℕ
⊢ (range (a + b)).val = (range a ∪ map (addLeftEmbedding a) (range b)).val

Tactic:
union_val

Goal state after:
a b : ℕ
⊢ (range (a + b)).val = (range a).val ∪ (map (addLeftEmbedding a) (range b)).val
Module: Mathlib.Data.Nat.Totient

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

Tactic:
← add_assoc

Goal state after:
case succ
a k n : ℕ
a_ne_zero : a ≠ 0
i : ℕ
ih : #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) ≤ φ a * (i + 1)
⊢ #({x ∈ Ico k (k + n % a + a * i + a) | a.Coprime x}) ≤ φ a * i + φ a + φ a
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : (d * x).gcd b = d
⊢ (d * x).gcd b ∣ b

Tactic:
apply gcd_dvd_right

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

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x ↦ x * p
h2 : image (fun x ↦ x * p) (range (p ^ n)) ⊆ range (p ^ (n + 1))
⊢ p * p ^ n - 1 * p ^ n = 1 * p ^ n * (p - 1)

Tactic:
← tsub_mul,

Goal state after:
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x ↦ x * p
h2 : image (fun x ↦ x * p) (range (p ^ n)) ⊆ range (p ^ (n + 1))
⊢ (p - 1) * p ^ n = 1 * p ^ n * (p - 1)
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: α : Type u_3
f : Filter α
s : ℕ → Set α
hs : f.HasAntitoneBasis s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
this : ∀ (t : Set ℕ), t.Finite → ∀ᶠ (n : ℕ) in atTop, ∀ m ∈ t, m < n ∧ r m n
φ : ℕ → ℕ
hφ : ∀ (n m : ℕ), m ∈ φ '' Iio n → m < φ n ∧ r m (φ n)
⊢ ∃ φ, StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)

Tactic:
simp only [forall_mem_image, forall_and, mem_Iio] at hφ

Goal state after:
α : Type u_3
f : Filter α
s : ℕ → Set α
hs : f.HasAntitoneBasis s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
this : ∀ (t : Set ℕ), t.Finite → ∀ᶠ (n : ℕ) in atTop, ∀ m ∈ t, m < n ∧ r m n
φ : ℕ → ℕ
hφ : (∀ (x : ℕ) ⦃x_1 : ℕ⦄, x_1 < x → φ x_1 < φ x) ∧ ∀ (x : ℕ) ⦃x_1 : ℕ⦄, x_1 < x → r (φ x_1) (φ x)
⊢ ∃ φ, StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)
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 : α
n : ℤ
hc : b - n • p ∈ Set.Ioc a (a + p)
⊢ toIocMod hp a b = b - n • p

Tactic:
rw [← toIocDiv_eq_of_sub_zsmul_mem_Ioc hp hc, toIocMod]

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 : α
⊢ toIocDiv hp (p + a) b = toIocDiv hp a b - 1

Tactic:
by
  rw [add_comm, toIocDiv_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 c : α
⊢ b - toIcoDiv hp (a + c) b • p ∈ Set.Ico (a + c) (a + c + p)

Tactic:
exact sub_toIcoDiv_zsmul_mem_Ico hp (a + c) b

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
h : Set α → Set β
m : β → γ
hh : Monotone h
⊢ f.lift (map m ∘ 𝓟 ∘ h) = f.lift' (image m ∘ h)

Tactic:
by simp only [comp_def, Filter.lift', map_principal]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hS : S.Finite
⊢ interior (⋂₀ S) = ⋂ s ∈ S, interior s

Tactic:
sInter_eq_biInter,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hS : S.Finite
⊢ interior (⋂ i ∈ S, i) = ⋂ s ∈ S, interior s
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ IsOpen[inst✝] {x} ↔ 𝓝 x = pure x

Tactic:
simp [← (pure_le_nhds _).ge_iff_eq', isOpen_iff_mem_nhds]

Goal state after:
Module: Mathlib.Topology.Continuous

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
l : Filter X
l' : Filter Y
h : Tendsto f l l'
s : Set Y
hs : s ∈ l'
⊢ ∀ᶠ (a : X) in l.lift' closure[inst✝¹], f a ∈ closure[inst✝] s

Tactic:
by
    filter_upwards [mem_lift' (h hs)] using (mapsTo_preimage _ _).closure hf

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 : α
this : toIcoMod hp 0 (a - b) + toIcoMod hp 0 (c - b) + (toIocMod hp 0 (b - a) + toIocMod hp 0 (b - c)) = p + p
⊢ toIcoMod hp b a ≤ toIocMod hp b c ∨ toIcoMod hp b c ≤ toIocMod hp b a

Tactic:
rw [_root_.add_comm (toIocMod _ _ _), add_add_add_comm, ← two_nsmul] at this

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
this : toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - c) + (toIcoMod hp 0 (c - b) + toIocMod hp 0 (b - a)) = 2 • p
⊢ toIcoMod hp b a ≤ toIocMod hp b c ∨ toIcoMod hp b c ≤ toIocMod hp b a
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case H.H.H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
z✝² z✝¹ z✝ : α
h₁₂₃ : btw ↑z✝² ↑z✝¹ ↑z✝
h₃₂₁ : btw ↑z✝ ↑z✝¹ ↑z✝²
⊢ ↑z✝² = ↑z✝¹ ∨ ↑z✝¹ = ↑z✝ ∨ ↑z✝ = ↑z✝²

Tactic:
rw [btw_cyclic] at h₃₂₁

Goal state after:
case H.H.H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
z✝² z✝¹ z✝ : α
h₁₂₃ : btw ↑z✝² ↑z✝¹ ↑z✝
h₃₂₁ : btw ↑z✝² ↑z✝ ↑z✝¹
⊢ ↑z✝² = ↑z✝¹ ∨ ↑z✝¹ = ↑z✝ ∨ ↑z✝ = ↑z✝²
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
hr : b - toIocDiv hp a b • p ≤ a + p
⊢ b ≤ a + (toIocDiv hp a b • p + p)

Tactic:
← add_assoc

Goal state after:
α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
hr : b - toIocDiv hp a b • p ≤ a + p
⊢ b ≤ a + toIocDiv hp a b • p + p
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
⊢ b < a + (toIcoDiv hp a b • p + p)

Tactic:
← add_assoc

Goal state after:
α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
⊢ b < a + toIcoDiv hp a b • p + p
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
ι : Sort u_4
s : ι → Set X
⊢ 𝓝ˢ (⋃ i, s i) = ⨆ i, 𝓝ˢ (s i)

Tactic:
by
  simp only [nhdsSet, image_iUnion, sSup_iUnion (β := Filter X)]

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
x✝ : ℕ
⊢ Disjoint (closure[inst✝] ((fun x ↦ ∅) x✝)) s

Tactic:
by simp only [closure_empty, empty_disjoint]

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

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (s : Set X), IsClosed[inst✝¹] s → s.Nonempty → IsClosed[inst✝] (f '' s)
s : Set X
hs : IsClosed[inst✝¹] s
h2s : s = ∅
⊢ IsClosed[inst✝] ∅

Tactic:
isClosed_empty

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
⊢ IsClosedMap f ↔ ∀ {s : Set X}, kernImage f (interior s) ⊆ interior (kernImage f s)

Tactic:
rw [isClosedMap_iff_closure_image, compl_surjective.forall]
  simp [kernImage_eq_compl]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
h : t ∈ 𝓝[s] a
⊢ 𝓝[t ∩ s] a = 𝓝[s] a

Tactic:
nhdsWithin_inter_of_mem h

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
h : t ∈ 𝓝[s] a
⊢ 𝓝[s] a = 𝓝[s] a
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: Y : Type v
Z : Type u_2
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
ι : Type u_5
κ : Type u_6
f : ι → Y
g : κ → Z
hf : DenseRange f
hg : DenseRange g
⊢ DenseRange (Prod.map f g)

Tactic:
by
  simpa only [DenseRange, prod_range_range_eq] using! hf.prod hg

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
ht : IsOpen[inst✝] t
⊢ frontier (s ∩ t) ∩ t = frontier s ∩ t

Tactic:
simp only [Set.inter_comm _ t, ← Subtype.preimage_coe_eq_preimage_coe_iff,
    ht.isOpenMap_subtype_val.preimage_frontier_eq_frontier_preimage continuous_subtype_val,
    Subtype.preimage_coe_self_inter]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: Y : Type v
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : DecidableEq ι
l : Filter Y
f : Y → (i : ι) → A i
x : (i : ι) → A i
hf : Tendsto f l (𝓝 x)
i : ι
g : Y → A i
xi : A i
hg : Tendsto g l (𝓝 xi)
j : ι
⊢ Tendsto (fun i_1 ↦ Function.update (f i_1) i (g i_1) j) l (𝓝 (Function.update x i xi j))

Tactic:
by rcases eq_or_ne j i with (rfl | hj) <;> simp [*, hf.apply_nhds]

Goal state after:
Module: Mathlib.Topology.Bases

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

Tactic:
refine ⟨fun i ↦ ⟨f i i.2, hfc i i.2⟩, fun i (hi : i ∈ I) ↦ ?_⟩

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

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

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

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝¹ : FirstCountableTopology α
x : α
f : Filter α
inst✝ : f.IsCountablyGenerated
hx : ClusterPt x f
⊢ ∃ ψ, Tendsto ψ atTop (𝓝 x) ∧ Tendsto ψ atTop f

Tactic:
unfold ClusterPt at hx

Goal state after:
α : Type u
t : TopologicalSpace α
inst✝¹ : FirstCountableTopology α
x : α
f : Filter α
inst✝ : f.IsCountablyGenerated
hx : (𝓝 x ⊓ f).NeBot
⊢ ∃ ψ, Tendsto ψ atTop (𝓝 x) ∧ Tendsto ψ atTop f
Module: Mathlib.Topology.Bases

Goal state before:
pp: case right.a
α : Type u
t : TopologicalSpace α
inst✝¹ : Countable α
inst✝ : FirstCountableTopology α
b : α → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun i ↦ b x i
⊢ range (uncurry b) ⊆ {s | IsOpen[t] s}

Tactic:
rintro _ ⟨⟨x, n⟩, rfl⟩

Goal state after:
case right.a
α : Type u
t : TopologicalSpace α
inst✝¹ : Countable α
inst✝ : FirstCountableTopology α
b : α → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun i ↦ b x i
x : α
n : ℕ
⊢ uncurry b (x, n) ∈ {s | IsOpen[t] s}
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x

Tactic:
have : ∀ x : s, (↑) ⁻¹' f x ∈ 𝓝 x := fun x => preimage_coe_mem_nhds_subtype.2 (hf x x.2)

Goal state after:
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x
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 ?_

Goal state after:
α : Type u_1
β : Type u_2
l : Filter β
f : α → β
⊢ ∀ (x : Filter (Set α)), map f (x.bind 𝓟) = (map (image f) x).bind 𝓟