mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: X'✝ X✝ : Type u
Y✝ : AddCommGrpCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget AddCommGrpCat).obj Y✝
x✝ : ↑(free.obj X'✝)
⊢ (FreeAbelianGroup.lift ⇑(ConcreteCategory.hom (f✝ ≫ g✝))) x✝ =
    (FreeAbelianGroup.lift (⇑(ConcreteCategory.hom g✝) ∘ ⇑(ConcreteCategory.hom f✝))) x✝

Tactic:
rfl

Goal state after:
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 : (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

Tactic:
rfl

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

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
i₁ : C
y₂ : F i₁
x✝ : ∃ (h : i₁ = i₁), y₂ = cast ⋯ y₂
⊢ c.inj i₁ y₂ = c.inj i₁ y₂

Tactic:
rfl

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

Goal state before:
pp: C✝ : Type u
F✝ : C✝ → Type v
C : Type u
F : C → Type v
c : Cofan F
i : C
f : { as := i } ⟶ { as := i }
⊢ (match (motive := (x : Discrete C) → (Discrete.functor F).obj x → c.pt) { as := i } with
      | { as := j } => ⇑(ConcreteCategory.hom (c.inj j))) ∘
      ⇑(ConcreteCategory.hom ((Discrete.functor F).map f)) =
    match (motive := (x : Discrete C) → (Discrete.functor F).obj x → c.pt) { as := i } with
    | { as := j } => ⇑(ConcreteCategory.hom (c.inj j))

Tactic:
rfl

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

Goal state before:
pp: X'✝ X✝ : Type u
Y✝ : GrpCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget GrpCat).obj Y✝
a✝ : X'✝
⊢ (Hom.hom ((ConcreteCategory.homEquiv.trans (FreeGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm (f✝ ≫ g✝)))
      (FreeGroup.of a✝) =
    (Hom.hom
        (free.map f✝ ≫ (ConcreteCategory.homEquiv.trans (FreeGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm g✝))
      (FreeGroup.of a✝)

Tactic:
rfl

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

Goal state before:
pp: X✝ : GrpCat
⊢ Abelianization.of.comp (Hom.hom (𝟙 X✝)) =
    Abelianization.lift.symm (CommGrpCat.Hom.hom (𝟙 (CommGrpCat.of (Abelianization ↑X✝))))

Tactic:
rfl

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

Goal state before:
pp: X✝ Y✝ Z✝ : GrpCat
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ Abelianization.of.comp (Hom.hom (f✝ ≫ g✝)) =
    Abelianization.lift.symm
      (CommGrpCat.Hom.hom
        (CommGrpCat.ofHom (Abelianization.lift (Abelianization.of.comp (Hom.hom f✝))) ≫
          CommGrpCat.ofHom (Abelianization.lift (Abelianization.of.comp (Hom.hom g✝)))))

Tactic:
rfl

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

Goal state before:
pp: X✝ : CommGrpCat
Y✝ : CommMonCat
f✝ : (forget₂ CommGrpCat CommMonCat).obj X✝ ⟶ Y✝
⊢ { toFun := fun f ↦ ofHom (CommMonCat.Hom.hom f).toHomUnits,
        invFun := fun f ↦ CommMonCat.ofHom ((Units.coeHom ↑Y✝).comp (Hom.hom f)), left_inv := ⋯, right_inv := ⋯ }
      f✝ =
    { app := fun X ↦ ofHom toUnits.toMonoidHom, naturality := ⋯ }.app X✝ ≫ CommMonCat.units.map f✝

Tactic:
rfl

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

Goal state before:
pp: X✝ : CommGrpCat
Y✝ : CommMonCat
g✝ : X✝ ⟶ CommMonCat.units.obj Y✝
⊢ { toFun := fun f ↦ ofHom (CommMonCat.Hom.hom f).toHomUnits,
          invFun := fun f ↦ CommMonCat.ofHom ((Units.coeHom ↑Y✝).comp (Hom.hom f)), left_inv := ⋯, right_inv := ⋯ }.symm
      g✝ =
    (forget₂ CommGrpCat CommMonCat).map g✝ ≫
      { app := fun X ↦ CommMonCat.ofHom (Units.coeHom ↑X), naturality := ⋯ }.app Y✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.ZMod.IntUnitsPower

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R (Additive ℤˣ)
⊢ Int.instUnitsPow = NPow.toPow

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.ZMod.IntUnitsPower

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R (Additive ℤˣ)
⊢ Int.instUnitsPow = ZPow.toPow

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b c : α
⊢ (a ≤ b ∧ ¬b ≤ a) ∧ b ≤ c ∧ ¬c ≤ b ∨ (b ≤ c ∧ ¬c ≤ b) ∧ c ≤ a ∧ ¬a ≤ c ∨ (c ≤ a ∧ ¬a ≤ c) ∧ a ≤ b ∧ ¬b ≤ a ↔
    (a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b) ∧ ¬(c ≤ b ∧ b ≤ a ∨ b ≤ a ∧ a ≤ c ∨ a ≤ c ∧ c ≤ b)

Tactic:
grind

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)
x y : ↥i.range
⊢ f (Exists.choose ⋯) = f (Exists.choose ⋯) + f (Exists.choose ⋯)

Tactic:
have eq1 : _ + _ = (x + y).1 := congr_arg₂ (· + ·) x.2.choose_spec y.2.choose_spec

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)
x y : ↥i.range
eq1 : i (Exists.choose ⋯) + i (Exists.choose ⋯) = ↑(x + y)
⊢ f (Exists.choose ⋯) = f (Exists.choose ⋯) + f (Exists.choose ⋯)
Module: Mathlib.Data.Nat.Factorization.Induction

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

Tactic:
convert! prime_pow_mul ((k + 2) / p ^ t) p t hp _ htp (hk _ (Nat.div_lt_of_lt_mul _)) using 1

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

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

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ (List.filter (fun b ↦ decide (p b)) (List.range n)).length = #({x ∈ range n | p x})

Tactic:
rfl

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n ≤ n

Tactic:
by
  rw [count_eq_card_filter_range]
  exact (card_filter_le _ _).trans_eq (card_range _)

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
⊢ ∀ (n : ℕ), count p n ≤ count p (n + 1)

Tactic:
grind

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n < count p (n + 1) ↔ p n

Tactic:
grind

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p (n + 1) = count p n + 1 ↔ p n

Tactic:
grind

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p (n + 1) = count p n ↔ ¬p n

Tactic:
grind

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
h : m ≠ n
this : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {m n : ℕ}, p m → p n → count p m = count p n → m ≠ n → m < n → False
hmn : ¬m < n
⊢ n < m

Tactic:
grind

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
r : R
a : ↥(supExtensionOfMaxSingleton i f y)
⊢ r • ↑(ExtensionOfMaxAdjoin.fst i a) + r • ExtensionOfMaxAdjoin.snd i a • y =
    ↑(r • ExtensionOfMaxAdjoin.fst i a) + r • ExtensionOfMaxAdjoin.snd i a • y

Tactic:
rfl

Goal state after:
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)
⊢ (a ≤ a + t ∧ a + t < a + k + 1) ∧ p (a + t)

Tactic:
grind

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

Goal state before:
pp: m : ℕ
inst✝¹ : NeZero (m + 1)
inst✝ : Fintype (ZMod (m + 1))ˣ
⊢ (∑ a, if a.val.Coprime (m + 1) then 1 else 0) = ∑ i, if (↑i).Coprime (m + 1) then 1 else 0

Tactic:
rfl

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

Goal state before:
pp: case h
ι : Type u_1
ι' : Type u_2
⊢ ∀ (b : Finset (ι × ι')), ∃ a, b ⊆ a.1 ×ˢ a.2

Tactic:
· intro b
    use (Finset.image Prod.fst b, Finset.image Prod.snd b)
    exact Finset.subset_product

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

Goal state before:
pp: α : Type u_3
inst✝ : Preorder α
⊢ Tendsto (fun a ↦ (a, a)) atBot (atBot ×ˢ atBot)

Tactic:
exact tendsto_id.prodMk tendsto_id

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

Goal state before:
pp: case right
β : Type u_4
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ l ≤ N, u l ≤ u k
ex : ∃ n ≥ N, u k < u n
n : ℕ
hnN : n ≥ N
hnk : u k < u n
hn_min : ∀ m < n, N ≤ m → u m ≤ u k
⊢ ∀ k < n, u k < u n

Tactic:
grind

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

Goal state before:
pp: α : Type u_3
inst✝ : Preorder α
⊢ Tendsto (fun a ↦ (a, a)) atTop (atTop ×ˢ atTop)

Tactic:
exact tendsto_id.prodMk tendsto_id

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

Goal state before:
pp: n : ℕ
⊢ φ (n + 3) = 1 ↔ n + 3 = 1 ∨ n + 3 = 2

Tactic:
have : 3 ≤ n + 3 := le_add_self

Goal state after:
n : ℕ
this : 3 ≤ n + 3
⊢ φ (n + 3) = 1 ↔ n + 3 = 1 ∨ n + 3 = 2
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
⊢ (∃ x, Tendsto x atTop l ∧ ∃ᶠ (x_1 : ℕ) in atTop, p (x x_1)) ↔
    ∃ x, Tendsto x atTop l ∧ ∃ᶠ (x_1 : ℕ) in atTop, p (x x_1)

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Basic

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

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Set α → Filter β
m : γ → β
⊢ ⨅ i ∈ f, comap m (g i) = ⨅ s ∈ f, (comap m ∘ g) s

Tactic:
rfl

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

Goal state before:
pp: case false
α : Type u_1
β : Type u_2
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ (bif false then f else g).lift' s = bif false then f.lift' s else g.lift' s

Tactic:
rfl

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

Goal state before:
pp: case true
α : Type u_1
β : Type u_2
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ (bif true then f else g).lift' s = bif true then f.lift' s else g.lift' s

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ interior s = ∅ ↔ Dense sᶜ

Tactic:
dense_iff_closure_eq,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ interior s = ∅ ↔ closure sᶜ = univ
Module: Mathlib.Topology.Closure

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

Tactic:
sdiff_sdiff_right_self,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ closure s ∩ interior s = interior s
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_4
inst✝ : TopologicalSpace (X × X)
⊢ sSup (range (𝓝 ∘ Function.diag)) = ⨆ x, 𝓝 (x, x)

Tactic:
rfl

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 ?_
  rcases sub_toIocDiv_zsmul_mem_Ioc hp a b with ⟨hl, hr⟩
  refine ⟨toIocDiv hp a b, ⟨lt_sub_iff_add_lt.mp hl, ?_⟩⟩
  rw [add_smul, one_smul, ← add_assoc]
  convert! sub_le_iff_le_add.mp hr using 1; abel

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type u_1
m : α → β
f : Filter α
g : Set (Set β)
b : β
⊢ (∀ i ∈ g, b ∈ i → ∀ᶠ (a : α) in f, m a ∈ i) ↔ ∀ s ∈ g, b ∈ s → m ⁻¹' s ∈ f

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: case a
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := ⋯
⊢ n a ≤ 𝓝 a

Tactic:
exact (nhds_basis_opens a).ge_iff.2 fun U ⟨haU, hUo⟩ ↦ hUo a haU

Goal state after:
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)
⊢ ∀ ⦃a : X⦄,
    a ∈ ⋃ n, u n \ closure[inst✝] (⋃ m, ⋃ (_ : m ≤ n), v m) → a ∉ ⋃ n, v n \ closure[inst✝] (⋃ m, ⋃ (_ : m ≤ n), u m)

Tactic:
rintro x ⟨un, ⟨n, rfl⟩, xinun⟩

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
⊢ x ∉ ⋃ n, v n \ closure[inst✝] (⋃ m, ⋃ (_ : m ≤ n), u m)
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
⊢ IsOpen[induced f inst✝¹] s ↔ ∃ t, IsOpen[inst✝¹] t ∧ f ⁻¹' t = s

Tactic:
isOpen_induced_iff

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
⊢ (∃ t, IsOpen[inst✝¹] t ∧ f ⁻¹' t = s) ↔ ∃ t, IsOpen[inst✝¹] t ∧ f ⁻¹' t = s
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
⊢ (∃ t ⊆ s, IsOpen[induced f T] t ∧ a ∈ t) ↔ ∃ u, (∃ t ⊆ u, IsOpen[T] t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s

Tactic:
isOpen_induced_iff

Goal state after:
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
⊢ (∃ t ⊆ s, (∃ t_1, IsOpen[T] t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t) ↔ ∃ u, (∃ t ⊆ u, IsOpen[T] t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
x : X
⊢ 𝓝 (h.symm (h x)) = 𝓝 x

Tactic:
h.symm_apply_apply

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
x : X
⊢ 𝓝 x = 𝓝 x
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
a : α
s : Set α
⊢ a ∈ closure[induced f t] s ↔ f a ∈ closure[t] (f '' s)

Tactic:
by
  simp only [mem_closure_iff_frequently, nhds_induced, frequently_comap, mem_image, and_comm]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
p : α → Prop
⊢ (∀ (x : α), p x → ∀ᶠ (x : α) in 𝓝 x, p x) ↔ ∀ x ∈ {x | p x}, {x | p x} ∈ 𝓝 x

Tactic:
rfl

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 : ∀ (x : X), ∃ g, ContinuousAt g (f x) ∧ g (f x) = x ∧ RightInverse g f
x : X
g : Y → X
hgc : ContinuousAt g (f x)
hgx : g (f x) = x
hgf : RightInverse g f
⊢ map f (𝓝 (g (f x))) = map f (𝓝 x)

Tactic:
rw [hgx]

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
hf : IsOpenEmbedding f
l : Filter Z
x : X
⊢ map g (𝓝 (f x)) ≤ l ↔ Tendsto g (𝓝 (f x)) l

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
⊢ IsOpen[instTopologicalSpaceSubtype] (s.domRestrict f ⁻¹' t) ↔ ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
rw [isOpen_induced_iff, Set.domRestrict_eq, Set.preimage_comp]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
⊢ (∃ t_1, IsOpen[inst✝¹] t_1 ∧ Subtype.val ⁻¹' t_1 = Subtype.val ⁻¹' f ⁻¹' t) ↔
    ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: Y : Type v
W : Type u_1
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace W
X : Type u_5
Z : Type u_6
f : X → Y
g : Z → W
⊢ induced (f ∘ Prod.fst) inst✝¹ ⊓ induced (g ∘ Prod.snd) inst✝ =
    induced (Prod.fst ∘ fun p ↦ (f p.1, g p.2)) inst✝¹ ⊓ induced (Prod.snd ∘ fun p ↦ (f p.1, g p.2)) inst✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (α i)
I : Set ι
s : (i : ι) → Set (α i)
x : (i : ι) → α i
⊢ x ∈ closure[Pi.topologicalSpace] (I.pi s) ↔ ∀ i ∈ I, x i ∈ closure[inst✝ i] (s i)

Tactic:
simp only [mem_closure_iff_nhdsWithin_neBot, nhdsWithin_pi_neBot]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
f g : α → β
a : α
h₁ : f =ᶠ[𝓝[≠] a] g
h₂ : f a = g a
⊢ ∀ (a_1 : α), (a_1 ∈ {a}ᶜ → f a_1 = g a_1) → f a_1 = g a_1

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
s : Set α
a : α
h : a ∈ s
f : α → β
l : Filter β
⊢ Tendsto (f ∘ Subtype.val) (𝓝 ⟨a, h⟩) l ↔ Tendsto (s.domRestrict f) (𝓝 ⟨a, h⟩) l

Tactic:
rfl

Goal state after:
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
⊢ (∀ (t : Set β), IsOpen[inst✝] t → IsOpen[inst✝¹] (s ∩ f ⁻¹' t)) →
    ∀ (t : Set β), IsOpen[inst✝] t → ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
· intro h t ht
    refine ⟨s ∩ f ⁻¹' t, h t ht, ?_⟩
    rw [@inter_comm _ s (f ⁻¹' t), inter_assoc, inter_self]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s u : Set α
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ (∃ U, IsOpen[TopologicalSpace.induced f t] U ∧ s ⊆ U ∧ U ⊆ u) ↔
    ∃ v, (∃ U, IsOpen[t] U ∧ f '' s ⊆ U ∧ U ⊆ v) ∧ f ⁻¹' v ⊆ u

Tactic:
isOpen_induced_iff

Goal state after:
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s u : Set α
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ (∃ U, (∃ t_1, IsOpen[t] t_1 ∧ f ⁻¹' t_1 = U) ∧ s ⊆ U ∧ U ⊆ u) ↔
    ∃ v, (∃ U, IsOpen[t] U ∧ f '' s ⊆ U ∧ U ⊆ v) ∧ f ⁻¹' v ⊆ u
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
t : Set ↑s
⊢ (∀ (x : X) (h : x ∈ s), ↑⟨x, h⟩ ∈ closure[inst✝] (val '' t)) ↔ s ⊆ closure[inst✝] ↑t

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
Y : Type u_5
p : X → Prop
l : Filter Y
f : Y → Subtype p
a : X
ha : p a
⊢ Tendsto (Subtype.val ∘ f) l (𝓝 a) ↔ Tendsto (fun x ↦ ↑(f x)) l (𝓝 ↑⟨a, ha⟩)

Tactic:
rfl

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

Goal state before:
pp: case inl
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
val✝ : X
⊢ ((Homeomorph.refl X).sumCongr (Homeomorph.refl Y)) (inl val✝) = (Homeomorph.refl (X ⊕ Y)) (inl val✝)

Tactic:
rfl

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

Goal state before:
pp: case inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
val✝ : Y
⊢ ((Homeomorph.refl X).sumCongr (Homeomorph.refl Y)) (inr val✝) = (Homeomorph.refl (X ⊕ Y)) (inr val✝)

Tactic:
rfl

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

Goal state before:
pp: case inl
X : Type u
Y : Type v
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
X' : Type u_5
Y' : Type u_6
inst✝³ : TopologicalSpace X'
inst✝² : TopologicalSpace Y'
X'' : Type u_7
Y'' : Type u_8
inst✝¹ : TopologicalSpace X''
inst✝ : TopologicalSpace Y''
h₁ : X ≃ₜ X'
h₂ : Y ≃ₜ Y'
h₃ : X' ≃ₜ X''
h₄ : Y' ≃ₜ Y''
val✝ : X
⊢ ((h₁.sumCongr h₂).trans (h₃.sumCongr h₄)) (inl val✝) = ((h₁.trans h₃).sumCongr (h₂.trans h₄)) (inl val✝)

Tactic:
rfl

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

Goal state before:
pp: case inr
X : Type u
Y : Type v
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
X' : Type u_5
Y' : Type u_6
inst✝³ : TopologicalSpace X'
inst✝² : TopologicalSpace Y'
X'' : Type u_7
Y'' : Type u_8
inst✝¹ : TopologicalSpace X''
inst✝ : TopologicalSpace Y''
h₁ : X ≃ₜ X'
h₂ : Y ≃ₜ Y'
h₃ : X' ≃ₜ X''
h₄ : Y' ≃ₜ Y''
val✝ : Y
⊢ ((h₁.sumCongr h₂).trans (h₃.sumCongr h₄)) (inr val✝) = ((h₁.trans h₃).sumCongr (h₂.trans h₄)) (inr val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ Tendsto f (map (Prod.mk x.1) (𝓝 x.2 ⊓ 𝓟 (Prod.mk x.1 ⁻¹' s))) (𝓝 (f (x.1, x.2))) ↔
    Tendsto (fun x_1 ↦ f (x.1, x_1)) (𝓝 x.2 ⊓ 𝓟 {b | (x.1, b) ∈ s}) (𝓝 (f (x.1, x.2)))

Tactic:
rfl

Goal state after: