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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
⊢ IsCodetector G ↔ (yoneda.obj G).ReflectsIsomorphisms

Tactic:
refine ⟨fun hG => ⟨fun f hf => ?_⟩, fun h => (isCodetector_def _).2 fun X Y f hf => ?_⟩
  · refine (isIso_unop_iff _).1 (hG.def _ ?_)
    rwa [isIso_iff_bijective, Function.bijective_iff_existsUnique] at hf
  · rw [← isIso_op_iff]
    suffices IsIso ((yoneda.obj G).map f.op) by
      exact @isIso_of_reflects_iso _ _ _ _ _ _ _ (yoneda.obj G) _ h
    rwa [isIso_iff_bijective, Function.bijective_iff_existsUnique]

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

Goal state before:
pp: 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
⊢ Function.Bijective ((Discrete.functor F).descColimitType c)

Tactic:
by
    constructor
    · intro x y h
      obtain ⟨⟨i⟩, x, rfl⟩ := (Discrete.functor F).ιColimitType_jointly_surjective x
      obtain ⟨⟨j⟩, y, rfl⟩ := (Discrete.functor F).ιColimitType_jointly_surjective y
      obtain rfl := h₃ _ _ _ _ h
      obtain rfl := h₂ _ h
      rfl
    · intro x
      obtain ⟨i, y, rfl⟩ := h₁ x
      exact ⟨(Discrete.functor F).ιColimitType ⟨i⟩ y, rfl⟩

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

Goal state before:
pp: z₁ z₂ : ZMod 2
au : Additive ℤˣ
⊢ Additive.toMul ((z₁ * z₂) • au) = Additive.toMul (z₁ • z₂ • au)

Tactic:
dsimp only [ZMod.smul_units_def, toMul_nsmul]

Goal state after:
z₁ z₂ : ZMod 2
au : Additive ℤˣ
⊢ Additive.toMul au ^ (z₁ * z₂).val = (Additive.toMul au ^ z₂.val) ^ z₁.val
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: case pos
n₁ n₂ : ℤ
h₂ : Even n₂
⊢ n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)

pp: case neg
n₁ n₂ : ℤ
h₂ : ¬Even n₂
⊢ n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)

Tactic:
· rw [negOnePow_even _ h₂, Int.even_sub, negOnePow_eq_one_iff]
    tauto

Goal state after:
case neg
n₁ n₂ : ℤ
h₂ : ¬Even n₂
⊢ n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)
Module: Mathlib.Order.Circular

Goal state before:
pp: α : Type u_1
inst✝ : CircularOrder α
a b : α
⊢ (cIoo a b)ᶜ = cIcc b a

Tactic:
by
  ext
  rw [Set.mem_cIcc, btw_iff_not_sbtw, cIoo, mem_compl_iff, mem_ofPred]

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

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

Tactic:
simpa only [sub_eq_add_neg] using h.add_const (-a)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddCommGroup α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
n : ℤ
⊢ f (n • c - x) = ↑n.negOnePow • f (-x)

Tactic:
rw [sub_eq_add_neg, add_comm]
  exact h.add_zsmul_eq n

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

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

Tactic:
simpa only [sub_eq_add_neg] using h.add_const (-a)

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

Goal state before:
pp: α : Type u_1
f : ℕ → α
a : ℕ
hf : Periodic f a
n : ℕ
⊢ f (n % a) = f n

Tactic:
conv_rhs => rw [← n.mod_add_div a, mul_comm, ← Nat.nsmul_eq_mul, hf.nsmul]

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
R : Type u
inst✝⁴ : Ring R
ι : Type w
M : ι → Type v
inst✝³ : Small.{v, u} R
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), Injective R (M i)
X Y : Type (max v w)
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
g : X →ₗ[R] (i : ι) → M i
l : (i : ι) → Y →ₗ[R] M i
hl : ∀ (i : ι), l i ∘ₗ f = LinearMap.proj i ∘ₗ g
x : X
⊢ (LinearMap.pi l) (f x) = g x

Tactic:
ext i

Goal state after:
R✝ : Type u
inst✝⁷ : Ring R✝
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R✝ Q
R : Type u
inst✝⁴ : Ring R
ι : Type w
M : ι → Type v
inst✝³ : Small.{v, u} R
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), Injective R (M i)
X Y : Type (max v w)
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
g : X →ₗ[R] (i : ι) → M i
l : (i : ι) → Y →ₗ[R] M i
hl : ∀ (i : ι), l i ∘ₗ f = LinearMap.proj i ∘ₗ g
x : X
i : ι
⊢ (LinearMap.pi l) (f x) i = g x i
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
hn : 2 < n
this✝¹ : Fact (1 < n)
this✝ : NeZero n
this : 2 = orderOf (-1)
⊢ Even (φ n)

Tactic:
← ZMod.card_units_eq_totient,

Goal state after:
n : ℕ
hn : 2 < n
this✝¹ : Fact (1 < n)
this✝ : NeZero n
this : 2 = orderOf (-1)
⊢ Even (Fintype.card (ZMod n)ˣ)
Module: Mathlib.Data.Set.Constructions

Goal state before:
pp: α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P : Set α
H : P ∈ finiteInterClosure (insert A S)
⊢ P ∈ S ∨ ∃ Q ∈ S, P = A ∩ Q

Tactic:
induction H with
  | basic h =>
    cases h
    · exact Or.inr ⟨Set.univ, cond.univ_mem, by simpa⟩
    · exact Or.inl (by assumption)
  | univ => exact Or.inl cond.univ_mem
  | @inter T1 T2 _ _ h1 h2 =>
    rcases h1 with (h | ⟨Q, hQ, rfl⟩) <;> rcases h2 with (i | ⟨R, hR, rfl⟩)
    · exact Or.inl (cond.inter_mem h i)
    · exact
        Or.inr ⟨T1 ∩ R, cond.inter_mem h hR, by simp only [← Set.inter_assoc, Set.inter_comm _ A]⟩
    · exact Or.inr ⟨Q ∩ T2, cond.inter_mem hQ i, by simp only [Set.inter_assoc]⟩
    · exact
        Or.inr
          ⟨Q ∩ R, cond.inter_mem hQ hR, by
            ext x
            constructor <;> simp +contextual⟩

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

Goal state before:
pp: case mpr.inl
m n : ℕ
h : φ m = 1
⊢ Coprime 1 (φ n)

pp: case mpr.inr
m n : ℕ
h : φ n = 1
⊢ (φ m).Coprime 1

Tactic:
exacts [Nat.coprime_one_left _, Nat.coprime_one_right _]

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

Goal state before:
pp: case inr
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ c ^ (2 * (c ^ 2 + d + 1) + d') < (2 * (c ^ 2 + d + 1) + d' - d)!

Tactic:
refine (Nat.le_mul_of_pos_right _ (Nat.pow_pos (n := d') c0)).trans_lt ?_

Goal state after:
case inr
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ c ^ (2 * (c ^ 2 + d + 1) + d') * c ^ d' < (2 * (c ^ 2 + d + 1) + d' - d)!
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: c d : ℕ
⊢ ∀ᶠ (n : ℕ) in atTop, c ^ n < (n - d)!

Tactic:
by
  rw [eventually_atTop]
  refine ⟨2 * (c ^ 2 + d + 1), ?_⟩
  intro n hn
  obtain ⟨d', rfl⟩ := Nat.exists_eq_add_of_le hn
  obtain (rfl | c0) := c.eq_zero_or_pos
  · simp [Nat.two_mul, ← Nat.add_assoc, Nat.add_right_comm _ 1, Nat.factorial_pos]
  refine (Nat.le_mul_of_pos_right _ (Nat.pow_pos (n := d') c0)).trans_lt ?_
  convert_to! (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2 + (c ^ 2 + d' + d + 1) + 1)!
  · rw [← pow_mul, ← pow_add]
    congr 1
    lia
  · congr 1
    lia
  refine (lt_of_lt_of_le ?_ Nat.factorial_mul_pow_le_factorial).trans_le <|
    (factorial_le (Nat.le_succ _))
  rw [← one_mul (_ ^ _ : ℕ)]
  apply Nat.mul_lt_mul_of_le_of_lt
  · exact Nat.one_le_of_lt (Nat.factorial_pos _)
  · exact Nat.pow_lt_pow_left (Nat.lt_succ_self _) (Nat.succ_ne_zero _)
  · exact (Nat.factorial_pos _)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst✝ : k.IsCountablyGenerated
⊢ Tendsto f k l ↔ ∀ (x : ℕ → α), Tendsto x atTop k → Tendsto (f ∘ x) atTop l

Tactic:
by
  refine ⟨fun h x hx => h.comp hx, fun H s hs => ?_⟩
  contrapose! H
  have : NeBot (k ⊓ 𝓟 (f ⁻¹' sᶜ)) := by simpa [neBot_iff, inf_principal_eq_bot]
  rcases (k ⊓ 𝓟 (f ⁻¹' sᶜ)).exists_seq_tendsto with ⟨x, hx⟩
  rw [tendsto_inf, tendsto_principal] at hx
  refine ⟨x, hx.1, fun h => ?_⟩
  rcases (hx.2.and (h hs)).exists with ⟨N, hnotMem, hmem⟩
  exact hnotMem hmem

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp (-a) b = -(toIocDiv hp a (-b) + 1)

Tactic:
by
  simpa only [neg_neg] using toIcoDiv_neg hp (-a) (-b)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
⊢ (iInf f).lift g = ⨅ i, (f i).lift g

Tactic:
refine lift_iInf_le.antisymm fun s => ?_
  have H : ∀ t ∈ iInf f, ⨅ i, (f i).lift g ≤ g t := by
    intro t ht
    refine iInf_sets_induct ht ?_ fun hs ht => ?_
    · inhabit ι
      exact iInf₂_le_of_le default univ (iInf_le _ univ_mem)
    · rw [hg]
      exact le_inf (iInf₂_le_of_le _ _ <| iInf_le _ hs) ht
  simp only [mem_lift_sets (Monotone.of_map_inf hg), exists_imp, and_imp]
  exact fun t ht hs => H t ht hs

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: case mpr
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
x : X
⊢ ∀ (o : Set X), IsOpen o → x ∈ o → (o ∩ s).Nonempty

Tactic:
intro U

Goal state after:
case mpr
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
x : X
U : Set X
⊢ IsOpen U → x ∈ U → (U ∩ s).Nonempty
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case inl
α : 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₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
h₃₁ : x₃' ≤ x₁ + p
⊢ x₃' ≤ toIocMod hp x₂' x₁

Tactic:
suffices hIoc₂₁ : toIocMod hp x₂' x₁ = x₁ + p from hIoc₂₁.trans_ge h₃₁

Goal state after:
case inl
α : 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₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
h₃₁ : x₃' ≤ x₁ + p
⊢ toIocMod hp x₂' x₁ = x₁ + p
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a : α
⊢ ⋃ n, Ioc (a + n • p) (a + (n + 1) • p) = univ

Tactic:
by
  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: 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 α := ⋯
⊢ 𝓝 a ≤ n a

Tactic:
intro U

Goal state after:
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 α := TopologicalSpace.mkOfNhds n
U : Set α
⊢ U ∈ n a → U ∈ 𝓝 a
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: 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))
h₀ : Set X
u₀ v₀ : ℕ → Set X
h₀_cov : h₀ ⊆ ⋃ n, u₀ n
dis : ∀ (n : ℕ), Disjoint (closure[inst✝] (v₀ n)) h₀
x : X
xinh : x ∈ h₀
⊢ x ∈ ⋃ n, u₀ n \ closure[inst✝] (⋃ m, ⋃ (_ : m ≤ n), v₀ m)

Tactic:
by
      rcases h₀_cov xinh with ⟨un, ⟨n, rfl⟩, xinun⟩
      simp only [mem_iUnion]
      refine ⟨n, xinun, ?_⟩
      simp_all only [closure_iUnion₂_le_nat, disjoint_right, mem_iUnion,
        exists_false, not_false_eq_true]

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
⊢ s = (s ∪ t) ∩ u

Tactic:
union_inter_distrib_right,

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 ∩ u ∪ t ∩ u
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
⊢ s = (s ∪ t) ∩ vᶜ

Tactic:
union_inter_distrib_right,

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 ∩ vᶜ ∪ t ∩ vᶜ
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
⊢ IsClosed[inst✝] s ↔ ∀ (x : X), f x ∈ closure[inst✝¹] (f '' s) → x ∈ s

Tactic:
rw [hf.eq_induced, isClosed_induced_iff']

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
⊢ v ⊆ sᶜ

Tactic:
exact (huv.mono_left hsu).subset_compl_left

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
h : X ≃ₜ Y
f : Z → X
hf : IsOpenMap (⇑h ∘ f)
⊢ IsOpenMap (id ∘ f)

Tactic:
← h.symm_comp_self,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
h : X ≃ₜ Y
f : Z → X
hf : IsOpenMap (⇑h ∘ f)
⊢ IsOpenMap ((⇑h.symm ∘ ⇑h) ∘ f)
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
⊢ IsQuotientMap f ↔ Surjective f ∧ ∀ (s : Set Y), IsClosed[inst✝] s ↔ IsClosed[inst✝¹] (f ⁻¹' s)

Tactic:
isQuotientMap_iff,

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsCoinducing f ∧ Surjective f ↔ Surjective f ∧ ∀ (s : Set Y), IsClosed[inst✝] s ↔ IsClosed[inst✝¹] (f ⁻¹' s)
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
hf : IsQuotientMap f
⊢ IsQuotientMap (g ∘ f) ↔ IsQuotientMap g

Tactic:
isQuotientMap_iff,

Goal state after:
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
hf : IsQuotientMap f
⊢ IsCoinducing (g ∘ f) ∧ Surjective (g ∘ f) ↔ IsQuotientMap g
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
hf : IsQuotientMap f
⊢ IsCoinducing (g ∘ f) ∧ Surjective (g ∘ f) ↔ IsQuotientMap g

Tactic:
isQuotientMap_iff,

Goal state after:
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
hf : IsQuotientMap f
⊢ IsCoinducing (g ∘ f) ∧ Surjective (g ∘ f) ↔ IsCoinducing g ∧ Surjective g
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
s : Set α
T : Set (TopologicalSpace α)
⊢ IsOpen[sSup T] s ↔ ∀ t ∈ T, IsOpen s

Tactic:
by
  simp +instances only [sSup_eq_iSup, isOpen_iSup_iff]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
⊢ (∀ x ∈ s, ContinuousWithinAt f s x) → ∀ (x : ↑s), ContinuousAt (s.domRestrict f) x

Tactic:
rintro h ⟨x, xs⟩
    exact (continuousWithinAt_iff_continuousAt_domRestrict f xs).mp (h x xs)

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 β
⊢ (∃ t_1, IsOpen[inst✝¹] t_1 ∧ Subtype.val ⁻¹' t_1 = Subtype.val ⁻¹' f ⁻¹' t) ↔
    ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
simp only [Subtype.preimage_coe_eq_preimage_coe_iff]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
x : { x // x ∈ s }
⊢ comap Subtype.val (𝓝[range Subtype.val] ↑x) = comap Subtype.val (𝓝[s] ↑x)

Tactic:
Subtype.range_val

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
x : { x // x ∈ s }
⊢ comap Subtype.val (𝓝[s] ↑x) = comap Subtype.val (𝓝[s] ↑x)
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsClosed[instTopologicalSpaceSum] (range inl)

Tactic:
by
  rw [← isOpen_compl_iff, compl_range_inl]
  exact isOpen_range_inr

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
t : Set ↑s
⊢ 𝓝ˢ[range Subtype.val] (Subtype.val '' t) = 𝓝ˢ[s] (Subtype.val '' t)

Tactic:
Subtype.range_val

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
t : Set ↑s
⊢ 𝓝ˢ[s] (Subtype.val '' t) = 𝓝ˢ[s] (Subtype.val '' t)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
x : ↑s
⊢ 𝓝[range Subtype.val] ↑x = 𝓝[s] ↑x

Tactic:
Subtype.range_val

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
x : ↑s
⊢ 𝓝[s] ↑x = 𝓝[s] ↑x
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
p : X → Prop
x : X
hx : p x
h : ∀ᶠ (x : X) in 𝓝 x, p x
⊢ range Subtype.val ∈ 𝓝 ↑⟨x, hx⟩

Tactic:
Subtype.range_val

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
p : X → Prop
x : X
hx : p x
h : ∀ᶠ (x : X) in 𝓝 x, p x
⊢ p ∈ 𝓝 ↑⟨x, hx⟩
Module: Mathlib.Topology.Constructions.SumProd

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

Tactic:
ext i

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
i : X ⊕ Y
⊢ ((Homeomorph.refl X).sumCongr (Homeomorph.refl Y)) i = (Homeomorph.refl (X ⊕ Y)) i
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: 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''
⊢ (h₁.sumCongr h₂).trans (h₃.sumCongr h₄) = (h₁.trans h₃).sumCongr (h₂.trans h₄)

Tactic:
ext i

Goal state after:
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''
i : X ⊕ Y
⊢ ((h₁.sumCongr h₂).trans (h₃.sumCongr h₄)) i = ((h₁.trans h₃).sumCongr (h₂.trans h₄)) i
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 : β → γ
t : Set β
y : β
hg : ContinuousWithinAt g t y
hf : ContinuousWithinAt f s x
hy : f x = y
⊢ ContinuousWithinAt (g ∘ f) (s ∩ f ⁻¹' t) x

Tactic:
by
  subst hy; exact hg.comp_inter hf

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 : α × β
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (fun x_1 ↦ f (x_1, x.2)) {a | (a, x.2) ∈ s} x.1

Tactic:
by
  rw [← x.eta]; simp_rw [ContinuousWithinAt, nhdsWithin, nhds_prod_eq, nhds_discrete, prod_pure,
    ← map_inf_principal_preimage]; rfl

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : IsOpenMap (s.domRestrict f)
finv : β → α
hleft : LeftInvOn finv f s
t : Set α
ht : IsOpen[inst✝¹] t
⊢ IsOpen[inst✝] (s.domRestrict f '' Subtype.val ⁻¹' t)

Tactic:
exact h _ (ht.preimage continuous_subtype_val)

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_5
s : ι → Set α
hf : ∀ (i : ι), ContinuousOn f (s i)
hs : ∀ (i : ι), IsOpen[inst✝¹] (s i)
⊢ ContinuousOn f (⋃ i, s i)

Tactic:
rintro x ⟨si, ⟨i, rfl⟩, hxsi⟩
  exact (hf i).continuousAt ((hs i).mem_nhds hxsi) |>.continuousWithinAt

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case h
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I).pi t ⊆ s
i : ι
hi : i ∈ I
⊢ t i ⊆ t i ∧ IsOpen[T i] (t i) ∧ a i ∈ t i

Tactic:
exact ⟨Subset.rfl, (h1 i) hi⟩

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
⊢ (∀ (i : ι), Continuous[coinduced (Sigma.mk i) (inst✝¹ i), inst✝] f) ↔
    ∀ (i : ι), Continuous[inst✝¹ i, inst✝] fun a ↦ f ⟨i, a⟩

Tactic:
exact forall_congr' fun _ => continuous_coinduced_dom

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case a
α : Type u
t : TopologicalSpace α
inst✝¹ : Countable α
inst✝ : FirstCountableTopology α
b : α → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun i ↦ b x i
x : α
⊢ 𝓝 x ≤ 𝓝 x

Tactic:
(hbb x).ge_iff

Goal state after:
case a
α : Type u
t : TopologicalSpace α
inst✝¹ : Countable α
inst✝ : FirstCountableTopology α
b : α → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun i ↦ b x i
x : α
⊢ ∀ (i' : ℕ), True → b x i' ∈ 𝓝 x