mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : uliftYoneda.{max w v₂, v₁, u₁}.LeftExtension (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
f g : Functor.LeftExtension.mk F.op.lan (compULiftYonedaIsoULiftYonedaCompLan F).hom ⟶ Φ
P : Cᵒᵖ ⥤ Type (max (max w v₁) v₂)
x : P.Elementsᵒᵖ
⊢ (coconeOfRepresentable P).ι.app x ≫ F.op.lanUnit.app P ≫ F.op.whiskerLeft ((StructuredArrow.Hom.right f).app P) =
    (coconeOfRepresentable P).ι.app x ≫ F.op.lanUnit.app P ≫ F.op.whiskerLeft ((StructuredArrow.Hom.right g).app P)

Tactic:
have eq := F.op.lanUnit.naturality (uliftYonedaEquiv.{max w v₂}.symm x.unop.2)

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : uliftYoneda.{max w v₂, v₁, u₁}.LeftExtension (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
f g : Functor.LeftExtension.mk F.op.lan (compULiftYonedaIsoULiftYonedaCompLan F).hom ⟶ Φ
P : Cᵒᵖ ⥤ Type (max (max w v₁) v₂)
x : P.Elementsᵒᵖ
eq :
  (𝟭 (Cᵒᵖ ⥤ Type (max (max w v₂) v₁))).map (uliftYonedaEquiv.symm (unop x).snd) ≫ F.op.lanUnit.app P =
    F.op.lanUnit.app (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).1)) ≫
      (F.op.lan ⋙ (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max (max w v₂) v₁))).obj F.op).map
        (uliftYonedaEquiv.symm (unop x).snd)
⊢ (coconeOfRepresentable P).ι.app x ≫ F.op.lanUnit.app P ≫ F.op.whiskerLeft ((StructuredArrow.Hom.right f).app P) =
    (coconeOfRepresentable P).ι.app x ≫ F.op.lanUnit.app P ≫ F.op.whiskerLeft ((StructuredArrow.Hom.right g).app P)
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case mpr.refine_4
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)
⊢ ∀ {T : Type u} (f : X ⟶ T) (g : Y ⟶ T) (m : c.pt ⟶ T),
    c.inl ≫ m = f →
      c.inr ≫ m = g →
        m =
          ↾fun x ↦
            if h : x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) then
              (ConcreteCategory.hom f) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨x, h⟩)
            else (ConcreteCategory.hom g) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inr)) h₂).symm ⟨x, ⋯⟩)

Tactic:
· rintro T _ _ m rfl rfl
        ext x
        simp only [TypeCat.Fun.toFun_apply, Functor.const_obj_obj, pair_obj_left, Set.mem_range,
          comp_apply, pair_obj_right, ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk]
        split_ifs <;> exact congr_arg _ (Equiv.apply_ofInjective_symm _ ⟨_, _⟩).symm

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

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

Tactic:
← Int.not_odd_iff_even

Goal state after:
case mp
n : ℤ
h : n.negOnePow = 1
⊢ ¬Odd n
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: n : ℤ
⊢ n.negOnePow = -1 ↔ Odd n

