mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
hS : S.Exact
h : S.RightHomologyData
inst✝ : Epi S.g
this✝ : Mono h.g'
this : Epi h.g'
⊢ IsIso h.g'

Tactic:
exact isIso_of_mono_of_epi h.g'

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
⊢ [∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Mono (F.map S.f),
      ∀ (S : ShortComplex C), S.Exact ∧ Mono S.f → (S.map F).Exact ∧ Mono (F.map S.f),
      ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F, PreservesFiniteLimits F].TFAE

Tactic:
by
  tfae_have 1 → 2
  | hF, S, ⟨hS, hf⟩ => by
    have := preservesMonomorphisms_of_preserves_shortExact_left F hF
    refine ⟨?_, inferInstance⟩
    let T := ShortComplex.mk S.f (Abelian.coimage.π S.g) (Abelian.comp_coimage_π_eq_zero S.zero)
    let φ : T.map F ⟶ S.map F :=
      { τ₁ := 𝟙 _
        τ₂ := 𝟙 _
        τ₃ := F.map <| Abelian.factorThruCoimage S.g
        comm₂₃ := show 𝟙 _ ≫ F.map _ = F.map (cokernel.π _) ≫ _ by
          rw [Category.id_comp, ← F.map_comp, cokernel.π_desc] }
    exact (exact_iff_of_epi_of_isIso_of_mono φ).1 (hF T ⟨(S.exact_iff_exact_coimage_π).1 hS⟩).1
  tfae_have 2 → 3
  | hF, X, Y, f => by
    refine preservesLimit_of_preserves_limit_cone (kernelIsKernel f) ?_
    apply (KernelFork.isLimitMapConeEquiv _ F).2
    let S := ShortComplex.mk _ _ (kernel.condition f)
    let hS := hF S ⟨exact_kernel f, inferInstance⟩
    have : Mono (S.map F).f := hS.2
    exact hS.1.fIsKernel
  tfae_have 3 → 4
  | hF => by
    exact preservesFiniteLimits_of_preservesKernels F
  tfae_have 4 → 1
  | ⟨_⟩, S, hS =>
    (S.map F).exact_and_mono_f_iff_f_is_kernel |>.2 ⟨KernelFork.mapIsLimit _ hS.fIsKernel F⟩
  tfae_finish

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f g : Subobject A
⊢ IsPullback ((f ⊓ g).ofLE f ⋯) ((f ⊓ g).ofLE g ⋯) f.arrow g.arrow

Tactic:
refine ⟨⟨by simp⟩, ⟨PullbackCone.IsLimit.mk _ (fun s ↦ (f ⊓ g).factorThru (s.fst ≫ f.arrow) ?_)
    ?_ (fun s ↦ ?_) fun _ _ h _ ↦ ?_⟩⟩
  · simpa using ⟨factors_comp_arrow s.fst, by simpa [s.condition] using factors_comp_arrow s.snd⟩
  · cat_disch
  · ext
    simp [s.condition]
  · ext
    simp [← h]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_3 : (∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact) → F.PreservesHomology
hF : ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact
S : ShortComplex C
hS : S.ShortExact
this✝ : Mono (S.map F).f
this : Epi (S.map F).g
⊢ (S.map F).ShortExact

Tactic:
exact ⟨hF S hS.exact⟩

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

Goal state before:
pp: case insert
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : a✝¹ ∉ s✝
ih : (∃ i ∈ s✝, (P i).Factors f) → (s✝.sup P).Factors f
⊢ (∃ i ∈ insert a✝¹ s✝, (P i).Factors f) → ((insert a✝¹ s✝).sup P).Factors f

Tactic:
rintro ⟨j, ⟨m, h⟩⟩

Goal state after:
case insert
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : a✝¹ ∉ s✝
ih : (∃ i ∈ s✝, (P i).Factors f) → (s✝.sup P).Factors f
j : I
m : j ∈ insert a✝¹ s✝
h : (P j).Factors f
⊢ ((insert a✝¹ s✝).sup P).Factors f
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case f.refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
⊢ (b : ↑(⇑(equivShrink (Subobject A)) '' s)) → underlying.obj ((equivShrink (Subobject A)).symm ↑b) ⟶ underlying.obj f

Tactic:
rintro ⟨g, m⟩

Goal state after:
case f.refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
g : Shrink.{w, max u₁ v₁} (Subobject A)
m : g ∈ ⇑(equivShrink (Subobject A)) '' s
⊢ underlying.obj ((equivShrink (Subobject A)).symm ↑⟨g, m⟩) ⟶ underlying.obj f
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mp
C : Type u_1
H : Type u_3
D : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
φ : F' ⟶ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft φ = α'
inst✝ : F'.IsLeftKanExtension α
a✝ : F''.IsLeftKanExtension α'
⊢ IsIso φ

Tactic:
rw [F'.hom_ext_of_isLeftKanExtension α φ (leftKanExtensionUnique _ α _ α').hom
      (by simp [comm])]

Goal state after:
case mp
C : Type u_1
H : Type u_3
D : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
φ : F' ⟶ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft φ = α'
inst✝ : F'.IsLeftKanExtension α
a✝ : F''.IsLeftKanExtension α'
⊢ IsIso (F'.leftKanExtensionUnique α F'' α').hom
Module: Mathlib.CategoryTheory.Limits.Shapes.Countable

Goal state before:
pp: J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsFiltered J
j : J
⊢ ∃ n, j ≤ sequentialFunctor_obj J n

Tactic:
by
  obtain ⟨m, h⟩ := (exists_surjective_nat _).choose_spec j
  refine ⟨m + 1, ?_⟩
  simpa only [h] using! leOfHom (IsFilteredOrEmpty.cocone_objs ((exists_surjective_nat _).choose m)
    (sequentialFunctor_obj J m)).choose_spec.choose

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

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ (cokernelOrderHom X).comp (kernelOrderHom X) = OrderHom.id

Tactic:
refine OrderHom.ext _ _ (funext (Subobject.ind _ ?_))

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ ∀ ⦃A : Cᵒᵖ⦄ (f : A ⟶ op X) [inst : Mono f],
    ((cokernelOrderHom X).comp (kernelOrderHom X)) (Subobject.mk f) = OrderHom.id (Subobject.mk f)
Module: Mathlib.CategoryTheory.Abelian.Subobject

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ (kernelOrderHom X).comp (cokernelOrderHom X) = OrderHom.id

Tactic:
refine OrderHom.ext _ _ (funext (Subobject.ind _ ?_))

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ ∀ ⦃A : C⦄ (f : A ⟶ X) [inst : Mono f],
    ((kernelOrderHom X).comp (cokernelOrderHom X)) (Subobject.mk f) = OrderHom.id (Subobject.mk f)
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:
rw [isIso_iff_yoneda_map_bijective] at h

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.Types.Coproducts

Goal state before:
pp: case left
C : Type u
F : C → Type v
c : CofanTypes F
h₁ : ∀ (x : c.pt), ∃ i y, c.inj i y = x
h₂ : ∀ (i : C), Function.Injective (c.inj i)
h₃ : ∀ (i j : C) (x : F i) (y : F j), c.inj i x = c.inj j y → i = j
i : C
x y : (Discrete.functor F).obj { as := i }
h :
  (Discrete.functor F).descColimitType c ((Discrete.functor F).ιColimitType { as := i } x) =
    (Discrete.functor F).descColimitType c ((Discrete.functor F).ιColimitType { as := i } y)
⊢ (Discrete.functor F).ιColimitType { as := i } x = (Discrete.functor F).ιColimitType { as := i } y

Tactic:
obtain rfl := h₂ _ h

Goal state after:
case left
C : Type u
F : C → Type v
c : CofanTypes F
h₁ : ∀ (x : c.pt), ∃ i y, c.inj i y = x
h₂ : ∀ (i : C), Function.Injective (c.inj i)
h₃ : ∀ (i j : C) (x : F i) (y : F j), c.inj i x = c.inj j y → i = j
i : C
x : (Discrete.functor F).obj { as := i }
h :
  (Discrete.functor F).descColimitType c ((Discrete.functor F).ιColimitType { as := i } x) =
    (Discrete.functor F).descColimitType c ((Discrete.functor F).ιColimitType { as := i } x)
⊢ (Discrete.functor F).ιColimitType { as := i } x = (Discrete.functor F).ιColimitType { as := i } x
Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal

Goal state before:
pp: G H : GrpCat
p : ↑G
q : ↑H
⊢ (hom (Functor.LaxMonoidal.μ (forget GrpCat) G H)) (p, q) = (p, q)

Tactic:
by
  apply Prod.ext
  · exact congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_fst (forget GrpCat.{u}) G H) (p, q)
  · exact congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_snd (forget GrpCat.{u}) G H) (p, q)

Goal state after:
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
  obtain ⟨g, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective g
  simp [shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm.{w}]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
X Y : Type u
f : X ⟶ Y
inst✝ : Mono f
⊢ Injective ⇑(ConcreteCategory.hom (BinaryCofan.mk f (↾Subtype.val)).inl) ∧
    Injective ⇑(ConcreteCategory.hom (BinaryCofan.mk f (↾Subtype.val)).inr) ∧
      IsCompl (Set.range ⇑(ConcreteCategory.hom (BinaryCofan.mk f (↾Subtype.val)).inl))
        (Set.range ⇑(ConcreteCategory.hom (BinaryCofan.mk f (↾Subtype.val)).inr))

Tactic:
refine ⟨(mono_iff_injective f).mp inferInstance, Subtype.val_injective, ?_⟩

Goal state after:
C : Type u
F : C → Type v
X Y : Type u
f : X ⟶ Y
inst✝ : Mono f
⊢ IsCompl (Set.range ⇑(ConcreteCategory.hom (BinaryCofan.mk f (↾Subtype.val)).inl))
    (Set.range ⇑(ConcreteCategory.hom (BinaryCofan.mk f (↾Subtype.val)).inr))
Module: Mathlib.Order.Circular

Goal state before:
pp: α : Type u_1
inst✝ : CircularOrder α
a b x✝ : α
⊢ x✝ ∈ (cIcc a b)ᶜ ↔ ¬btw a x✝ b

Tactic:
cIcc,

Goal state after:
α : Type u_1
inst✝ : CircularOrder α
a b x✝ : α
⊢ x✝ ∈ {x | btw a x b}ᶜ ↔ ¬btw a x✝ b
Module: Mathlib.Order.Circular

Goal state before:
pp: α : Type u_1
inst✝ : CircularOrder α
a b x✝ : α
⊢ x✝ ∈ (cIoo a b)ᶜ ↔ btw b x✝ a

Tactic:
btw_iff_not_sbtw,

Goal state after:
α : Type u_1
inst✝ : CircularOrder α
a b x✝ : α
⊢ x✝ ∈ (cIoo a b)ᶜ ↔ ¬sbtw a x✝ b
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : NonAssocSemiring α
h : Periodic f c
n : ℕ
⊢ Periodic f (↑n * c)

Tactic:
simpa only [nsmul_eq_mul] using h.nsmul n

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

Goal state before:
pp: n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ (filter p (Ico n (n + a))).card = count p a

Tactic:
by
  rw [count_eq_card_filter_range, Finset.card, Finset.filter_val, Finset.range_val, ←
    multiset_Ico_map_mod n, ← map_count_True_eq_filter_card, ← map_count_True_eq_filter_card,
    map_map]
  congr; funext n
  exact (pp.map_mod_nat n).symm

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

Goal state before:
pp: n : ℕ
this : ∃ x < n + 1, (n + 1).gcd x = 1
⊢ φ (n + 1) = 0 ↔ n + 1 = 0

Tactic:
by simpa [totient, filter_eq_empty_iff]

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
⊢ ↑F ⊆ S → ⋂₀ ↑F ∈ S

Tactic:
refine Finset.induction_on F (fun _ => ?_) ?_

Goal state after:
case refine_1
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
x✝ : ↑∅ ⊆ S
⊢ ⋂₀ ↑∅ ∈ S

case refine_2
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
⊢ ∀ (a : Set α) (s : Finset (Set α)), a ∉ s → (↑s ⊆ S → ⋂₀ ↑s ∈ S) → ↑(insert a s) ⊆ S → ⋂₀ ↑(insert a s) ∈ S
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case inr.i_surj
d : ℕ
hd0 : d > 0
x q : ℕ
hb1 : d * q < d * x
hb2 : d * x.gcd q = d
⊢ x.Coprime q

