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

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✝⁹ : HasZeroMorphisms C
inst✝⁸ : HasZeroMorphisms D
S : ShortComplex C
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
F : C ⥤ D
inst✝⁷ : F.PreservesZeroMorphisms
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hl₁ : S₁.LeftHomologyData
hr₁ : S₁.RightHomologyData
hl₂ : S₂.LeftHomologyData
hr₂ : S₂.RightHomologyData
ψl : LeftHomologyMapData φ hl₁ hl₂
ψr : RightHomologyMapData φ hr₁ hr₂
inst✝⁶ : S₁.HasHomology
inst✝⁵ : S₂.HasHomology
inst✝⁴ : (F.mapShortComplex.obj S₁).HasHomology
inst✝³ : (F.mapShortComplex.obj S₂).HasHomology
inst✝² : F.PreservesLeftHomologyOf S₁
inst✝¹ : F.PreservesLeftHomologyOf S₂
inst✝ : QuasiIso φ
⊢ QuasiIso (F.mapShortComplex.map φ)

Tactic:
have γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData := default
  have : IsIso γ.φH := by
    rw [← γ.quasiIso_iff]
    infer_instance
  rw [(γ.map F).quasiIso_iff, LeftHomologyMapData.map_φH]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u_1
inst✝³ : Category.{v_1, u_1} D
F : C ⥤ D
inst✝² : F.Full
inst✝¹ : F.Faithful
inst✝ : F.PreservesMonomorphisms
I : C
hI : Injective (F.obj I)
X✝ Y✝ : C
g : X✝ ⟶ I
f : X✝ ⟶ Y✝
x✝ : Mono f
⊢ ∃ h, f ≫ h = g

Tactic:
obtain ⟨h, fac⟩ := hI.factors (F.map g) (F.map f)

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u_1
inst✝³ : Category.{v_1, u_1} D
F : C ⥤ D
inst✝² : F.Full
inst✝¹ : F.Faithful
inst✝ : F.PreservesMonomorphisms
I : C
hI : Injective (F.obj I)
X✝ Y✝ : C
g : X✝ ⟶ I
f : X✝ ⟶ Y✝
x✝ : Mono f
h : F.obj Y✝ ⟶ F.obj I
fac : F.map f ≫ h = F.map g
⊢ ∃ h, f ≫ h = g
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S₁ S₂ S₃ S : ShortComplex C
inst✝ : S.HasLeftHomology
A : C
k k' : A ⟶ S.X₂
hk : k ≫ S.g = 0
hk' : k' ≫ S.g = 0
⊢ k ≫ S.g + k' ≫ S.g = 0

Tactic:
hk,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S₁ S₂ S₃ S : ShortComplex C
inst✝ : S.HasLeftHomology
A : C
k k' : A ⟶ S.X₂
hk : k ≫ S.g = 0
hk' : k' ≫ S.g = 0
⊢ 0 + k' ≫ S.g = 0
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S₁ S₂ S₃ S : ShortComplex C
inst✝ : S.HasLeftHomology
A : C
k k' : A ⟶ S.X₂
hk : k ≫ S.g = 0
hk' : k' ≫ S.g = 0
⊢ k ≫ S.g - k' ≫ S.g = 0

Tactic:
hk,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S₁ S₂ S₃ S : ShortComplex C
inst✝ : S.HasLeftHomology
A : C
k k' : A ⟶ S.X₂
hk : k ≫ S.g = 0
hk' : k' ≫ S.g = 0
⊢ 0 - k' ≫ S.g = 0
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
this : S.HasHomology
⊢ IsZero h.left.H → h.left.π ≫ h.iso.hom ≫ h.right.ι = 0

pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
this : S.HasHomology
⊢ h.left.π ≫ h.iso.hom ≫ h.right.ι = 0 → IsZero h.left.H

Tactic:
· intro z
    rw [IsZero.eq_of_src z h.iso.hom 0, zero_comp, comp_zero]

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
this : S.HasHomology
⊢ h.left.π ≫ h.iso.hom ≫ h.right.ι = 0 → IsZero h.left.H
Module: Mathlib.Algebra.Homology.ShortComplex.Ab

Goal state before:
pp: S : ShortComplex Ab
hS : S.Exact
inst✝¹ : Finite ↑S.X₁
inst✝ : Finite ↑S.X₃
this : Finite ↥(AddCommGrpCat.Hom.hom S.f).range
⊢ Finite (↑S.X₂ ⧸ (AddCommGrpCat.Hom.hom S.f).range)