Tactic:
constructor
  · intro h
    rw [← Int.not_even_iff_odd]
    intro h'
    rw [negOnePow_even _ h'] at h
    contradiction
  · exact negOnePow_odd n

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

Goal state before:
pp: case neg
n₁ n₂ : ℤ
h₂ : Odd n₂
⊢ Odd n₁ ↔ (¬Odd n₁ ↔ Even n₂)

Tactic:
← Int.not_odd_iff_even

Goal state after:
case neg
n₁ n₂ : ℤ
h₂ : Odd n₂
⊢ Odd n₁ ↔ (¬Odd n₁ ↔ ¬Odd n₂)
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
c : α
inst✝¹ : Add α
inst✝ : MulOneClass β
g : α → β
l : List (α → β)
ih : (∀ f ∈ l, Periodic f c) → Periodic l.prod c
hl : ∀ f ∈ g :: l, Periodic f c
⊢ Periodic (g :: l).prod c

Tactic:
List.forall_mem_cons

Goal state after:
case cons
α : Type u_1
β : Type u_2
c : α
inst✝¹ : Add α
inst✝ : MulOneClass β
g : α → β
l : List (α → β)
ih : (∀ f ∈ l, Periodic f c) → Periodic l.prod c
hl : Periodic g c ∧ ∀ x ∈ l, Periodic x c
⊢ Periodic (g :: l).prod c
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst✝ : AddGroup α
h1 : Periodic f c₁
h2 : Periodic f c₂
x : α
⊢ f (x + (c₁ - c₂)) = f x

Tactic:
rw [sub_eq_add_neg, ← add_assoc, h2.neg, h1]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddCommSemigroup α
h : Periodic f c
a x : α
⊢ (fun x ↦ f (x + a)) (x + c) = (fun x ↦ f (x + a)) x

Tactic:
by
  simpa only [add_right_comm] using h (x + a)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddCommSemigroup α
inst✝ : Neg β
h : Antiperiodic f c
a x : α
⊢ (fun x ↦ f (x + a)) (x + c) = -(fun x ↦ f (x + a)) x

Tactic:
by
  simpa only [add_right_comm] using h (x + a)

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
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
⊢ extensionToFun i f h x = ↑(extensionOfMax i f).toLinearPMap ⟨a, ha⟩ + (extendIdealTo i f h y) r

Tactic:
have eq3 :=
    ExtensionOfMaxAdjoin.extendIdealTo_eq i f h (r - ExtensionOfMaxAdjoin.snd i x)
      (by rw [← eq2]; exact Submodule.sub_mem _ (ExtensionOfMaxAdjoin.fst i x).2 ha)

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 - snd i x) = ↑(extensionOfMax i f).toLinearPMap ⟨(r - snd i x) • y, ⋯⟩
⊢ extensionToFun i f h x = ↑(extensionOfMax i f).toLinearPMap ⟨a, ha⟩ + (extendIdealTo i f h y) r
Module: Mathlib.Data.Nat.Cast.Field

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

Tactic:
rcases eq_or_ne d 0 with (rfl | hd); · simp [Nat.zero_dvd.1 hm]
  replace hd : (d : K) ≠ 0 := by norm_cast
  rw [cast_div hm, cast_div hn, div_div_div_cancel_right₀ hd] <;> exact hd

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count (fun k ↦ p (k + 1)) n + count p 1 = count (fun k ↦ p (k + 1)) n + if p 0 then 1 else 0

Tactic:
count_one

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ (count (fun k ↦ p (k + 1)) n + if p 0 then 1 else 0) = count (fun k ↦ p (k + 1)) n + if p 0 then 1 else 0
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: case succ
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime_mul : ∀ (p a : ℕ), Prime p → motive a → motive (p * a)
a p : ℕ
hp : Prime p
ha : motive a
n : ℕ
ih : motive (p ^ n * a)
⊢ motive (p * p ^ n * a)

Tactic:
mul_assoc

Goal state after:
case succ
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime_mul : ∀ (p a : ℕ), Prime p → motive a → motive (p * a)
a p : ℕ
hp : Prime p
ha : motive a
n : ℕ
ih : motive (p ^ n * a)
⊢ motive (p * (p ^ n * a))
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case mp
m n : ℕ
⊢ ¬(Odd (φ m) ∨ Odd (φ n)) → ¬(φ m).Coprime (φ n)

Tactic:
not_or,

Goal state after:
case mp
m n : ℕ
⊢ ¬Odd (φ m) ∧ ¬Odd (φ n) → ¬(φ m).Coprime (φ n)
Module: Mathlib.Data.Nat.Totient

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

Tactic:
by
  constructor
  · rw [← not_imp_not]
    simp_rw [← odd_totient_iff, not_or, not_odd_iff_even, even_iff_two_dvd]
    exact fun h ↦ Nat.not_coprime_of_dvd_of_dvd one_lt_two h.1 h.2
  · simp_rw [← totient_eq_one_iff]
    rintro (h | h) <;> rw [h]
    exacts [Nat.coprime_one_left _, Nat.coprime_one_right _]

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

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

Tactic:
rw [shuffle, shuffle]

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

case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ a.primeFactors, p ∣ a

case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ b.primeFactors, p ∣ b

case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ (a.gcd b).primeFactors, p ∣ a.gcd b

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

Goal state before:
pp: a b : ℕ
d : ℕ := ⋯
ha0 : a > 0
hd0 : 0 < d
⊢ φ a * φ b * d ≤ φ (a * b) * d

Tactic:
grw [← totient_gcd_mul_totient_mul a b, mul_comm, d.totient_le]

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

Goal state before:
pp: p n : ℕ
hp : Prime p
h : p ∣ n
h1 : φ p * φ (p * n) = φ p * φ n * p
⊢ φ (p * n) = p * φ n

Tactic:
mul_assoc

Goal state after:
p n : ℕ
hp : Prime p
h : p ∣ n
h1 : φ p * φ (p * n) = φ p * (φ n * p)
⊢ φ (p * n) = p * φ n
Module: Mathlib.Data.Nat.Totient

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

Tactic:
Nat.lt_mul_iff_one_lt_left

Goal state after:
case neg.refine_1
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
⊢ 1 < p

case neg.refine_1
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
⊢ 0 < φ a
Module: Mathlib.Data.Nat.Totient

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

Tactic:
mul_assoc

Goal state after:
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
⊢ a * (p * d) ≠ 0
Module: Mathlib.Topology.Basic

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

Tactic:
| empty =>

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
s₁ s₂ : Set X
inst✝ : TopologicalSpace X
h₁ : IsOpen[inst✝] s₁ᶜ
h₂ : IsOpen[inst✝] s₂ᶜ
⊢ IsOpen[inst✝] (s₁ ∩ s₂)ᶜ

Tactic:
rw [compl_inter]

Goal state after:
X : Type u
s₁ s₂ : Set X
inst✝ : TopologicalSpace X
h₁ : IsOpen[inst✝] s₁ᶜ
h₂ : IsOpen[inst✝] s₂ᶜ
⊢ IsOpen[inst✝] (s₁ᶜ ∪ s₂ᶜ)
Module: Mathlib.Topology.Closure

Goal state before:
pp: case empty
X : Type u
inst✝ : TopologicalSpace X
ι : Type u_1
s : Set ι
f : ι → Set X
⊢ interior (⋂ i ∈ ∅, f i) = ⋂ i ∈ ∅, interior (f i)

Tactic:
| empty =>

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

Tactic:
(zsmul_left_strictMono hp).le_iff_le

Goal state after:
α : 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
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
⊢ ClusterPt x (𝓟 C) → x ∈ C ∨ AccPt x (𝓟 C)

Tactic:
intro h
    by_contra! hc
    rw [accPt_principal_iff_clusterPt] at hc
    simp_all only [not_false_eq_true, sdiff_singleton_eq_self, not_true_eq_false, hc.1]

Goal state after:
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 : α
⊢ ⋃ n, Ioc (a + n • p) (a + (n + 1) • p) = univ

Tactic:
refine eq_univ_iff_forall.mpr fun b => mem_iUnion.mpr ?_

Goal state after:
α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ ∃ i, b ∈ Ioc (a + i • p) (a + (i + 1) • 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 : α
⊢ ⋃ n, Ico (a + n • p) (a + (n + 1) • p) = univ

Tactic:
refine eq_univ_iff_forall.mpr fun b => mem_iUnion.mpr ?_

Goal state after:
α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ ∃ i, b ∈ Ico (a + i • p) (a + (i + 1) • p)
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ n, u n
u_props : ∀ (n : ℕ), IsOpen[inst✝] (u n) ∧ Disjoint (closure[inst✝] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ n, v n
v_props : ∀ (n : ℕ), IsOpen[inst✝] (v n) ∧ Disjoint (closure[inst✝] (v n)) s
open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst✝] (u₀ n)) → IsOpen[inst✝] (⋃ n, u₀ n \ closure[inst✝] (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ n, u₀ n →
      (∀ (n : ℕ), Disjoint (closure[inst✝] (v₀ n)) h₀) → h₀ ⊆ ⋃ n, u₀ n \ closure[inst✝] (⋃ m, ⋃ (_ : m ≤ n), v₀ m)
x : X
n : ℕ
xinun : x ∈ (fun n ↦ u n \ closure[inst✝] (⋃ m, ⋃ (_ : m ≤ n), v m)) n
m : ℕ
⊢ x ∈ v m → x ∈ closure[inst✝] (⋃ m' ∈ {m' | m' ≤ m}, u m')

Tactic:
xinvm

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ n, u n
u_props : ∀ (n : ℕ), IsOpen[inst✝] (u n) ∧ Disjoint (closure[inst✝] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ n, v n
v_props : ∀ (n : ℕ), IsOpen[inst✝] (v n) ∧ Disjoint (closure[inst✝] (v n)) s
open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst✝] (u₀ n)) → IsOpen[inst✝] (⋃ n, u₀ n \ closure[inst✝] (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ n, u₀ n →
      (∀ (n : ℕ), Disjoint (closure[inst✝] (v₀ n)) h₀) → h₀ ⊆ ⋃ n, u₀ n \ closure[inst✝] (⋃ m, ⋃ (_ : m ≤ n), v₀ m)
x : X
n : ℕ
xinun : x ∈ (fun n ↦ u n \ closure[inst✝] (⋃ m, ⋃ (_ : m ≤ n), v m)) n
m : ℕ
xinvm : x ∈ v m
⊢ x ∈ closure[inst✝] (⋃ m' ∈ {m' | m' ≤ m}, u m')
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 : ∀ (x : X) (l : Filter Y), ClusterPt (f x) l → ClusterPt x (comap f l)
⊢ IsOpenMap f

Tactic:
simp only [isOpenMap_iff_nhds_le, le_map_iff]

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (x : X) (l : Filter Y), ClusterPt (f x) l → ClusterPt x (comap f l)
⊢ ∀ (x : X), ∀ s ∈ 𝓝 x, f '' s ∈ 𝓝 (f x)
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 Y} (x : Set X), s ⊆ kernImage f (interior x) → s ⊆ interior (kernImage f x)

Tactic:
isClosedMap_iff_kernImage_interior

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ (∀ {s : Set X}, kernImage f (interior s) ⊆ interior (kernImage f s)) ↔
    ∀ {s : Set Y} (x : Set X), s ⊆ kernImage f (interior x) → s ⊆ interior (kernImage f x)
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Z : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
α : Type u_5
f : X → α → Z
s : Set α
t : Set Z
ht : IsClosed[inst✝] t
hf : ∀ a ∈ s, Continuous[inst✝¹, inst✝] fun x ↦ f x a
⊢ IsClosed[inst✝¹] {x | MapsTo (f x) s t}

Tactic:
by
  simpa only [MapsTo, ofPred_forall] using! isClosed_biInter fun y hy ↦ ht.preimage (hf y 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
ε : Type u_3
ζ : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : TopologicalSpace Z
inst✝⁴ : TopologicalSpace W
inst✝³ : TopologicalSpace ε
inst✝² : TopologicalSpace ζ
inst✝¹ : Preorder X
inst✝ : Preorder Y
x : X × Y
hx₁ : (𝓝[<] x.1).NeBot
hx₂ : (𝓝[<] x.2).NeBot
⊢ 𝓝[<] x.1 ×ˢ 𝓝[<] x.2 ≤ 𝓝[<] x

Tactic:
← nhdsWithin_prod_eq

Goal state after:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : TopologicalSpace Z
inst✝⁴ : TopologicalSpace W
inst✝³ : TopologicalSpace ε
inst✝² : TopologicalSpace ζ
inst✝¹ : Preorder X
inst✝ : Preorder Y
x : X × Y
hx₁ : (𝓝[<] x.1).NeBot
hx₂ : (𝓝[<] x.2).NeBot
⊢ 𝓝[Iio x.1 ×ˢ Iio x.2] (x.1, x.2) ≤ 𝓝[<] x
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : TopologicalSpace Z
inst✝⁴ : TopologicalSpace W
inst✝³ : TopologicalSpace ε
inst✝² : TopologicalSpace ζ
inst✝¹ : Preorder X
inst✝ : Preorder Y
x : X × Y
hx₁ : (𝓝[>] x.1).NeBot
hx₂ : (𝓝[>] x.2).NeBot
⊢ 𝓝[>] x.1 ×ˢ 𝓝[>] x.2 ≤ 𝓝[>] x

Tactic:
← nhdsWithin_prod_eq

Goal state after:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : TopologicalSpace Z
inst✝⁴ : TopologicalSpace W
inst✝³ : TopologicalSpace ε
inst✝² : TopologicalSpace ζ
inst✝¹ : Preorder X
inst✝ : Preorder Y
x : X × Y
hx₁ : (𝓝[>] x.1).NeBot
hx₂ : (𝓝[>] x.2).NeBot
⊢ 𝓝[Ioi x.1 ×ˢ Ioi x.2] (x.1, x.2) ≤ 𝓝[>] x
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s : Set α
p : α → Prop
h : ∀ᶠ (y : α) in 𝓝[s] a, ∀ᶠ (x : α) in 𝓝[s] y, p x
⊢ ∀ᶠ (x : α) in 𝓝[s] a, p x

Tactic:
simp only [eventually_nhdsWithin_iff] at h ⊢

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s : Set α
p : α → Prop
h : ∀ᶠ (x : α) in 𝓝 a, x ∈ s → ∀ᶠ (x : α) in 𝓝 x, x ∈ s → p x
⊢ ∀ᶠ (x : α) in 𝓝 a, x ∈ s → p 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
t : Set Y
x : X
y : Y
⊢ s ×ˢ t ∈ 𝓝 x ×ˢ 𝓝 y ↔ s ∈ 𝓝 x ∧ t ∈ 𝓝 y

Tactic:
prod_mem_prod_iff

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
x : X
y : Y
⊢ s ∈ 𝓝 x ∧ t ∈ 𝓝 y ↔ s ∈ 𝓝 x ∧ t ∈ 𝓝 y
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
X : α → β
s : Set β
t : Set α
a : α
h : a ∈ t
hs : s ∈ 𝓝 (X a)
⊢ X ⁻¹' s ∈ 𝓝[t] a

Tactic:
lift a to t using h

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
X : α → β
s : Set β
t : Set α
a : { x // x ∈ t }
hs : s ∈ 𝓝 (X ↑a)
⊢ X ⁻¹' s ∈ 𝓝[t] ↑a
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: case empty
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_5
I : Set ι
s : ι → Set α
a : α
⊢ 𝓝[⋃ i ∈ ∅, s i] a = ⨆ i ∈ ∅, 𝓝[s i] a

Tactic:
| empty =>

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:
rw [compl_inter]

Goal state after:
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
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst✝¹] s
h : ∀ (t : Set β), IsOpen[inst✝] t → IsOpen[inst✝¹] (s ∩ f ⁻¹' t)
t : Set β
ht : IsOpen[inst✝] t
⊢ f ⁻¹' t ∩ s = s ∩ f ⁻¹' t ∩ s

Tactic:
rw [@inter_comm _ s (f ⁻¹' t), inter_assoc, inter_self]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
u : Set Y
hu : IsClosed[inst✝] u
⊢ IsClosed[instTopologicalSpaceSum] (inr '' u)

Tactic:
simpa [isClosed_sum_iff, preimage_image_eq u Sum.inr_injective]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
t : Set ↑s
⊢ Dense t ↔ s ⊆ closure[inst✝] ↑t

Tactic:
by
  rw [IsInducing.subtypeVal.dense_iff, SetCoe.forall]
  rfl

Goal state after:
Module: Mathlib.Topology.Bases

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

Tactic:
simpa [and_assoc] using h_nhds a

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t✝ : TopologicalSpace α
B : Set (Set α)
s✝ : Set α
inst✝² : TopologicalSpace β
inst✝¹ : SeparableSpace α
inst✝ : SeparableSpace β
s : Set α
hsc : s.Countable
hsd : Dense s
t : Set β
htc : t.Countable
htd : Dense t
⊢ Dense (Sum.inl '' s ∪ Sum.inr '' t)

Tactic:
simp_rw [dense_iff_closure_eq, closure_union, IsClosedEmbedding.inl.closure_image_eq,
    hsd.closure_eq, IsClosedEmbedding.inr.closure_image_eq, htd.closure_eq, image_univ,
    range_inl_union_range_inr]

Goal state after:
Module: Mathlib.Order.Filter.Ultrafilter.Basic

Goal state before:
pp: case empty
α : Type u
f : Ultrafilter α
s : Set (Set α)
⊢ ⋃₀ ∅ ∈ f ↔ ∃ t ∈ ∅, t ∈ f

Tactic:
| empty =>

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case mpr
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
S : Set β
U : ι → Set β
F : Finset ι
hUT : ∀ i ∈ F, U i ∈ preimage (f i) '' T i
hSU : S = ⋂ i ∈ F, U i
⊢ ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i

Tactic:
choose! U' hU' hUU' using hUT
    exact ⟨U', F, hU', hSU ▸ (.symm <| iInter₂_congr hUU')⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_1
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
b : Set (Set α)
hb₁ : b.Countable
hb₂ : t = generateFrom b
⊢ ((fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ b} \ {∅}).Countable

pp: case refine_2
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
b : Set (Set α)
hb₁ : b.Countable
hb₂ : t = generateFrom b
⊢ ∅ ∈ {∅}

Tactic:
exacts [((countable_ofPred_finite_subset hb₁).image _).mono sdiff_subset, rfl]

Goal state after: