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✝ : HasZeroMorphisms C
S : ShortComplex Cᵒᵖ
h : S.Exact
⊢ S.unop.Exact

Tactic:
obtain ⟨h, z⟩ := h
  exact ⟨⟨h.unop, (IsZero.of_iso z h.iso.symm).unop⟩⟩

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

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : HasZeroMorphisms C
inst✝⁵ : HasZeroMorphisms D
S : ShortComplex C
inst✝⁴ : S.HasHomology
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : F.PreservesLeftHomologyOf S
inst✝¹ : F.PreservesRightHomologyOf S
inst✝ : F.Faithful
h : 𝟙 (F.obj S.leftHomologyData.H) = 0
⊢ F.map (𝟙 S.leftHomologyData.H) = F.map 0

Tactic:
rw [F.map_id, F.map_zero, h]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : kernel.ι S.g ≫ cokernel.π S.f = 0
⊢ IsColimit (CokernelCofork.ofπ (Abelian.coimage.π S.g) ⋯)

Tactic:
refine CokernelCofork.IsColimit.ofπ _ _
    (fun u hu => cokernel.desc (kernel.ι S.g) u
      (by rw [← cokernel.π_desc S.f u hu, ← Category.assoc, h, zero_comp]))
    (by simp) ?_

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : kernel.ι S.g ≫ cokernel.π S.f = 0
⊢ ∀ {Z' : C} (g' : S.X₂ ⟶ Z') (eq' : S.f ≫ g' = 0) (m : Abelian.coimage S.g ⟶ Z'),
    Abelian.coimage.π S.g ≫ m = g' → m = cokernel.desc (kernel.ι S.g) 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
hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact
X Y : A
f : X ⟶ Y
⊢ PreservesLimit (parallelPair f 0) L

Tactic:
have := preservesMonomorphisms_of_map_exact _ hL

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
hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact
X Y : A
f : X ⟶ Y
this : L.PreservesMonomorphisms
⊢ PreservesLimit (parallelPair f 0) L
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
F : C ⥤ H
Y : D
L L' : C ⥤ D
e : L ≅ L'
inst✝ : L.HasPointwiseRightKanExtensionAt F Y
⊢ L'.HasPointwiseRightKanExtensionAt F Y

Tactic:
let Φ : StructuredArrow Y L' ≌ StructuredArrow Y L := Comma.mapRightIso _ e.symm

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
F : C ⥤ H
Y : D
L L' : C ⥤ D
e : L ≅ L'
inst✝ : L.HasPointwiseRightKanExtensionAt F Y
Φ : StructuredArrow Y L' ≌ StructuredArrow Y L := Comma.mapRightIso (fromPUnit Y) e.symm
⊢ L'.HasPointwiseRightKanExtensionAt F Y
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mpr
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
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft e.hom = α'
⊢ F''.IsLeftKanExtension α' → F'.IsLeftKanExtension α

