mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g h : MonoOver A
k₁ : f ⟶ h
k₂ : g ⟶ h
⊢ coprod.inl ≫ coprod.desc (Over.Hom.left k₁.hom) (Over.Hom.left k₂.hom) ≫ h.arrow =
    coprod.inl ≫ ((Functor.uncurry.obj Over.coprod).obj (((forget A).prod (forget A)).obj (f, g))).hom

pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g h : MonoOver A
k₁ : f ⟶ h
k₂ : g ⟶ h
⊢ coprod.inr ≫ coprod.desc (Over.Hom.left k₁.hom) (Over.Hom.left k₂.hom) ≫ h.arrow =
    coprod.inr ≫ ((Functor.uncurry.obj Over.coprod).obj (((forget A).prod (forget A)).obj (f, g))).hom

Tactic:
· simp [w k₁]

Goal state after:
case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g h : MonoOver A
k₁ : f ⟶ h
k₂ : g ⟶ h
⊢ coprod.inr ≫ coprod.desc (Over.Hom.left k₁.hom) (Over.Hom.left k₂.hom) ≫ h.arrow =
    coprod.inr ≫ ((Functor.uncurry.obj Over.coprod).obj (((forget A).prod (forget A)).obj (f, g))).hom
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.Faithful
S : ShortComplex C
hS : kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f) = 0
⊢ F.map (kernel.ι S.g) ≫ F.map S.g = 0

Tactic:
simp only [← F.map_comp, kernel.condition, CategoryTheory.Functor.map_zero]

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

Goal state before:
pp: A : Type u₁
B : Type u₂
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Abelian A
inst✝¹ : Abelian B
L : A ⥤ B
inst✝ : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact
X Y : A
f : X ⟶ Y
this : L.PreservesMonomorphisms
⊢ PreservesLimit (parallelPair f 0) L

Tactic:
apply preservesLimit_of_preserves_limit_cone (kernelIsKernel f)

Goal state after:
A : Type u₁
B : Type u₂
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Abelian A
inst✝¹ : Abelian B
L : A ⥤ B
inst✝ : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact
X Y : A
f : X ⟶ Y
this : L.PreservesMonomorphisms
⊢ IsLimit (L.mapCone (Fork.ofι (kernel.ι f) ⋯))
Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor

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✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_3 : (∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact) → F.PreservesHomology
hF : ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact
S : ShortComplex C
hS : S.ShortExact
⊢ (S.map F).ShortExact

Tactic:
have : Mono (S.map F).f := exact_iff_mono _ (by simp) |>.1 <|
      hF (.mk (0 : 0 ⟶ S.X₁) S.f <| by simp) (exact_iff_mono _ (by simp) |>.2 hS.mono_f)
    have : Epi (S.map F).g := exact_iff_epi _ (by simp) |>.1 <|
      hF (.mk S.g (0 : S.X₃ ⟶ 0) <| by simp) (exact_iff_epi _ (by simp) |>.2 hS.epi_g)
    exact ⟨hF S hS.exact⟩

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
p : A.obj (op X)
p' q' : F.obj (op (CostructuredArrow.mk (yonedaEquiv.symm p)))
h : fst ⟨p, p'⟩ = fst ⟨p, q'⟩
h' : (ConcreteCategory.hom (F.map (eqToHom ⋯))) (snd ⟨p, q'⟩) = snd ⟨p, p'⟩
⊢ ⟨p, p'⟩.snd ≍ ⟨p, q'⟩.snd