Tactic:
rw [hS.ab_range_eq_ker]

Goal state after:
S : ShortComplex Ab
hS : S.Exact
inst✝¹ : Finite ↑S.X₁
inst✝ : Finite ↑S.X₃
this : Finite ↥(AddCommGrpCat.Hom.hom S.f).range
⊢ Finite (↑S.X₂ ⧸ (AddCommGrpCat.Hom.hom S.g).ker)
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : HasZeroMorphisms C
X' : C
f : X' ⟶ X
inst✝¹ : IsIso f
g : X ⟶ Y
inst✝ : HasKernel g
⊢ (kernelSubobjectIsoComp f g).hom ≫ (kernelSubobject g).arrow = (kernelSubobject (f ≫ g)).arrow ≫ f

Tactic:
by
  simp [kernelSubobjectIsoComp]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : HasZeroMorphisms C
X' : C
f : X' ⟶ X
inst✝¹ : IsIso f
g : X ⟶ Y
inst✝ : HasKernel g
⊢ (kernelSubobjectIsoComp f g).inv ≫ (kernelSubobject (f ≫ g)).arrow = (kernelSubobject g).arrow ≫ inv f

Tactic:
by
  simp [kernelSubobjectIsoComp]

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

Goal state before:
pp: case f
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
⊢ underlying.obj (sSup s) ⟶ underlying.obj f

Tactic:
refine (underlyingIso _).hom ≫ image.lift ⟨_, f.arrow, ?_, ?_⟩

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
⊢ (∐ fun j ↦ underlying.obj ((equivShrink (Subobject A)).symm ↑j)) ⟶ underlying.obj f

case f.refine_2
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
⊢ ?f.refine_1 ≫ f.arrow = smallCoproductDesc s
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst✝ : HasCoproduct Z
X : C
π : (a : α) → Z a ⟶ X
⊢ (Sigma.desc π).op ≫ (opCoproductIsoProduct Z).hom = Pi.lift fun a ↦ (π a).op

Tactic:
by
  convert!
    desc_op_comp_opCoproductIsoProduct'_hom (coproductIsCoproduct Z) (productIsProduct (op <| Z ·))
      (Cofan.mk _ π)
  · simp [Sigma.desc, coproductIsCoproduct]
  · simp [productIsProduct]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : C ⥤ D
d : Dᵒᵖ
⊢ (map (𝟙 d).unop).toCatHom.toFunctor = (𝟙 (Cat.of (StructuredArrow (Opposite.unop d) T))).toFunctor

Tactic:
exact Functor.ext (fun ⟨_, _, _⟩ => by simp)

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E : L.LeftExtension F
E' : ?m.13
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
Y₁ Y₂ : D
φ : Y₁ ⟶ Y₂
X : CostructuredArrow L Y₁
⊢ (E.coconeAt Y₁).ι.app X ≫ (StructuredArrow.right E).map φ ≫ (h Y₂).desc (G.coconeAt Y₂) =
    (G.coconeAt Y₁).ι.app X ≫ (StructuredArrow.right G).map φ

Tactic:
simpa using (h Y₂).fac (coconeAt G Y₂) ((CostructuredArrow.map φ).obj X)

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
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ ((cokernelOrderHom X).comp (kernelOrderHom X)) (Subobject.mk f) = OrderHom.id (Subobject.mk f)

Tactic:
dsimp only [OrderHom.comp_coe, Function.comp_apply, kernelOrderHom_coe, Subobject.lift_mk,
      cokernelOrderHom_coe, OrderHom.id_coe, id]

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
hf : Mono f
⊢ Subobject.mk (cokernel.π (kernel.ι f.unop)).op = Subobject.mk f
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₁)
s : Cocone (functorToRepresentables P)
m : (coconeOfRepresentable P).pt ⟶ s.pt
hm : ∀ (j : P.Elementsᵒᵖ), (coconeOfRepresentable P).ι.app j ≫ m = s.ι.app j
⊢ m = { app := fun X ↦ ↾fun x ↦ uliftYonedaEquiv (s.ι.app (op (P.elementsMk X x))), naturality := ⋯ }