Tactic:
· intro
    refine isLeftKanExtension_of_iso e.symm α' α ?_
    rw [← comm, assoc, ← whiskerLeft_comp, Iso.symm_hom, e.hom_inv_id, whiskerLeft_id', comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Countable

Goal state before:
pp: J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsCofiltered J
j : J
m : ℕ
h : ⋯.choose m = j
⊢ sequentialFunctor_obj J (m + 1) ≤ j

Tactic:
simpa only [h] using! leOfHom (IsCofilteredOrEmpty.cone_objs ((exists_surjective_nat _).choose m)
    (sequentialFunctor_obj J m)).choose_spec.choose

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
f :
  CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
    (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E
x✝¹ x✝ : Cᵒᵖ
g : x✝¹ ⟶ x✝
x : P.obj x✝¹
⊢ uliftYoneda.{max w v₂, v₁, u₁}.map g.unop ≫ (CostructuredArrow.mk (uliftYonedaEquiv.symm x)).hom =
    (CostructuredArrow.mk (uliftYonedaEquiv.symm ((hom (P.map g)) x))).hom

Tactic:
by
              dsimp
              rw [uliftYonedaEquiv_symm_map]

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)
⊢ ∀ (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:
by rintro (_ | _) <;> cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
X : C
f : uliftYoneda.{max w v₂, v₁, u₁}.obj X ⟶ P
⊢ uliftYonedaEquiv (f ≫ presheafHom φ P) =
    (hom ((G.map f).app (op (F.obj X)))) ((hom ((φ.app X).app (op (F.obj X)))) { down := 𝟙 (unop (op (F.obj X))) })

Tactic:
obtain ⟨x, rfl⟩ := uliftYonedaEquiv.symm.surjective f
  erw [(colimitOfRepresentable P).fac _ (Opposite.op (P.elementsMk _ x))]
  dsimp only [coconeApp]
  apply Equiv.apply_symm_apply

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)
inst✝ : Nonempty J
s t : Trident f
k : s.pt ⟶ t.pt
w : k ≫ t.ι = s.ι
⊢ ∀ (j : WalkingParallelFamily J), k ≫ t.π.app j = s.π.app j

Tactic:
rintro ⟨_ | _⟩
    · exact w
    · simpa using w =≫ f (Classical.arbitrary J)

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasProduct fun x ↦ G
h : ∀ (A : C), Mono (Pi.lift fun f ↦ f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f = g

Tactic:
have := h Y

Goal state after:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasProduct fun x ↦ G
h : ∀ (A : C), Mono (Pi.lift fun f ↦ f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
this : Mono (Pi.lift fun f ↦ f)
⊢ f = g
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : NonAssocSemiring α
inst✝ : NegZeroClass β
h : Antiperiodic f c
hi : f 0 = 0
n : ℕ
⊢ f (↑(n + 1) * c) = 0

Tactic:
simp [add_mul, h _, Antiperiodic.nat_mul_eq_of_eq_zero h hi n]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddGroup α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
n : ℕ
⊢ f (x - n • c) = (-1) ^ n • f x

Tactic:
simpa only [Int.reduceNeg, natCast_zsmul] using! h.sub_zsmul_eq n

Goal state after:
Module: Mathlib.Data.Nat.Cast.Field

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

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

Tactic:
· simp [Nat.zero_dvd.1 hm]

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
a k : ℕ
h : 0 < count (fun k ↦ p (a + k)) (k + 1)
t : ℕ
ht : t < k + 1
hp : p (a + t)
⊢ ∃ x ∈ Set.Ico a (a + k + 1), p x

Tactic:
Set.mem_Ico

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
a k : ℕ
h : 0 < count (fun k ↦ p (a + k)) (k + 1)
t : ℕ
ht : t < k + 1
hp : p (a + t)
⊢ ∃ x, (a ≤ x ∧ x < a + k + 1) ∧ p x
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: 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
⊢ f 1 = (factorization 1).prod fun p k ↦ f (p ^ k)

Tactic:
factorization_one,

Goal state after:
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
⊢ f 1 = Finsupp.prod 0 fun p k ↦ f (p ^ k)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: m n : ℕ
h : m.Coprime n
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
⊢ Fintype.card (ZMod m × ZMod n)ˣ = Fintype.card (ZMod m)ˣ * Fintype.card (ZMod n)ˣ

Tactic:
Fintype.card_congr (@MulEquiv.prodUnits (ZMod m) (ZMod n) _ _).toEquiv,

Goal state after:
m n : ℕ
h : m.Coprime n
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
⊢ Fintype.card ((ZMod m)ˣ × (ZMod n)ˣ) = Fintype.card (ZMod m)ˣ * Fintype.card (ZMod n)ˣ
Module: Mathlib.Data.Set.Constructions

Goal state before:
pp: α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P : Set α
H : P ∈ finiteInterClosure (insert A S)
⊢ P ∈ S ∨ ∃ Q ∈ S, P = A ∩ Q

Tactic:
induction H with

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

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x ↦ x * p
b : ℕ
h : b < p ^ n
⊢ b * p < p ^ n * p

Tactic:
exact (mul_lt_mul_iff_left₀ hp.pos).2 h

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

Goal state before:
pp: p : ℕ
inst✝ : Fintype (ZMod p)ˣ
⊢ Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1

Tactic:
rcases eq_zero_or_neZero p with rfl | hp
  · simp [ZMod, not_prime_zero, zero_tsub]
  rw [ZMod.card_units_eq_totient, Nat.totient_eq_iff_prime <| NeZero.pos p]

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

Goal state before:
pp: n : ℕ
⊢ ↑(φ n) = ↑n * ∏ p ∈ n.primeFactors, (1 - (↑p)⁻¹)

Tactic:
by
  by_cases hn : n = 0
  · simp [hn]
  have hn' : (n : ℚ) ≠ 0 := by simp [hn]
  have hpQ : (∏ p ∈ n.primeFactors, (p : ℚ)) ≠ 0 := by
    rw [← cast_prod, cast_ne_zero, ← zero_lt_iff, prod_primeFactors_prod_factorization]
    exact prod_pos fun p hp => pos_of_mem_primeFactors hp
  simp only [totient_eq_div_primeFactors_mul n, prod_primeFactors_dvd n, cast_mul, cast_prod,
    cast_div_charZero, mul_comm_div, mul_right_inj' hn', div_eq_iff hpQ, ← prod_mul_distrib]
  refine prod_congr rfl fun p hp => ?_
  have hp := pos_of_mem_primeFactorsList (List.mem_toFinset.mp hp)
  have hp' : (p : ℚ) ≠ 0 := cast_ne_zero.mpr hp.ne.symm
  rw [sub_mul, one_mul, mul_comm, mul_inv_cancel₀ hp', cast_pred hp]

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

Goal state before:
pp: case pos
a b : ℕ
h : a ∣ b
h' : φ a = φ b
ha : a = 0
⊢ a = b ∨ 2 * a = b

Tactic:
rw [ha, totient_zero, eq_comm, totient_eq_zero] at h'
    simp [ha, h']

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

Tactic:
rw [sub_smul, ← sub_add, add_right_comm]

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

Tactic:
rw [sub_smul, ← sub_add, add_right_comm]

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

Tactic:
simpa only [neg_neg] using toIcoMod_neg hp (-a) (-b)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α × α → β
x : Filter α
y : Filter β
⊢ Tendsto f (x ×ˢ x) y ↔ ∀ W ∈ y, ∃ U ∈ x, ∀ (x x' : α), x ∈ U → x' ∈ U → f (x, x') ∈ W

Tactic:
by
  simp only [tendsto_def, mem_prod_same_iff, prod_sub_preimage_iff]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : closure s ⊆ s
⊢ IsClosed s

Tactic:
rw [subset_closure.antisymm h]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : closure s ⊆ s
⊢ IsClosed (closure s)
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ frontier (s ∩ t) ⊆ frontier s ∩ closure t ∪ closure s ∩ frontier t

Tactic:
by
  simp only [frontier_eq_closure_inter_closure, compl_inter, closure_union]
  refine (inter_subset_inter_left _ (closure_inter_subset_inter_closure s t)).trans_eq ?_
  simp only [inter_union_distrib_left, inter_assoc,
    inter_comm (closure t)]

Goal state after:
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 : ∀ a ∉ s, f a = x✝
U : Set α
t : Set X
ht : t ∈ 𝓝 x✝
htU : f ⁻¹' t ⊆ U
x : α
hx : x ∈ sᶜ
⊢ x ∈ U

Tactic:
have : f x ∈ t := (h x hx).symm ▸ mem_of_mem_nhds ht

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
α : Type u_1
x✝ : X
f : α → X
l : Filter α
s : Set α
h : ∀ a ∉ s, f a = x✝
U : Set α
t : Set X
ht : t ∈ 𝓝 x✝
htU : f ⁻¹' t ⊆ U
x : α
hx : x ∈ sᶜ
this : f x ∈ t
⊢ x ∈ U
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed s
⊢ closure s \ interior s = s \ interior s

Tactic:
hs.closure_eq

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed s
⊢ s \ interior s = s \ interior s
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 = toIocMod hp a b} = ⋃ z, Set.Ioo (a + z • p) (a + p + z • p)

Tactic:
ext1
  simp_rw [Set.mem_ofPred, Set.mem_iUnion, ← Set.sub_mem_Ioo_iff_left, ←
    not_modEq_iff_toIcoMod_eq_toIocMod, modEq_iff_forall_notMem_Ioo_mod hp, not_forall,
    Classical.not_not]

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: case mpr
X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
h : (pure x ⊓ F.lift' closure[inst✝]).NeBot
U : Set X
hU : U ∈ F.lift' closure[inst✝]
⊢ U ∈ pure x

Tactic:
simp_rw [← forall_mem_nonempty_iff_neBot, mem_inf_iff] at h

Goal state after:
case mpr
X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
U : Set X
hU : U ∈ F.lift' closure[inst✝]
h : ∀ (s : Set X), (∃ t₁ ∈ pure x, ∃ t₂ ∈ F.lift' closure[inst✝], s = t₁ ∩ t₂) → s.Nonempty
⊢ U ∈ pure x
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
m : ℤ
⊢ toIocMod hp (a - ↑m * p) b = toIocMod hp a b - ↑m * p

Tactic:
simpa using toIocMod_sub_zsmul' hp a b m

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: case inr
α : Type u
inst✝ : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b a : α
s : Set α
hs : s ∈ update pure a₀ l a
ha : a ≠ a₀
⊢ ∀ᶠ (y : α) in update pure a₀ l a, s ∈ update pure a₀ l y

Tactic:
· simpa only [update_of_ne ha, mem_pure, eventually_pure] using hs

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

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

Tactic:
by
  simp_rw [isEmbedding_iff, hg.isInducing.of_comp_iff, hg.injective.of_comp_iff f]

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
h₁ : IsOpenMap f
h₂ : Injective f
h₃ : Continuous[inst✝¹, inst✝] f
s : Set X
hs' : IsClosed[inst✝¹] s
⊢ f ⁻¹' closure[inst✝] (f '' s) = s

Tactic:
rw [h₁.preimage_closure_eq_closure_preimage h₃, Set.preimage_image_eq _ h₂, hs'.closure_eq]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
s : Set X
t : Set Y
⊢ 𝓝[s ×ˢ t] (x, y) = 𝓝[s] x ×ˢ 𝓝[t] y

Tactic:
simp only [nhdsWithin, nhds_prod_eq, ← prod_inf_prod, prod_principal_principal]

Goal state after:
Module: Mathlib.Topology.Constructions

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

Tactic:
by
  rw [mapClusterPt_iff_frequently] at hf hg
  rw [((𝓝 x).basis_sets.prod_nhds (𝓝 y).basis_sets).mapClusterPt_iff_frequently]
  rintro ⟨s, t⟩ ⟨hs, ht⟩
  rw [frequently_curry_iff]
  exact (hf s hs).mono fun x hx ↦ (hg t ht).mono fun y hy ↦ ⟨hx, hy⟩

Goal state after:
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
hx : x ∉ s
⊢ x ∉ closure[inst✝¹] s

Tactic:
hs.closure_eq

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 ∉ s
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_2
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I).pi t ⊆ s
⊢ ∃ I t, (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1) ∧ (↑I).pi t ⊆ s

Tactic:
refine ⟨I, fun a => ite (a ∈ I) (t a) univ, fun i => ?_, ?_⟩

Goal state after:
case refine_2.refine_1
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I).pi t ⊆ s
i : ι
⊢ ∃ t_1 ⊆ (fun a ↦ if a ∈ I then t a else univ) i, IsOpen[T i] t_1 ∧ a i ∈ t_1

case refine_2.refine_2
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I).pi t ⊆ s
⊢ ((↑I).pi fun a ↦ if a ∈ I then t a else univ) ⊆ s
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
⊢ IsOpenMap f ↔ ∀ (i : ι), IsOpenMap fun a ↦ f ⟨i, a⟩

Tactic:
by
  simp only [isOpenMap_iff_nhds_le, Sigma.forall, Sigma.nhds_eq, map_map, comp_def]

Goal state after:
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : SigmaCompactSpace X
e : Y → X
he : IsClosedEmbedding e
⊢ e ⁻¹' univ = univ

Tactic:
preimage_univ

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : SigmaCompactSpace X
e : Y → X
he : IsClosedEmbedding e
⊢ univ = univ
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ ⊤ ≤ upperClosure s ↔ s = ∅

Tactic:
le_upperClosure

Goal state after:
α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ s ⊆ ↑⊤ ↔ s = ∅
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
hs : IsLowerSet s
⊢ Disjoint s ↑(upperClosure t) ↔ Disjoint s t

Tactic:
by
  simpa only [disjoint_comm] using hs.disjoint_upperClosure_left

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
⊢ s.sdiff t ⊓ upperClosure t = s

Tactic:
sdiff_inf_upperClosure hts hst

Goal state after:
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
⊢ s = s
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
f : ι → X
x : X
hf : Tendsto f cofinite (𝓝 x)
⊢ IsCompact (insert x (range f))

Tactic:
let : TopologicalSpace ι := ⊥

Goal state after:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
f : ι → X
x : X
hf : Tendsto f cofinite (𝓝 x)
this : TopologicalSpace ι := ⊥
⊢ IsCompact (insert x (range f))
Module: Mathlib.Topology.Inseparable

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

Tactic:
simp only [GeneralizingMap_iff_stableUnderGeneralization_image, Set.image_comp] at *

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : ∀ (s : Set X), StableUnderGeneralization s → StableUnderGeneralization (f '' s)
hg : ∀ (s : Set Y), StableUnderGeneralization s → StableUnderGeneralization (g '' s)
⊢ ∀ (s : Set X), StableUnderGeneralization s → StableUnderGeneralization (g '' f '' s)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty { U // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
⊢ (⋃₀ c)ᶜ = ⋂ U, (↑U)ᶜ

pp: case h.refine_3
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty { U // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
⊢ (⋂ U, (↑U)ᶜ).Nonempty

Tactic:
· ext
            simp only [not_exists, not_and, Set.mem_iInter, Subtype.forall,
              mem_compl_iff, mem_sUnion]

Goal state after:
case h.refine_3
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty { U // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
⊢ (⋂ U, (↑U)ᶜ).Nonempty