Tactic:
mul_eq_left hd0.ne'

Goal state after:
case inr.i_surj
d : ℕ
hd0 : d > 0
x q : ℕ
hb1 : d * q < d * x
hb2 : x.gcd q = 1
⊢ x.Coprime q
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:
by
  simp only [eventually_atTop_prod_self, forall_cond_comm]

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

Goal state before:
pp: α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirectedOrder α
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
c : α → α → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun n ↦ List.foldl (fun x n ↦ c x (ys n)) (ys 0) (List.range n)
n : ℕ
⊢ xs (n + 1) = c (xs n) (ys n)

Tactic:
simp [xs, List.range_succ]

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

Tactic:
suffices toIcoDiv hp a (-b) = -toIocDiv hp (-(a + p)) b by
    rwa [neg_add, ← sub_eq_add_neg, toIocDiv_sub_eq_toIocDiv_add', toIocDiv_add_right] at this
  rw [← neg_eq_iff_eq_neg, eq_comm]
  apply toIocDiv_eq_of_sub_zsmul_mem_Ioc
  obtain ⟨hc, ho⟩ := sub_toIcoDiv_zsmul_mem_Ico hp a (-b)
  rw [← neg_lt_neg_iff, neg_sub' (-b), neg_neg, ← neg_smul] at ho
  rw [← neg_le_neg_iff, neg_sub' (-b), neg_neg, ← neg_smul] at hc
  refine ⟨ho, hc.trans_eq ?_⟩
  rw [neg_add, neg_add_cancel_right]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Set α → Filter β
hm : Monotone g
⊢ (f.lift g).NeBot ↔ ∀ s ∈ f, (g s).NeBot

Tactic:
by
  simp only [neBot_iff, Ne, ← empty_mem_iff_bot, mem_lift_sets hm, not_exists, not_and]

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) = p - toIocMod hp (-a) b

Tactic:
simp_rw [toIcoMod, toIocMod, toIcoDiv_neg, neg_smul, add_smul]

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

Tactic:
add_add_add_comm,

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 + (p + -p)
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)
this : l ⊓ 𝓟 s ⊔ 𝓟 sᶜ ≤ comap f (𝓝 x)
⊢ l ≤ comap f (𝓝 x)

Tactic:
sup_inf_right,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)
this : (l ⊔ 𝓟 sᶜ) ⊓ (𝓟 s ⊔ 𝓟 sᶜ) ≤ comap f (𝓝 x)
⊢ l ≤ comap f (𝓝 x)
Module: Mathlib.Algebra.Order.ToIntervalMod

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

Tactic:
add_add_add_comm,

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)) = p + p
⊢ toIcoMod hp b a ≤ toIocMod hp b c ∨ toIcoMod hp b c ≤ toIocMod hp b a
Module: Mathlib.Topology.Order

Goal state before:
pp: case refl.refine_1.inter
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
s✝ t✝ : Set α
a✝¹ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) s✝
a✝ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) t✝
h₁ : s✝ = ∅ ∨ s✝ = univ
h₂ : t✝ = ∅ ∨ t✝ = univ
⊢ s✝ ∩ t✝ = ∅ ∨ s✝ ∩ t✝ = univ

Tactic:
rcases h₁ with (rfl | rfl) <;> rcases h₂ with (rfl | rfl)

Goal state after:
case refl.refine_1.inter.inl.inl
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
a✝¹ a✝ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) ∅
⊢ ∅ ∩ ∅ = ∅ ∨ ∅ ∩ ∅ = univ

case refl.refine_1.inter.inl.inr
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
a✝¹ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) ∅
a✝ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) univ
⊢ ∅ ∩ univ = ∅ ∨ ∅ ∩ univ = univ

case refl.refine_1.inter.inr.inl
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
a✝¹ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) univ
a✝ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) ∅
⊢ univ ∩ ∅ = ∅ ∨ univ ∩ ∅ = univ

case refl.refine_1.inter.inr.inr
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
a✝¹ a✝ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) univ
⊢ univ ∩ univ = ∅ ∨ univ ∩ univ = univ
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace W
inst✝² : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝¹ : TopologicalSpace X'
inst✝ : TopologicalSpace Y'
f : X ≃ₜ Y
g : Y → X
hg : Function.RightInverse g ⇑f
this : g = ⇑f.symm
⊢ Function.RightInverse g ⇑f