Tactic:
by
    ext X x
    simp only [functorToRepresentables_obj, coconeOfRepresentable_pt, Functor.const_obj_obj,
      coconeOfRepresentable_ι_app, Functor.leftOp_obj, CategoryOfElements.π_obj, op_unop,
      TypeCat.Fun.toFun_apply, hom_ofHom, TypeCat.Fun.coe_mk] at hm ⊢
    rw [← hm, uliftYonedaEquiv_comp, 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)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j ↦ F.map (line j)
j j' : WalkingParallelFamily J
g : j ⟶ j'
⊢ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map g ≫ t.π.app j' ≫ eqToHom ⋯ =
    (t.π.app j ≫ eqToHom ⋯) ≫ F.map g

Tactic:
cases g <;> cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
hf : (ObjectProperty.ofObj f).IsCoseparating
c : Fan f
hc : IsLimit c
x✝³ x✝² : C
x✝¹ x✝ : x✝³ ⟶ x✝²
huv : ∀ (h : x✝² ⟶ c.pt), x✝¹ ≫ h = x✝ ≫ h
b : β
g : x✝² ⟶ f b
⊢ x✝¹ ≫ g = x✝ ≫ g

Tactic:
simpa using huv (hc.lift (Fan.mk _ (Pi.single b g))) =≫ c.proj b

Goal state after:
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: A : Type u_1
inst✝ : AddCommGroup A
H : ∀ {n : ℤ}, n ≠ 0 → n • ⊤ = ⊤
a : A
n : ℤ
hn : ¬n = 0
⊢ a ∈ n • ⊤

Tactic:
rw [H hn]

Goal state after:
A : Type u_1
inst✝ : AddCommGroup A
H : ∀ {n : ℤ}, n ≠ 0 → n • ⊤ = ⊤
a : A
n : ℤ
hn : ¬n = 0
⊢ a ∈ ⊤
Module: Mathlib.Algebra.Ring.Periodic

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

Tactic:
by
  simpa only [sub_eq_add_neg] using h.neg_nsmul n x

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
⊢ m = n

Tactic:
by_contra h : m ≠ n
  wlog hmn : m < n
  · exact this hn hm heq.symm h.symm (by grind)
  · simpa [heq] using count_strict_mono hm hmn

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
m : M
⊢ f m =
    ↑{ domain := supExtensionOfMaxSingleton i f y,
          toFun := { toFun := ExtensionOfMaxAdjoin.extensionToFun i f h, map_add' := ⋯, map_smul' := ⋯ } }
      ⟨i m, ⋯⟩

Tactic:
by
    dsimp
    rw [(extensionOfMax i f).is_extension,
      ExtensionOfMaxAdjoin.extensionToFun_wd i f h _ ⟨i m, _⟩ 0 _, map_zero, add_zero]
    simp

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

Goal state before:
pp: m n : ℕ
h : m.Coprime n
hmn0 : m * n = 0
⊢ φ (m * n) = φ m * φ n

Tactic:
by
    rcases Nat.mul_eq_zero.1 hmn0 with h | h <;>
      simp only [totient_zero, mul_zero, zero_mul, h]

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

Goal state before:
pp: α : Type u_3
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsCodirectedOrder α
p : α × α → Prop
⊢ (∀ᶠ (x : α × α) in atBot, p x) ↔ ∃ a, ∀ (k l : α), k ≤ a → l ≤ a → p (k, l)

Tactic:
simp [← prod_atBot_atBot_eq, (@atBot_basis α _ _).prod_self.eventually_iff]

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

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
⊢ φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)

Tactic:
totient_eq_prod_factorization hn

Goal state after:
case neg
n : ℕ
hn : ¬n = 0
⊢ (n.factorization.prod fun p k ↦ p ^ (k - 1) * (p - 1)) * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)
Module: Mathlib.Data.Nat.Totient

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

Tactic:
d.totient_le

Goal state after:
a b : ℕ
d : ℕ := a.gcd b
ha0 : a > 0
hd0 : 0 < d
⊢ φ (a * b) * d ≤ φ (a * b) * d
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✝] (⋃ b, bif b then s₁ else s₂)

Tactic:
exact isOpen_iUnion (Bool.forall_bool.2 ⟨h₂, h₁⟩)

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 (closure s)

Tactic:
exact isClosed_closure

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ ⋂₀ {t | IsClosed t ∧ s ⊆ t} = ⋂₀ (compl '' {t | IsOpen t ∧ t ⊆ sᶜ})

Tactic:
compl_image_ofPred

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ ⋂₀ {t | IsClosed t ∧ s ⊆ t} = ⋂₀ {s_1 | IsOpen s_1ᶜ ∧ s_1ᶜ ⊆ 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

Tactic:
rw [toIcoMod, toIocMod, sub_le_sub_iff_left]
  exact zsmul_left_mono hp.le (toIocDiv_wcovBy_toIcoDiv _ _ _).le

Goal state after:
Module: Mathlib.Topology.NhdsSet

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

Tactic:
← range_comp

Goal state after:
X : Type u_4
inst✝ : TopologicalSpace (X × X)
⊢ sSup (range (𝓝 ∘ Function.diag)) = ⨆ x, 𝓝 (x, x)
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ a < b - ↑(-⌊(a + p - b) / p⌋) * p ∧ b - ↑(-⌊(a + p - b) / p⌋) * p ≤ a + p

Tactic:
Int.cast_neg,

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ a < b - -↑⌊(a + p - b) / p⌋ * p ∧ b - -↑⌊(a + p - b) / p⌋ * p ≤ a + p
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ 𝓝ˢ (insert x s) = 𝓝 x ⊔ 𝓝ˢ s

Tactic:
rw [insert_eq, nhdsSet_union, nhdsSet_singleton]

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
⊢ ⋃ n, Icc (↑n) (↑n + 1) = univ

Tactic:
simpa only [zero_add] using iUnion_Icc_add_intCast (0 : α)

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst✝] (s ∪ t)
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
⊢ IsOpen[inst✝] s

Tactic:
suffices s = (s ∪ t) ∩ u from this ▸ hst'.inter hu

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst✝] (s ∪ t)
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
⊢ s = (s ∪ t) ∩ u
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
hf : IsOpenMap f
hf' : Continuous[inst✝¹, inst✝] f
s : Set X
⊢ ⨆ i ∈ s, map f (𝓝 i) = ⨆ i ∈ s, 𝓝 (f i)

Tactic:
hf.map_nhds_eq hf'.continuousAt

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
⊢ 𝓝 (x, y) = comap Prod.fst (𝓝 x) ⊓ comap Prod.snd (𝓝 y)