Tactic:
simpa [snd] using! h'.symm

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: C : Type u
inst✝¹¹ : Category.{v, u} C
D : Type u_1
J : Type u_2
inst✝¹⁰ : Category.{v_1, u_1} D
inst✝⁹ : Category.{v_2, u_2} J
inst✝⁸ : HasLimitsOfShape J C
inst✝⁷ : HasLimitsOfShape J D
inst✝⁶ : HasExactLimitsOfShape J D
F : C ⥤ D
inst✝⁵ : PreservesFiniteColimits F
inst✝⁴ : ReflectsFiniteColimits F
inst✝³ : HasFiniteColimits C
inst✝² : PreservesLimitsOfShape J F
I : Type
inst✝¹ : SmallCategory I
inst✝ : FinCategory I
G : I ⥤ J ⥤ C
c : Cocone G
hc : IsColimit c
i : I
⊢ (preservesLimitIso F (G.obj i)).hom ≫ limMap (whiskerRight (c.ι.app i) F) ≫ (preservesLimitIso F c.pt).inv =
    F.map (limMap (c.ι.app i))

Tactic:
rw [← Iso.eq_inv_comp]

Goal state after:
C : Type u
inst✝¹¹ : Category.{v, u} C
D : Type u_1
J : Type u_2
inst✝¹⁰ : Category.{v_1, u_1} D
inst✝⁹ : Category.{v_2, u_2} J
inst✝⁸ : HasLimitsOfShape J C
inst✝⁷ : HasLimitsOfShape J D
inst✝⁶ : HasExactLimitsOfShape J D
F : C ⥤ D
inst✝⁵ : PreservesFiniteColimits F
inst✝⁴ : ReflectsFiniteColimits F
inst✝³ : HasFiniteColimits C
inst✝² : PreservesLimitsOfShape J F
I : Type
inst✝¹ : SmallCategory I
inst✝ : FinCategory I
G : I ⥤ J ⥤ C
c : Cocone G
hc : IsColimit c
i : I
⊢ limMap (whiskerRight (c.ι.app i) F) ≫ (preservesLimitIso F c.pt).inv =
    (preservesLimitIso F (G.obj i)).inv ≫ F.map (limMap (c.ι.app i))
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian C
inst✝¹ : Abelian D
inst✝ : IsGrothendieckAbelian.{w, v, u} C
α : C ≌ D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
⊢ AB5OfSize.{w, w, v₂, u₂} D

pp: case refine_3
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian C
inst✝¹ : Abelian D
inst✝ : IsGrothendieckAbelian.{w, v, u} C
α : C ≌ D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
⊢ HasSeparator D

Tactic:
· refine ⟨fun _ _ _ => ?_⟩
    exact HasExactColimitsOfShape.of_codomain_equivalence _ α

Goal state after:
case refine_3
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian C
inst✝¹ : Abelian D
inst✝ : IsGrothendieckAbelian.{w, v, u} C
α : C ≌ D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
⊢ HasSeparator D
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
P : ObjectProperty C
hP : P.IsCoseparating
X Y : StructuredArrow S T
f g : X ⟶ Y
hfg : ∀ (G : StructuredArrow S T), P.inverseImage (proj S T) G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
G : C
hG : P G
h : Y.right ⟶ G
⊢ Hom.right f ≫ h = Hom.right g ≫ h

Tactic:
exact congr_arg CommaMorphism.right (hfg (mk (Y.hom ≫ T.map h)) hG (homMk h 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
hc : IsColimit c
i j : C
x : F i
y : F j
hij : i = j
⊢ F i = F j

Tactic:
rw [hij]

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

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

Tactic:
obtain rfl | hn := eq_or_ne n 0 <;> simp [*]

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Range

Goal state before:
pp: a : ℕ
s : Finset ℕ
⊢ ∀ ⦃a_1 : ℕ⦄, a_1 < a → ¬∃ a_3 ∈ s, (addLeftEmbedding a) a_3 = a_1

Tactic:
addLeftEmbedding_apply

Goal state after:
a : ℕ
s : Finset ℕ
⊢ ∀ ⦃a_1 : ℕ⦄, a_1 < a → ¬∃ a_3 ∈ s, a + a_3 = a_1
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
h✝ : Baer R Q
X Y : Type v
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
i : X →ₗ[R] Y
hi : Function.Injective ⇑i
f : X →ₗ[R] Q
h : Y →ₗ[R] Q
H : h ∘ₗ i = f
⊢ ∃ h, ∀ (x : X), h (i x) = f x

Tactic:
exact ⟨h, DFunLike.congr_fun H⟩

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

Goal state before:
pp: a k n : ℕ
a_ne_zero : a ≠ 0
⊢ #({x ∈ Ico k (k + n) | a.Coprime x}) ≤ φ a * (n / a + 1)

Tactic:
by
  conv_lhs => rw [← Nat.mod_add_div n a]
  induction n / a with
  | zero =>
    rw [← filter_coprime_Ico_eq_totient a k]
    simp only [add_zero, mul_one, mul_zero, zero_add]
    gcongr
    exact le_of_lt (mod_lt n (pos_iff_ne_zero.mpr a_ne_zero))
  | succ i ih => ?_
  simp only [mul_succ]
  simp_rw [← add_assoc] at ih ⊢
  calc
    #{x ∈ Ico k (k + n % a + a * i + a) | a.Coprime x}
      ≤ #{x ∈ Ico k (k + n % a + a * i) ∪
        Ico (k + n % a + a * i) (k + n % a + a * i + a) | a.Coprime x} := by
      gcongr
      apply Ico_subset_Ico_union_Ico
    _ ≤ #{x ∈ Ico k (k + n % a + a * i) | a.Coprime x} + a.totient := by
      rw [filter_union, ← filter_coprime_Ico_eq_totient a (k + n % a + a * i)]
      apply card_union_le
    _ ≤ a.totient * i + a.totient + a.totient := by grw [← mul_add_one, ih]

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

Goal state before:
pp: n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
⊢ ↑(∏ i ∈ n.primeFactors, i) ≠ 0

Tactic:
cast_ne_zero,

Goal state after:
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
⊢ ∏ i ∈ n.primeFactors, i ≠ 0
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a b : ℕ
⊢ φ a * φ b ≤ φ (a * b)

Tactic:
let d := a.gcd b

Goal state after:
a b : ℕ
d : ℕ := a.gcd b
⊢ φ a * φ b ≤ φ (a * b)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a : ℕ
ha : ¬a = 0
c : ℕ
h' : φ c = 1
hb : ¬a * c = 0
this : a.Coprime c
⊢ a = a * c ∨ 2 * a = a * c

Tactic:
totient_eq_one_iff

Goal state after:
a : ℕ
ha : ¬a = 0
c : ℕ
h' : c = 1 ∨ c = 2
hb : ¬a * c = 0
this : a.Coprime c
⊢ a = a * c ∨ 2 * a = a * c
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
⊢ IsOpen[inst✝] ∅

Tactic:
by
  rw [← sUnion_empty]; exact isOpen_sUnion fun a => False.elim

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

Goal state before:
pp: α : Type u_1
β : Type u_2
g : Set α → Filter β
⊢ ⊤.lift g = g univ

Tactic:
simp [Filter.lift]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g h : Set α → Filter β
⊢ (f.lift fun x ↦ g x ⊓ h x) = f.lift g ⊓ f.lift h

Tactic:
simp only [Filter.lift, iInf_inf_eq]

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
x₁ x₂ x₃ : α
h : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
⊢ toIcoMod hp x₂ x₃ ≤ toIocMod hp x₂ x₁

Tactic:
by
  let x₂' := toIcoMod hp x₁ x₂
  let x₃' := toIcoMod hp x₂' x₃
  have h : x₂' ≤ toIocMod hp x₁ x₃' := by simpa [x₃']
  have h₂₁ : x₂' < x₁ + p := toIcoMod_lt_right _ _ _
  have h₃₂ : x₃' - p < x₂' := sub_lt_iff_lt_add.2 (toIcoMod_lt_right _ _ _)
  suffices hequiv : x₃' ≤ toIocMod hp x₂' x₁ by
    obtain ⟨z, hd⟩ : ∃ z : ℤ, x₂ = x₂' + z • p := ((toIcoMod_eq_iff hp).1 rfl).2
    simpa [hd, toIocMod_add_zsmul', toIcoMod_add_zsmul', add_le_add_iff_right]
  rcases le_or_gt x₃' (x₁ + p) with h₃₁ | h₁₃
  · suffices hIoc₂₁ : toIocMod hp x₂' x₁ = x₁ + p from hIoc₂₁.trans_ge h₃₁
    apply (toIocMod_eq_iff hp).2
    exact ⟨⟨h₂₁, by simp [x₂', left_le_toIcoMod]⟩, -1, by simp⟩
  have hIoc₁₃ : toIocMod hp x₁ x₃' = x₃' - p := by
    apply (toIocMod_eq_iff hp).2
    exact ⟨⟨lt_sub_iff_add_lt.2 h₁₃, le_of_lt (h₃₂.trans h₂₁)⟩, 1, by simp⟩
  have not_h₃₂ := (h.trans hIoc₁₃.le).not_gt
  contradiction

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

Tactic:
simpa using toIcoDiv_add_zsmul' 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 : ℤ
⊢ toIocMod hp a (↑m * p + b) = toIocMod hp a b

Tactic:
by
  rw [add_comm, toIocMod_add_intCast_mul]

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
⊢ ⋃ n, Icc (n • p) ((n + 1) • p) = univ

Tactic:
simpa only [zero_add] using iUnion_Icc_add_zsmul hp 0

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

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

Tactic:
by
  simp only [ContinuousAt, ← h.map_nhds_eq, tendsto_map'_iff, comp_def]

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
p : X → Prop
⊢ (∀ᶠ (x : X) in 𝓝ˢ (s ∪ t), p x) ↔ (∀ᶠ (x : X) in 𝓝ˢ s, p x) ∧ ∀ᶠ (x : X) in 𝓝ˢ t, p x

Tactic:
rw [nhdsSet_union, eventually_sup]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
f : α → β
g : β → γ
t₁ : TopologicalSpace α
t₂ : TopologicalSpace γ
⊢ Continuous[coinduced f t₁, t₂] g ↔ Continuous[t₁, t₂] (g ∘ f)

Tactic:
simp only [continuous_iff_coinduced_le, coinduced_compose]

Goal state after:
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
p : X → Prop
q : Y → Prop
f : X ≃ₜ Y
hs : IsClopen {x | p x}
ht : IsClopen {y | q y}
⊢ IsClosed[inst✝¹] {x | p x ↔ q (f x)}

Tactic:
simpa [iff_def] using! (isClosed_imp hs.2 (f.isClosed_preimage.2 ht.1)).inter
    (isClosed_imp (f.isOpen_preimage.2 ht.2) hs.1)

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
h : s ∈ 𝓝[t] a
⊢ 𝓝[s] a ⊓ 𝓝[t] a = 𝓝[t] a

Tactic:
inf_eq_right

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
h : s ∈ 𝓝[t] a
⊢ 𝓝[t] a ≤ 𝓝[s] a
Module: Mathlib.Topology.ContinuousOn

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

Tactic:
rintro ⟨u, ou, useq⟩
        exact ⟨u, ou, by simpa only [Set.inter_comm, eq_comm] using useq⟩

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

Tactic:
rintro ⟨u, ou, useq⟩
        exact ⟨u, ou, by simpa only [Set.inter_comm, eq_comm] using useq⟩

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

Goal state before:
pp: case inr.mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : IsOpen[inst✝¹] s ∧ IsOpen[inst✝] t
⊢ IsOpen[instTopologicalSpaceProd] (s ×ˢ t)

Tactic:
exact H.1.prod H.2

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
hf : IsInducing f
hg : IsInducing g
hFg : Disjoint (closure[inst✝] (range f)) (range g)
hfG : Disjoint (range f) (closure[inst✝] (range g))
⊢ IsInducing (Sum.elim f g)

Tactic:
rw [← disjoint_principal_nhdsSet] at hFg
  rw [← disjoint_nhdsSet_principal] at hfG
  rw [isInducing_iff_nhds]
  intro x
  apply le_antisymm ((hf.continuous.sumElim hg.continuous).tendsto x).le_comap
  obtain x | x := x <;>
  simp only [comap_sumElim_eq, nhds_inl, nhds_inr, elim_inl, elim_inr, ← hf.nhds_eq_comap,
    ← hg.nhds_eq_comap, sup_le_iff, le_rfl, true_and, and_true] <;>
  convert! bot_le (α := Filter (X ⊕ Y)) <;>
  rw [map_eq_bot_iff, comap_eq_bot_iff_compl_range]
  · rw [← disjoint_principal_right]
    exact hfG.mono_left (nhds_le_nhdsSet (mem_range_self x))
  · rw [← disjoint_principal_left]
    exact hFg.mono_right (nhds_le_nhdsSet (mem_range_self x))

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 : α × β → γ
⊢ IsOpenMap f ↔ ∀ (a : α), IsOpenMap fun x ↦ f (a, x)

Tactic:
simp_rw [isOpenMap_iff_nhds_le, Prod.forall, nhds_prod_eq, nhds_discrete, pure_prod, map_map]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
⊢ (∀ (a : α) (b : β), 𝓝 (f (a, b)) ≤ map (f ∘ Prod.mk a) (𝓝 b)) ↔
    ∀ (a : α) (x : β), 𝓝 (f (a, x)) ≤ map (fun x ↦ f (a, x)) (𝓝 x)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: Y : Type v
n : ℕ
A : Fin (n + 1) → Type u_9
inst✝ : (i : Fin (n + 1)) → TopologicalSpace (A i)
f : Y → A 0
g : Y → (j : Fin n) → A j.succ
l : Filter Y
x : A 0
y : (j : Fin n) → A j.succ
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ ∀ (i : Fin n), Tendsto (fun i_1 ↦ Fin.cons (f i_1) (g i_1) i.succ) l (𝓝 (Fin.cons x y i.succ))

Tactic:
simpa using tendsto_pi_nhds.1 hg

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
g : β → α
x : β
h : LeftInverse f g
hf : ContinuousWithinAt f (range g) (g x)
hg : ContinuousAt g x
⊢ ContinuousWithinAt f (g '' univ) (g x)

Tactic:
rwa [image_univ]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: Y : Type v
n : ℕ
A : Fin (n + 1) → Type u_9
inst✝ : (i : Fin (n + 1)) → TopologicalSpace (A i)
i : Fin (n + 1)
f : Y → A i
g : Y → (j : Fin n) → A (i.succAbove j)
l : Filter Y
x : A i
y : (j : Fin n) → A (i.succAbove j)
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ ∀ (j : Fin n), Tendsto (fun i_1 ↦ i.insertNth (f i_1) (g i_1) (i.succAbove j)) l (𝓝 (i.insertNth x y (i.succAbove j)))

Tactic:
simpa using tendsto_pi_nhds.1 hg

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝¹ : SeparableSpace α
inst✝ : Nonempty α
⊢ ∃ u, DenseRange u

Tactic:
obtain ⟨s : Set α, hs, s_dense⟩ := exists_countable_dense α

Goal state after:
α : Type u
t : TopologicalSpace α
inst✝¹ : SeparableSpace α
inst✝ : Nonempty α
s : Set α
hs : s.Countable
s_dense : Dense s
⊢ ∃ u, DenseRange u
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s s' : Set α
t : Set β
hf : ContinuousOn f s'
hs' : s' ∈ 𝓝ˢ s
hst : MapsTo f s t
V : Set α
hV : IsOpen[inst✝¹] V
hsV : s ⊆ V
hVs' : V ⊆ s'
⊢ Tendsto f (𝓝ˢ s) (𝓝ˢ t)

Tactic:
refine ((hasBasis_nhdsSet s).tendsto_iff (hasBasis_nhdsSet t)).mpr fun U hU ↦
    ⟨V ∩ f ⁻¹' U, ?_, fun _ ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s s' : Set α
t : Set β
hf : ContinuousOn f s'
hs' : s' ∈ 𝓝ˢ s
hst : MapsTo f s t
V : Set α
hV : IsOpen[inst✝¹] V
hsV : s ⊆ V
hVs' : V ⊆ s'
U : Set β
hU : IsOpen[inst✝] U ∧ t ⊆ U
⊢ IsOpen[inst✝¹] (V ∩ f ⁻¹' U) ∧ s ⊆ V ∩ f ⁻¹' U

case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s s' : Set α
t : Set β
hf : ContinuousOn f s'
hs' : s' ∈ 𝓝ˢ s
hst : MapsTo f s t
V : Set α
hV : IsOpen[inst✝¹] V
hsV : s ⊆ V
hVs' : V ⊆ s'
U : Set β
hU : IsOpen[inst✝] U ∧ t ⊆ U
x✝ : α
⊢ x✝ ∈ V ∩ f ⁻¹' U → f x✝ ∈ U
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t✝] u
a : α → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set ↑u
T_count : T.Countable
hT : ⋃ i ∈ T, a ↑i = ⋃ i, a ↑i
⊢ ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a

Tactic:
refine ⟨(fun (x : u) ↦ a x) '' T, ?_, T_count.image _, ?_⟩

Goal state after:
case refine_1
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t✝] u
a : α → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set ↑u
T_count : T.Countable
hT : ⋃ i ∈ T, a ↑i = ⋃ i, a ↑i
⊢ (fun x ↦ a ↑x) '' T ⊆ t

case refine_2
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t✝] u
a : α → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set ↑u
T_count : T.Countable
hT : ⋃ i ∈ T, a ↑i = ⋃ i, a ↑i
⊢ u = ⋃ a_1 ∈ (fun x ↦ a ↑x) '' T, a_1
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_3
l✝ l' la : Filter α
lb : Filter β
l : Filter α
⊢ l.smallSets.NeBot

Tactic:
by
  refine (lift'_neBot_iff ?_).2 fun _ _ => powerset_nonempty
  exact monotone_powerset

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
n : ℕ
⊢ L n ⊆ f '' s

Tactic:
exact (subset_iUnion _ n).trans hcov.le

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case h_nhds
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen[inst✝] U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
⊢ ∃ v ∈ image π '' V, π x ∈ v ∧ v ⊆ U

Tactic:
have W_open : IsOpen W := U_open.preimage h'.continuous

Goal state after:
case h_nhds
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen[inst✝] U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
W_open : IsOpen[inst✝¹] W
⊢ ∃ v ∈ image π '' V, π x ∈ v ∧ v ⊆ U
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
ι : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
s t : Set X
f : X → Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace Y
⊢ IsCompact univ

Tactic:
rw [← range_inl_union_range_inr]
    exact (isCompact_range continuous_inl).union (isCompact_range continuous_inr)

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s s' t : Set α
inst✝ : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure[inst✝²] t)
h' : ContinuousOn g (s' ∩ closure[inst✝²] tᶜ)
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f g (s ∩ frontier t)
⊢ ContinuousOn f (t.ite s s' ∩ closure[inst✝²] t)

pp: case hg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s s' t : Set α
inst✝ : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure[inst✝²] t)
h' : ContinuousOn g (s' ∩ closure[inst✝²] tᶜ)
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f g (s ∩ frontier t)
⊢ ContinuousOn g (t.ite s s' ∩ closure[inst✝²] tᶜ)

Tactic:
· rwa [ite_inter_closure_eq_of_inter_frontier_eq H]

Goal state after:
case hg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s s' t : Set α
inst✝ : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure[inst✝²] t)
h' : ContinuousOn g (s' ∩ closure[inst✝²] tᶜ)
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f g (s ∩ frontier t)
⊢ ContinuousOn g (t.ite s s' ∩ closure[inst✝²] tᶜ)
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : R0Space X
inst✝ : TopologicalSpace Y
f : Y → X
hf : IsInducing f
a b : Y
⊢ a ⤳ b → b ⤳ a

Tactic:
simpa only [← hf.specializes_iff] using Specializes.symm

Goal state after: