mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝ : F'.IsRightKanExtension α
c : Cone F
hc : IsLimit c
s : Cone F'
m : s.pt ⟶ (F'.coneOfIsRightKanExtension α c).pt
hm : ∀ (j : D), m ≫ (F'.coneOfIsRightKanExtension α c).π.app j = s.π.app j
j : C
this : m ≫ (F'.coneOfIsRightKanExtension α c).π.app (L.obj j) = s.π.app (L.obj j)
⊢ m ≫ c.π.app j = hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ c.π.app j

Tactic:
← F'.liftOfIsRightKanExtension_fac_app α ((const D).obj c.pt)

Goal state after:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝ : F'.IsRightKanExtension α
c : Cone F
hc : IsLimit c
s : Cone F'
m : s.pt ⟶ (F'.coneOfIsRightKanExtension α c).pt
hm : ∀ (j : D), m ≫ (F'.coneOfIsRightKanExtension α c).π.app j = s.π.app j
j : C
this : m ≫ (F'.coneOfIsRightKanExtension α c).π.app (L.obj j) = s.π.app (L.obj j)
⊢ m ≫ (F'.liftOfIsRightKanExtension α ((const D).obj c.pt) c.π).app (L.obj j) ≫ α.app j =
    hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ c.π.app j
Module: Mathlib.Algebra.Category.Grp.AB

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
x : ↑(S.map colim).X₂
hx : (AddCommGrpCat.Hom.hom (colimMap S.g)) x = 0
⊢ x ∈ (AddCommGrpCat.Hom.hom (S.map colim).f).range

Tactic:
rcases Concrete.colimit_exists_rep S.X₂ x with ⟨j, y, rfl⟩

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
j : J
y : ToType (S.X₂.obj j)
hx : (AddCommGrpCat.Hom.hom (colimMap S.g)) ((ConcreteCategory.hom (colimit.ι S.X₂ j)) y) = 0
⊢ (ConcreteCategory.hom (colimit.ι S.X₂ j)) y ∈ (AddCommGrpCat.Hom.hom (S.map colim).f).range
Module: Mathlib.Algebra.Category.Grp.AB

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
j : J
y : ToType (S.X₂.obj j)
hx : (AddCommGrpCat.Hom.hom (colimMap S.g)) ((ConcreteCategory.hom (colimit.ι S.X₂ j)) y) = 0
⊢ (ConcreteCategory.hom (colimit.ι S.X₂ j)) y ∈ (AddCommGrpCat.Hom.hom (S.map colim).f).range

Tactic:
← ConcreteCategory.comp_apply,

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
j : J
y : ToType (S.X₂.obj j)
hx : (ConcreteCategory.hom (colimit.ι S.X₂ j ≫ colimMap S.g)) y = 0
⊢ (ConcreteCategory.hom (colimit.ι S.X₂ j)) y ∈ (AddCommGrpCat.Hom.hom (S.map colim).f).range
Module: Mathlib.Algebra.Category.Grp.AB

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
j : J
y : ToType (S.X₂.obj j)
hx :
  (ConcreteCategory.hom (colimit.ι S.X₃ j)) ((ConcreteCategory.hom (S.g.app j)) y) =
    (AddCommGrpCat.Hom.hom (colimit.ι S.X₃ j)) 0
k : J
e₁ e₂ : j ⟶ k
hk : (ConcreteCategory.hom (S.X₃.map e₁)) ((ConcreteCategory.hom (S.g.app j)) y) = 0
⊢ (ConcreteCategory.hom (colimit.ι S.X₂ j)) y ∈ (AddCommGrpCat.Hom.hom (S.map colim).f).range

Tactic:
← ConcreteCategory.comp_apply,

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
j : J
y : ToType (S.X₂.obj j)
hx :
  (ConcreteCategory.hom (colimit.ι S.X₃ j)) ((ConcreteCategory.hom (S.g.app j)) y) =
    (AddCommGrpCat.Hom.hom (colimit.ι S.X₃ j)) 0
k : J
e₁ e₂ : j ⟶ k
hk : (ConcreteCategory.hom (S.g.app j ≫ S.X₃.map e₁)) y = 0
⊢ (ConcreteCategory.hom (colimit.ι S.X₂ j)) y ∈ (AddCommGrpCat.Hom.hom (S.map colim).f).range
Module: Mathlib.Algebra.Category.Grp.AB

Goal state before:
pp: case h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
j : J
y : ToType (S.X₂.obj j)
hx :
  (ConcreteCategory.hom (colimit.ι S.X₃ j)) ((ConcreteCategory.hom (S.g.app j)) y) =
    (AddCommGrpCat.Hom.hom (colimit.ι S.X₃ j)) 0
k : J
e₁ e₂ : j ⟶ k
hk : (ConcreteCategory.hom (S.g.app k)) ((ConcreteCategory.hom (S.X₂.map e₁)) y) = 0
t : ↑(S.map ((evaluation J AddCommGrpCat).obj k)).X₁
ht : (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj k)).f) t = (ConcreteCategory.hom (S.X₂.map e₁)) y
⊢ (AddCommGrpCat.Hom.hom (S.map colim).f) ((ConcreteCategory.hom (colimit.ι S.X₁ k)) t) =
    (ConcreteCategory.hom (colimit.ι S.X₂ j)) y

Tactic:
← ConcreteCategory.comp_apply,

Goal state after:
case h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
j : J
y : ToType (S.X₂.obj j)
hx :
  (ConcreteCategory.hom (colimit.ι S.X₃ j)) ((ConcreteCategory.hom (S.g.app j)) y) =
    (AddCommGrpCat.Hom.hom (colimit.ι S.X₃ j)) 0
k : J
e₁ e₂ : j ⟶ k
hk : (ConcreteCategory.hom (S.g.app k)) ((ConcreteCategory.hom (S.X₂.map e₁)) y) = 0
t : ↑(S.map ((evaluation J AddCommGrpCat).obj k)).X₁
ht : (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj k)).f) t = (ConcreteCategory.hom (S.X₂.map e₁)) y
⊢ (ConcreteCategory.hom (colimit.ι S.X₁ k ≫ (S.map colim).f)) t = (ConcreteCategory.hom (colimit.ι S.X₂ j)) y
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case mp
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ IsCompl
    (⇑(ConcreteCategory.hom (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) ''
      Set.range ⇑(ConcreteCategory.hom (↾Sum.inl)))
    (Set.range ⇑(ConcreteCategory.hom (↾Sum.inr ≫ (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)))

Tactic:
← eq_compl_iff_isCompl,

Goal state after:
case mp
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ ⇑(ConcreteCategory.hom (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) ''
      Set.range ⇑(ConcreteCategory.hom (↾Sum.inl)) =
    (Set.range ⇑(ConcreteCategory.hom (↾Sum.inr ≫ (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)))ᶜ
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
⊢ 1 < b

Tactic:
have : a * b ^ m < a * b ^ (m + 1) := hx.1.1.trans_le hx.1.2

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
this : a * b ^ m < a * b ^ (m + 1)
⊢ 1 < b
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case inr.i_surj
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ b < d * x, (d * x).gcd b = d → ∃ a, (a < x ∧ x.Coprime a) ∧ d * a = b

Tactic:
intro b hb1 hb2

Goal state after:
case inr.i_surj
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : (d * x).gcd b = d
⊢ ∃ a, (a < x ∧ x.Coprime a) ∧ d * a = b
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
⊢ {a ∈ range (p ^ (n + 1)) | (p ^ (n + 1)).Coprime a} = range (p ^ (n + 1)) \ image (fun x ↦ x * p) (range (p ^ n))

Tactic:
rw [sdiff_eq_filter]
          apply filter_congr
          simp only [mem_range, coprime_pow_left_iff n.succ_pos, mem_image, not_exists,
            hp.coprime_iff_not_dvd]
          intro a ha
          constructor
          · intro hap b h; rcases h with ⟨_, rfl⟩
            exact hap (dvd_mul_left _ _)
          · rintro h ⟨b, rfl⟩
            rw [pow_succ'] at ha
            exact h b ⟨lt_of_mul_lt_mul_left ha (zero_le _), mul_comm _ _⟩

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

Goal state before:
pp: α : Type u_3
inst✝ : Preorder α
p : α → Prop
⊢ (∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y) ↔ ∀ᶠ (x : α) in atTop, p x

Tactic:
by
  refine ⟨fun h ↦ h.mono fun x hx ↦ hx x le_rfl, fun h ↦ ?_⟩
  rcases (hasBasis_iInf_principal_finite _).eventually_iff.1 h with ⟨S, hSf, hS⟩
  refine mem_iInf_of_iInter hSf (V := fun x ↦ Ici x.1) (fun _ ↦ Subset.rfl) fun x hx y hy ↦ ?_
  simp only [mem_iInter] at hS hx
  exact hS fun z hz ↦ le_trans (hx ⟨z, hz⟩) hy

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 c : α
h : toIocMod hp a b = toIocMod hp a c
| c - (toIocMod hp a b + toIocDiv hp a b • p)

Tactic:
← toIocMod_add_toIocDiv_zsmul hp a c

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : toIocMod hp a b = toIocMod hp a c
| toIocMod hp a c + toIocDiv hp a c • p - (toIocMod hp a b + toIocDiv hp a b • p)
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
tfae_3_to_2 : toIcoMod hp a b ≠ toIocMod hp a b → ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
x✝ : toIcoMod hp a b + p = toIocMod hp a b
h : toIcoMod hp a b + p = toIocMod hp a b := x✝
⊢ toIcoMod hp a b ≠ toIocMod hp a b

Tactic:
by
    rw [← h, Ne, eq_comm, add_eq_left]
    exact hp.ne'

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ closure[inst✝] s \ closure[inst✝] t = (closure[inst✝] t)ᶜ ∩ closure[inst✝] s

Tactic:
by simp only [sdiff_eq, inter_comm]

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ closure[inst✝] ((closure[inst✝] t)ᶜ ∩ s) = closure[inst✝] (s \ closure[inst✝] t)

Tactic:
by simp only [sdiff_eq, inter_comm]

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 c : α
⊢ (∃ n, b - a = n • p) ↔ a ≡ b [PMOD p]

Tactic:
AddCommGroup.modEq_iff_zsmul'

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ (∃ n, b - a = n • p) ↔ ∃ m, b - a = m • p
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
F : Filter X
hx : F.HasBasis p s
⊢ (∀ ⦃i : Set X⦄, i ∈ 𝓝 x → ∀ ⦃j : ι⦄, p j → (id i ∩ s j).Nonempty) ↔
    ∀ (i : ι), p i → ∀ {U : Set X}, U ∈ 𝓝 x → ∃ x ∈ U, x ∈ s i

Tactic:
exact ⟨fun h a b c d ↦ h d b, fun h a b c d ↦ h c d b⟩

Goal state after:
Module: Mathlib.Topology.ClusterPt

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

Tactic:
mem_inf_iff

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 : ℤ
⊢ toIocDiv hp a (↑m * p + b) = m + toIocDiv hp a b

Tactic:
by
  simpa using toIocDiv_zsmul_add hp a b m

Goal state after:
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 : ℤ
⊢ toIcoMod hp (a + ↑m * p) b = ↑m * p + toIcoMod hp a b

Tactic:
toIcoMod_add_intCast_mul',

Goal state after:
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 : ℤ
⊢ toIcoMod hp a b + ↑m * p = ↑m * p + toIcoMod hp a b
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 b : α
⊢ ∃ i, b ∈ Ioc (a + i • p) (a + (i + 1) • p)

Tactic:
rcases sub_toIocDiv_zsmul_mem_Ioc hp a b with ⟨hl, hr⟩

Goal state after:
α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
hr : b - toIocDiv hp a b • p ≤ a + p
⊢ ∃ i, b ∈ Ioc (a + i • p) (a + (i + 1) • p)
Module: Mathlib.Topology.Order

Goal state before:
pp: case refl.refine_1
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
h : IsOpen[⊤] U
⊢ U = ∅ ∨ U = univ

Tactic:
induction h with
    | basic _ h => exact False.elim h
    | univ => exact .inr rfl
    | inter _ _ _ _ h₁ h₂ =>
      rcases h₁ with (rfl | rfl) <;> rcases h₂ with (rfl | rfl) <;> simp
    | sUnion _ _ ih => exact sUnion_mem_empty_univ ih

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 Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hg : IsInducing g
⊢ Continuous[inst✝¹, inst✝²] f ↔ Continuous[inst✝¹, inst✝] (g ∘ f)

Tactic:
simp_rw [continuous_iff_continuousAt, hg.continuousAt_iff]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: case mp
α : Type u
t : TopologicalSpace α
⊢ induced ofTopology t = ⊤ → t = ⊤

pp: case mpr
α : Type u
t : TopologicalSpace α
⊢ t = ⊤ → induced ofTopology t = ⊤

Tactic:
· intro h
    simpa [induced_compose, comp_def, induced_fun_id] using congr(induced (toTopology t) $h)

Goal state after:
case mpr
α : Type u
t : TopologicalSpace α
⊢ t = ⊤ → induced ofTopology t = ⊤
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
f : α → β
t₁ t₂ : TopologicalSpace α
t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₁
h₂ : Continuous[t₁, t₃] f
⊢ Continuous[t₂, t₃] f

Tactic:
rw [continuous_iff_le_induced] at h₂ ⊢
  exact le_trans h₁ h₂

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 : IsClosedMap g
hf : IsClosedMap f
⊢ IsClosedMap (g ∘ f)

Tactic:
by
  intro s hs
  rw [image_comp]
  exact hg _ (hf _ hs)

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 ζ
X : Type ?u.28
Y : Type ?u.32
Z : Type ?u.36
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
h : Continuous[instTopologicalSpaceProd, tc1] fun p ↦ f p.1 p.2
this : TopologicalSpace X
⊢ Sort ?u.38

Tactic:
haveI := tb1 ⊓ tb2

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 ζ
X : Type ?u.28
Y : Type ?u.32
Z : Type ?u.36
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
h : Continuous[instTopologicalSpaceProd, tc1] fun p ↦ f p.1 p.2
this✝ : TopologicalSpace X
this : TopologicalSpace Y
⊢ Sort ?u.38
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 (Prod.fst ∘ fun x' ↦ (x, f x')) inst✝² ⊓ induced (Prod.snd ∘ fun x' ↦ (x, f x')) inst✝ ↔
    inst✝¹ = induced f inst✝

Tactic:
Function.comp_def,

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_1 ↦ x) inst✝² ⊓ induced (fun x ↦ f x) 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 (Prod.fst ∘ fun x ↦ (f x, y)) inst✝ ⊓ induced (Prod.snd ∘ fun x ↦ (f x, y)) inst✝¹ ↔
    inst✝² = induced f inst✝

Tactic:
Function.comp_def,

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) inst✝ ⊓ induced (fun x ↦ y) inst✝¹ ↔ inst✝² = induced f inst✝
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
y : β
hg : ContinuousAt g y
hf : ContinuousWithinAt f s x
hy : f x = y
⊢ ContinuousWithinAt (g ∘ f) s x

Tactic:
by
  subst hy; exact hg.comp_continuousWithinAt hf

Goal state after:
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
f : X → Z
g : Y → Z
⊢ IsEmbedding (Sum.elim f g) ↔
    IsEmbedding f ∧
      IsEmbedding g ∧ Disjoint (closure[inst✝] (range f)) (range g) ∧ Disjoint (range f) (closure[inst✝] (range g))

Tactic:
by
  simp_rw [isEmbedding_iff, isInducing_sumElim, Sum.elim_injective]
  constructor
  · intro ⟨⟨hf₁, hg₁, hFg, hfG⟩, ⟨hf₂, hg₂, f_ne_g⟩⟩
    exact ⟨⟨hf₁, hf₂⟩, ⟨hg₁, hg₂⟩, hFg, hfG⟩
  · intro ⟨⟨hf₁, hf₂⟩, ⟨hg₁, hg₂⟩, hFg, hfG⟩
    refine ⟨⟨hf₁, hg₁, hFg, hfG⟩, ⟨hf₂, hg₂, ?_⟩⟩
    exact fun a b ↦ hfG.ne_of_mem (mem_range_self a) (subset_closure (mem_range_self b))

Goal state after:
Module: Mathlib.Topology.Constructions

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

Tactic:
exact fun s ⟨t, ht, Eq⟩ => ⟨t, Finset.univ, by simp [ht, Eq]⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : Set α → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
⊢ IsTopologicalBasis (⋃ u ∈ countableBasis α, s u)

Tactic:
apply isTopologicalBasis_of_isOpen_of_nhds

Goal state after:
case h_open
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : Set α → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
⊢ ∀ u ∈ ⋃ u ∈ countableBasis α, s u, IsOpen[t✝] u

case h_nhds
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : Set α → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen[t✝] u → ∃ v ∈ ⋃ u ∈ countableBasis α, s u, a ∈ v ∧ v ⊆ u
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
f : Filter α
⊢ f.smallSets = generate (powerset '' f.sets)

Tactic:
simp_rw [generate_eq_biInf, smallSets, iInf_image, Filter.lift', Filter.lift, Function.comp_apply,
    Filter.mem_sets]

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

Goal state before:
pp: α : Type u_4
l : Filter α
p : Set α → Prop
hp : ∀ ⦃s t : Set α⦄, s ⊆ t → p s → p t
⊢ (∃ᶠ (s : Set α) in l.smallSets, p s) ↔ ∀ t ∈ l, p t

Tactic:
convert! not_iff_not.mpr <| l.eventually_smallSets' (p := (¬p ·)) (by tauto)
  simp

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst✝¹] U
hZ : IsClosed[inst✝¹] Z
hUZ : range f = U ∩ Z
x : X
H : U ∈ 𝓝 (f x)
⊢ (comap f (𝓝[range f] f x)).HasBasis (fun s ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun s ↦ f ⁻¹' (s ∩ Z)

Tactic:
hUZ,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst✝¹] U
hZ : IsClosed[inst✝¹] Z
hUZ : range f = U ∩ Z
x : X
H : U ∈ 𝓝 (f x)
⊢ (comap f (𝓝[U ∩ Z] f x)).HasBasis (fun s ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun s ↦ f ⁻¹' (s ∩ Z)
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
ι : Type u_1
E : ι → Type u_2
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : Countable ι
inst✝ : ∀ (i : ι), SecondCountableTopology (E i)
b : Set (Set ((i : ι) × E i)) := ⋃ i, (fun u ↦ Sigma.mk i '' u) '' countableBasis (E i)
A : IsTopologicalBasis b
⊢ SecondCountableTopology ((i : ι) × E i)

Tactic:
have B : b.Countable := countable_iUnion fun i => (countable_countableBasis _).image _

Goal state after:
α : Type u
t : TopologicalSpace α
ι : Type u_1
E : ι → Type u_2
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : Countable ι
inst✝ : ∀ (i : ι), SecondCountableTopology (E i)
b : Set (Set ((i : ι) × E i)) := ⋃ i, (fun u ↦ Sigma.mk i '' u) '' countableBasis (E i)
A : IsTopologicalBasis b
B : b.Countable
⊢ SecondCountableTopology ((i : ι) × E i)
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
⊢ IsTopologicalBasis ((fun u ↦ Sum.inl '' u) '' s ∪ (fun u ↦ Sum.inr '' u) '' t)

Tactic:
apply isTopologicalBasis_of_isOpen_of_nhds

Goal state after:
case h_open
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
⊢ ∀ u ∈ (fun u ↦ Sum.inl '' u) '' s ∪ (fun u ↦ Sum.inr '' u) '' t, IsOpen[instTopologicalSpaceSum] u

case h_nhds
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
⊢ ∀ (a : α ⊕ β) (u : Set (α ⊕ β)),
    a ∈ u →
      IsOpen[instTopologicalSpaceSum] u → ∃ v ∈ (fun u ↦ Sum.inl '' u) '' s ∪ (fun u ↦ Sum.inr '' u) '' t, a ∈ v ∧ v ⊆ u