Tactic:
instTopologicalSpaceProd,

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
⊢ 𝓝 (x, y) = comap Prod.fst (𝓝 x) ⊓ comap Prod.snd (𝓝 y)
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
x : X
y : Y
hs : s ∈ map Prod.fst (𝓝[Prod.snd ⁻¹' {(x, y).2}] (x, y))
⊢ s ∈ 𝓝 (x, y).1

Tactic:
rw [mem_map, nhdsWithin, mem_inf_principal, mem_nhds_prod_iff] at hs

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
x : X
y : Y
hs : ∃ u ∈ 𝓝 x, ∃ v ∈ 𝓝 y, u ×ˢ v ⊆ {x_1 | x_1 ∈ Prod.snd ⁻¹' {(x, y).2} → x_1 ∈ Prod.fst ⁻¹' s}
⊢ s ∈ 𝓝 (x, y).1
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
x : X
y : Y
hs : s ∈ map Prod.snd (𝓝[Prod.fst ⁻¹' {(x, y).1}] (x, y))
⊢ s ∈ 𝓝 (x, y).2

Tactic:
rw [mem_map, nhdsWithin, mem_inf_principal, mem_nhds_prod_iff] at hs

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
x : X
y : Y
hs : ∃ u ∈ 𝓝 x, ∃ v ∈ 𝓝 y, u ×ˢ v ⊆ {x_1 | x_1 ∈ Prod.fst ⁻¹' {(x, y).1} → x_1 ∈ Prod.snd ⁻¹' s}
⊢ s ∈ 𝓝 (x, y).2
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
x : X
f : Y → Z
⊢ inst✝¹ = induced (fun x' ↦ (x, f x')) instTopologicalSpaceProd ↔ inst✝¹ = induced f inst✝

Tactic:
instTopologicalSpaceProd,

Goal state after:
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
x : X
f : Y → Z
⊢ inst✝¹ = induced (fun x' ↦ (x, f x')) (induced Prod.fst inst✝² ⊓ induced Prod.snd inst✝) ↔ inst✝¹ = induced f inst✝
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
y : Y
f : X → Z
⊢ inst✝² = induced (fun x ↦ (f x, y)) instTopologicalSpaceProd ↔ inst✝² = induced f inst✝

Tactic:
instTopologicalSpaceProd,

Goal state after:
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
y : Y
f : X → Z
⊢ inst✝² = induced (fun x ↦ (f x, y)) (induced Prod.fst inst✝ ⊓ induced Prod.snd inst✝¹) ↔ inst✝² = induced f inst✝
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
f : X → Bool
b : Bool
⊢ IsOpen[inst✝] (f ⁻¹' {b}) ∧ IsOpen[inst✝] (f ⁻¹' {!b}) ↔ IsClopen (f ⁻¹' {b})

Tactic:
IsClopen,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
f : X → Bool
b : Bool
⊢ IsOpen[inst✝] (f ⁻¹' {b}) ∧ IsOpen[inst✝] (f ⁻¹' {!b}) ↔ IsClosed[inst✝] (f ⁻¹' {b}) ∧ IsOpen[inst✝] (f ⁻¹' {b})
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hs : ∀ (a : X), f a ∈ s
hf : ∀ (s_1 : Set ↑s), IsOpen[instTopologicalSpaceSubtype] s_1 → IsOpen[inst✝¹] (codRestrict f s hs ⁻¹' s_1)
t : Set Y
ht : IsOpen[inst✝] t
⊢ IsOpen[inst✝¹] (f ⁻¹' t)

Tactic:
exact hf (Subtype.val ⁻¹' t) (isOpen_induced ht)

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hs : ∀ (a : X), f a ∈ s
⊢ Continuous[inst✝¹, instTopologicalSpaceSubtype] (codRestrict f s hs) ↔ Continuous[inst✝¹, inst✝] f

Tactic:
refine ⟨?_, fun hf ↦ hf.codRestrict hs⟩
  simp_rw [continuous_def]
  intro hf t ht
  exact hf (Subtype.val ⁻¹' t) (isOpen_induced ht)

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

Goal state before:
pp: case e'_3
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
hf : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
x : X
⊢ (range g)ᶜ ∈ 𝓝 (f x)

Tactic:
rw [← disjoint_principal_right]
    exact hfG.mono_left (nhds_le_nhdsSet (mem_range_self x))

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_1
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : ⋃ i, U i = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
i : ι
s : Set { x // x ∈ U i }
sb : s ∈ b i
⊢ IsOpen[t] (Subtype.val '' s)

Tactic:
exact (Uo i).isOpenMap_subtype_val _ ((hb i).isOpen sb)

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

Goal state before:
pp: case mk
α : Type u_2
t' : Bornology α
cobounded✝ : Filter α
le_cofinite✝ : cobounded✝ ≤ cofinite
h_cobounded : cobounded α = cobounded α
⊢ { cobounded := cobounded✝, le_cofinite := le_cofinite✝ } = t'

Tactic:
cases t'

Goal state after:
case mk.mk
α : Type u_2
cobounded✝¹ : Filter α
le_cofinite✝¹ : cobounded✝¹ ≤ cofinite
cobounded✝ : Filter α
le_cofinite✝ : cobounded✝ ≤ cofinite
h_cobounded : cobounded α = cobounded α
⊢ { cobounded := cobounded✝¹, le_cofinite := le_cofinite✝¹ } = { cobounded := cobounded✝, le_cofinite := le_cofinite✝ }
Module: Mathlib.Topology.Bornology.Basic

Goal state before:
pp: α : Type u_2
s : Set α
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B
union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B
sUnion_univ : ∀ (x : α), {x} ∈ B
⊢ sᶜ ∈ comk (fun x ↦ x ∈ B) empty_mem subset_mem union_mem ↔ s ∈ B

Tactic:
compl_mem_comk

Goal state after:
α : Type u_2
s : Set α
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B
union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B
sUnion_univ : ∀ (x : α), {x} ∈ B
⊢ s ∈ B ↔ s ∈ B
Module: Mathlib.Topology.Bases

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

Tactic:
rsuffices ⟨f, hf⟩ : ∃ f : (i : I) → c i, g ⟨I, f⟩ ∈ Set.pi I u

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

ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst✝ i] (c i)
this : ∀ (i : ι), Countable ↑(c i)
g : (I : Finset ι) × ((i : ↥I) → ↑(c ↑i)) → (i : ι) → X i := ⋯
f : (i : ι) → X i
hf : f ∈ univ.pi s
o : Set ((i : ι) → X i)
ho : IsOpen[Pi.topologicalSpace] o
hfo : f ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst✝ a] (u a) ∧ f a ∈ u a
hI : (↑I).pi u ⊆ o
⊢ ∃ f, g ⟨I, f⟩ ∈ (↑I).pi u