Tactic:
convert! f.right_inv using 1

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
open_map : IsOpenMap f
cont : Continuous[inst✝¹, inst✝] f
surj : Surjective f
⊢ IsQuotientMap f

Tactic:
isQuotientMap_iff

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
open_map : IsOpenMap f
cont : Continuous[inst✝¹, inst✝] f
surj : Surjective f
⊢ IsCoinducing f ∧ Surjective f
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
hf : Surjective f
hf' : Continuous[inst✝², inst✝¹] f
hfg : IsClosedMap (g ∘ f)
⊢ IsClosedMap g

Tactic:
intro K hK

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
hf : Surjective f
hf' : Continuous[inst✝², inst✝¹] f
hfg : IsClosedMap (g ∘ f)
K : Set Y
hK : IsClosed[inst✝¹] K
⊢ IsClosed[inst✝] (g '' K)
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
γ : Type u_5
x : X
y : Y
f : Filter γ
mx : γ → X
my : γ → Y
hx : Tendsto mx f (𝓝 x)
hy : Tendsto my f (𝓝 y)
⊢ Tendsto (fun c ↦ (mx c, my c)) f (𝓝 (x, y))

Tactic:
by
  rw [nhds_prod_eq]
  exact hx.prodMk hy

Goal state after:
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 → Z
g : Y → W
x : X
y : Y
⊢ ContinuousAt (Prod.map f g) (x, y) ↔ ContinuousAt f x ∧ ContinuousAt g y

Tactic:
by
  simp [ContinuousAt, nhds_prod_eq, tendsto_iff_comap, comap_prodMap_prod]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X✝ : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
X : Type u_5
s t : Set X
hs : s.Nonempty → sᶜ.Finite
ht : t.Nonempty → tᶜ.Finite
x : X
hxs : x ∈ s
hxt : x ∈ t
⊢ (sᶜ ∪ tᶜ).Finite

Tactic:
exact (hs ⟨x, hxs⟩).union (ht ⟨x, hxt⟩)

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Sort u_5
s : ι → Set α
hs : ∀ (x : α), ∃ i, s i ∈ 𝓝 x
hf : ∀ (i : ι), ContinuousOn f (s i)
x : α
i : ι
hi : s i ∈ 𝓝 x
⊢ ContinuousAt f x

Tactic:
rw [ContinuousAt, ← nhdsWithin_eq_nhds.2 hi]
    exact hf _ _ (mem_of_mem_nhds hi)

Goal state after:
Module: Mathlib.Topology.Constructions

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

Tactic:
rintro ⟨V, hVU, V_op, haV⟩

Goal state after:
case mp
X : Type u
x : CofiniteTopology X
U V : Set (CofiniteTopology X)
hVU : V ⊆ U
V_op : V.Nonempty → Vᶜ.Finite
haV : x ∈ V
⊢ U ∈ pure x ⊔ cofinite
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
x✝ : X × Y
a : X
b : Y
⊢ (𝓝[s] a ×ˢ 𝓝[t] b).NeBot ↔ (𝓝[s] a).NeBot ∧ (𝓝[t] b).NeBot

Tactic:
prod_neBot

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : Finite ι
s : Set ((a : ι) → A a)
val✝ : Fintype ι
a : (a : ι) → A a
x✝¹ : a ∈ s
x✝ : ∃ u, (∀ (a_1 : ι), IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ univ.pi u ⊆ s
u : (a : ι) → Set (A a)
h1 : ∀ (a_1 : ι), IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1
right✝ : univ.pi u ⊆ s
⊢ (↑Finset.univ).pi u ⊆ s

Tactic:
rwa [Finset.coe_univ]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case intro
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
⊢ Pi.topologicalSpace = generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}

Tactic:
rw [pi_generateFrom_eq]

Goal state after:
case intro
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
⊢ generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s} =
    generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2.refine_3
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x✝ : TopologicalSpace β := ⨅ i, t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ i, t i] u
F : Set ι
U : ι → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ ⋂ i ∈ F, U i ⊆ u

Tactic:
exact hUu

Goal state after: