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

Goal state before:
pp: ⊢ ∀ {X' X : GrpCat} {Y : CommGrpCat} (f : X' ⟶ X) (g : X ⟶ (forget₂ CommGrpCat GrpCat).obj Y),
    ((ConcreteCategory.homEquiv.trans Abelianization.lift.symm).trans ConcreteCategory.homEquiv.symm).symm (f ≫ g) =
      abelianize.map f ≫
        ((ConcreteCategory.homEquiv.trans Abelianization.lift.symm).trans ConcreteCategory.homEquiv.symm).symm g

Tactic:
intros

Goal state after:
X'✝ X✝ : GrpCat
Y✝ : CommGrpCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ CommGrpCat GrpCat).obj Y✝
⊢ ((ConcreteCategory.homEquiv.trans Abelianization.lift.symm).trans ConcreteCategory.homEquiv.symm).symm (f✝ ≫ g✝) =
    abelianize.map f✝ ≫
      ((ConcreteCategory.homEquiv.trans Abelianization.lift.symm).trans ConcreteCategory.homEquiv.symm).symm g✝
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: X'✝ X✝ : GrpCat
Y✝ : CommGrpCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ CommGrpCat GrpCat).obj Y✝
x✝ : ↑(abelianize.obj X'✝)
⊢ ∀ (x : ↑X'✝),
    (CommGrpCat.Hom.hom
          (abelianize.map f✝ ≫
            ((ConcreteCategory.homEquiv.trans Abelianization.lift.symm).trans ConcreteCategory.homEquiv.symm).symm g✝))
        (Abelianization.of x) =
      (ConcreteCategory.homEquiv.symm.symm (f✝ ≫ g✝)) x

Tactic:
intros

Goal state after:
X'✝ X✝ : GrpCat
Y✝ : CommGrpCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ CommGrpCat GrpCat).obj Y✝
x✝¹ : ↑(abelianize.obj X'✝)
x✝ : ↑X'✝
⊢ (CommGrpCat.Hom.hom
        (abelianize.map f✝ ≫
          ((ConcreteCategory.homEquiv.trans Abelianization.lift.symm).trans ConcreteCategory.homEquiv.symm).symm g✝))
      (Abelianization.of x✝) =
    (ConcreteCategory.homEquiv.symm.symm (f✝ ≫ g✝)) x✝
Module: Mathlib.Algebra.Category.Grp.Adjunctions

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

Tactic:
intros

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

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

Tactic:
intros

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

Goal state before:
pp: k : ℤ
⊢ (k + k).negOnePow = 1

Tactic:
rw [negOnePow_add, units_mul_self]

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
a b p : G
⊢ a ≡ b [PMOD p] ↔ ↑a = ↑b

Tactic:
by
  rw [modEq_comm]
  simp_rw [modEq_iff_eq_add_zsmul, QuotientAddGroup.eq_iff_sub_mem, AddSubgroup.mem_zmultiples_iff,
    eq_sub_iff_add_eq', eq_comm]

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

Goal state after:
case inl
K : Type u_1
inst✝¹ : DivisionSemiring K
m : ℕ
inst✝ : CharZero K
hnm : 0 ∣ m
⊢ ↑(m / 0) = ↑m / ↑0

case inr
K : Type u_1
inst✝¹ : DivisionSemiring K
m n : ℕ
inst✝ : CharZero K
hnm : n ∣ m
hn : n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: case e_a
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
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑x = ↑⟨a, ha⟩ + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 :
  (extendIdealTo i f h y) r =
    ↑(extensionOfMax i f).toLinearPMap ⟨r • y - snd i x • y, ⋯⟩ + (extendIdealTo i f h y) (snd i x)
⊢ ↑(fst i x) = a + (r • y - snd i x • y)

Tactic:
add_sub,

Goal state after:
case e_a
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
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑x = ↑⟨a, ha⟩ + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 :
  (extendIdealTo i f h y) r =
    ↑(extensionOfMax i f).toLinearPMap ⟨r • y - snd i x • y, ⋯⟩ + (extendIdealTo i f h y) (snd i x)
⊢ ↑(fst i x) = a + r • y - snd i x • y
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: n : ℕ
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
⊢ f n = n.factorization.prod fun p k ↦ f (p ^ k)

Tactic:
obtain rfl | hn := eq_or_ne n 0

Goal state after:
case inl
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
⊢ f 0 = (factorization 0).prod fun p k ↦ f (p ^ k)

case inr
n : ℕ
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
hn : n ≠ 0
⊢ f n = n.factorization.prod fun p k ↦ f (p ^ k)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
⊢ φ n * ?m.28 / ?m.28 = (n / ∏ p ∈ n.primeFactors, p) * ∏ p ∈ n.primeFactors, (p - 1)

pp: n : ℕ
⊢ 0 < ?m.28

pp: n : ℕ
⊢ ℕ

Tactic:
totient_mul_prod_primeFactors,

Goal state after:
n : ℕ
⊢ (n * ∏ p ∈ n.primeFactors, (p - 1)) / ∏ p ∈ n.primeFactors, p =
    (n / ∏ p ∈ n.primeFactors, p) * ∏ p ∈ n.primeFactors, (p - 1)

n : ℕ
⊢ 0 < ∏ p ∈ n.primeFactors, p
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ a.primeFactors, p ∣ a

Tactic:
apply prod_primeFactors_dvd

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

Goal state before:
pp: case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ b.primeFactors, p ∣ b

Tactic:
apply prod_primeFactors_dvd

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

Goal state before:
pp: case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ (a.gcd b).primeFactors, p ∣ a.gcd b

Tactic:
apply prod_primeFactors_dvd

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

Goal state before:
pp: case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ (a * b).primeFactors, p ∣ a * b

Tactic:
apply prod_primeFactors_dvd

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

Goal state before:
pp: a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ a.gcd b * (a * b) / ((∏ p ∈ (a.gcd b).primeFactors, p) * ∏ p ∈ (a * b).primeFactors, p) *
      ((∏ p ∈ (a.gcd b).primeFactors, (p - 1)) * ∏ p ∈ (a * b).primeFactors, (p - 1)) =
    a * b / ((∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p) *
        ((∏ p ∈ a.primeFactors, (p - 1)) * ∏ p ∈ b.primeFactors, (p - 1)) *
      a.gcd b

Tactic:
apply prod_primeFactors_dvd

Goal state after:
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ a.gcd b * (a * b) / ((∏ p ∈ (a.gcd b).primeFactors, p) * ∏ p ∈ (a * b).primeFactors, p) *
      ((∏ p ∈ (a.gcd b).primeFactors, (p - 1)) * ∏ p ∈ (a * b).primeFactors, (p - 1)) =
    a * b / ((∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p) *
        ((∏ p ∈ a.primeFactors, (p - 1)) * ∏ p ∈ b.primeFactors, (p - 1)) *
      a.gcd b
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
this : φ a < φ (p * a * d)
⊢ False

Tactic:
rw [← mul_assoc, mul_comm a] at h'

Goal state after:
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (p * a * d)
hb : ¬a * (p * d) = 0
this : φ a < φ (p * a * d)
⊢ False
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 : α
⊢ (c ∈ Set.Ico a (a + p) ∧ ∃ z, b = c + z • p) → toIcoMod hp a b = c

Tactic:
simp_rw [← @sub_eq_iff_eq_add]

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ (c ∈ Set.Ico a (a + p) ∧ ∃ z, b - z • p = c) → toIcoMod hp a b = c
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 : α
⊢ (c ∈ Set.Ioc a (a + p) ∧ ∃ z, b = c + z • p) → toIocMod hp a b = c

Tactic:
simp_rw [← @sub_eq_iff_eq_add]

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ (c ∈ Set.Ioc a (a + p) ∧ ∃ z, b - z • p = c) → toIocMod hp a b = c
Module: Mathlib.Topology.Basic

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

Tactic:
← sUnion_empty

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
⊢ IsOpen[inst✝] (⋃₀ ∅)
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: case refine_2
α : Type u_1
γ : Type u_3
ι : Sort u_6
p : ι → Prop
s✝ : ι → Set α
f : Filter α
hf : f.HasBasis p s✝
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), (g (s✝ i)).HasBasis (pg i) (sg i)
gm : Monotone g
s : Set γ
⊢ (∃ i ∈ f.sets, s ∈ g i) ↔ ∃ i, p i ∧ ∃ x, pg i x ∧ sg i x ⊆ s

Tactic:
· simp only [← (hg _).mem_iff]
    exact hf.exists_iff fun t₁ t₂ ht H => gm ht H

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

Goal state before:
pp: case refine_1
α : 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
s : Set β
t : Set α
ht : t ∈ iInf f
⊢ ⨅ i, (f i).lift g ≤ g univ

pp: case refine_2
α : 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
s : Set β
t : Set α
ht✝ : t ∈ iInf f
i✝ : ι
s₁✝ s₂✝ : Set α
hs : s₁✝ ∈ f i✝
ht : ⨅ i, (f i).lift g ≤ g s₂✝
⊢ ⨅ i, (f i).lift g ≤ g (s₁✝ ∩ s₂✝)

Tactic:
· inhabit ι
      exact iInf₂_le_of_le default univ (iInf_le _ univ_mem)

Goal state after:
case refine_2
α : 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
s : Set β
t : Set α
ht✝ : t ∈ iInf f
i✝ : ι
s₁✝ s₂✝ : Set α
hs : s₁✝ ∈ f i✝
ht : ⨅ i, (f i).lift g ≤ g s₂✝
⊢ ⨅ i, (f i).lift g ≤ g (s₁✝ ∩ s₂✝)
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
s₁ s₂ : Set X
inst✝ : TopologicalSpace X
⊢ IsClosed[inst✝] s₁ → IsClosed[inst✝] s₂ → IsClosed[inst✝] (s₁ ∪ s₂)

Tactic:
simpa only [← isOpen_compl_iff, compl_union] using IsOpen.inter

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 : toIcoMod hp a b = toIcoMod hp a c
| c - (toIcoMod hp a b + toIcoDiv hp a b • p)

Tactic:
← toIcoMod_add_toIcoDiv_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 : toIcoMod hp a b = toIcoMod hp a c
| toIcoMod hp a c + toIcoDiv hp a c • p - (toIcoMod hp a b + toIcoDiv hp a b • p)
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ frontier sᶜ = frontier s

Tactic:
simp only [frontier_eq_closure_inter_closure, compl_compl, inter_comm]

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ ClusterPt x F ↔ ¬Disjoint (𝓝 x) F

Tactic:
disjoint_iff,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ ClusterPt x F ↔ ¬𝓝 x ⊓ F = ⊥
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
f : Filter X
H : 𝓝 x ≤ f
⊢ ClusterPt x f

Tactic:
by
  simp only [ClusterPt, inf_eq_left.mpr H, nhds_neBot]

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 : α
⊢ toIcoMod hp 0 (-(b - a)) = p - toIocMod hp 0 (b - a)

Tactic:
toIcoMod_neg,

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

Goal state before:
pp: case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
⊢ ClusterPt x (𝓟 C) → x ∈ C ∨ AccPt x (𝓟 C)

pp: case mpr
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
⊢ x ∈ C ∨ AccPt x (𝓟 C) → ClusterPt x (𝓟 C)

Tactic:
· intro h
    by_contra! hc
    rw [accPt_principal_iff_clusterPt] at hc
    simp_all only [not_false_eq_true, sdiff_singleton_eq_self, not_true_eq_false, hc.1]

Goal state after:
case mpr
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
⊢ x ∈ C ∨ AccPt x (𝓟 C) → ClusterPt x (𝓟 C)
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case left
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬x₃ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
h : x₃ ≡ x₂ [PMOD p]
⊢ False

Tactic:
exact h₁₂₃.2 (left_lt_toIocMod _ _ _).le

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

Tactic:
by
  constructor
  · suffices h : ¬x₃ ≡ x₂ [PMOD p] by
      have h₁₂₃' := toIxxMod_cyclic_left _ (toIxxMod_cyclic_left _ h₁₂₃.1)
      have h₂₃₄' := toIxxMod_cyclic_left _ (toIxxMod_cyclic_left _ h₂₃₄.1)
      rw [(not_modEq_iff_toIcoMod_eq_toIocMod hp).1 h] at h₂₃₄'
      exact toIxxMod_cyclic_left _ (h₁₂₃'.trans h₂₃₄')
    by_contra h
    rw [(modEq_iff_toIcoMod_eq_left hp).1 h] at h₁₂₃
    exact h₁₂₃.2 (left_lt_toIocMod _ _ _).le
  · rw [not_le] at h₁₂₃ h₂₃₄ ⊢
    exact (h₁₂₃.2.trans_le (toIcoMod_le_toIocMod _ x₃ x₂)).trans h₂₃₄.2

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
h : IsClosed[inst✝] t
⊢ 𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ tᶜ = 𝓝ˢ (s ∩ t) ⊔ 𝓟 tᶜ

Tactic:
h.isOpen_compl.nhdsSet_eq

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
h : IsClosed[inst✝] t
⊢ 𝓝ˢ (s ∩ t) ⊔ 𝓟 tᶜ = 𝓝ˢ (s ∩ t) ⊔ 𝓟 tᶜ
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ DiscreteTopology α ↔ ∀ (x : α), 𝓝 x = pure x

Tactic:
by
  simp only [discreteTopology_iff_singleton_mem_nhds]
  apply forall_congr' (fun x ↦ ?_)
  simp [le_antisymm_iff, pure_le_nhds x]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
s : Set (Set α)
⊢ generateFrom (insert ∅ s) = generateFrom s

Tactic:
← sUnion_empty

Goal state after:
α : Type u_1
s : Set (Set α)
⊢ generateFrom (insert (⋃₀ ∅) s) = generateFrom s
Module: Mathlib.Topology.Order

Goal state before:
pp: case a
α : Type u
a : α
f : Filter α
x✝ : TopologicalSpace α := ⋯
⊢ 𝓝 a ≤ pure a ⊔ f

Tactic:
rintro t ⟨hat : a ∈ t, htf : t ∈ f⟩

Goal state after:
case a
α : Type u
a : α
f : Filter α
x✝ : TopologicalSpace α := nhdsAdjoint a f
t : Set α
hat : a ∈ t
htf : t ∈ f
⊢ t ∈ 𝓝 a
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
⊢ IsOpen[inst✝] (range f)

Tactic:
by
  rw [← image_univ]
  exact hf _ isOpen_univ

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsOpenMap f ↔ ∀ {u : Set X}, IsClosed[inst✝¹] u → IsClosed[inst✝] (kernImage f u)

Tactic:
IsOpenMap,

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ (∀ (U : Set X), IsOpen[inst✝¹] U → IsOpen[inst✝] (f '' U)) ↔
    ∀ {u : Set X}, IsClosed[inst✝¹] u → IsClosed[inst✝] (kernImage f u)
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 : IsOpenEmbedding g
⊢ IsOpenMap f ↔ IsOpenMap (g ∘ f)

Tactic:
by
  simp_rw [isOpenMap_iff_nhds_le, ← map_map, comp, ← hg.map_nhds_eq, map_le_map_iff hg.injective]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), DenseRange (f i)
⊢ Dense (univ.pi fun i ↦ range (f i))

Tactic:
exact dense_pi Set.univ (fun i _ => hf i)

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst✝¹] s
⊢ ContinuousOn f s ↔ ∀ (t : Set β), IsOpen[inst✝] t → IsOpen[inst✝¹] (s ∩ f ⁻¹' t)

Tactic:
rw [continuousOn_iff']
  constructor
  · intro h t ht
    rcases h t ht with ⟨u, u_open, hu⟩
    rw [inter_comm, hu]
    apply IsOpen.inter u_open hs
  · intro h t ht
    refine ⟨s ∩ f ⁻¹' t, h t ht, ?_⟩
    rw [@inter_comm _ s (f ⁻¹' t), inter_assoc, inter_self]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_1.refine_1
ι : 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 : (i : ι) → Set (A i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1
h2 : (↑I).pi t ⊆ s
i : ι
hi : i ∈ I
⊢ IsOpen[T i] ⋯.choose ∧ a i ∈ ⋯.choose

Tactic:
exact (h1 i).choose_spec.2

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
z : β
x : α
⊢ ∀ (x_1 : α), x_1 ≤ x ∧ z ∈ s x_1 → ∃ i, z ∈ s i

Tactic:
x'

Goal state after:
case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
z : β
x x' : α
⊢ x' ≤ x ∧ z ∈ s x' → ∃ i, z ∈ s i
Module: Mathlib.Topology.Bornology.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Bornology α
s : Set ι
f : ι → Set α
hs : s.Finite
⊢ IsBounded (⋃ i ∈ s, f i) ↔ ∀ i ∈ s, IsBounded (f i)

Tactic:
simp only [← isCobounded_compl_iff, compl_iUnion, isCobounded_biInter hs]

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

Goal state before:
pp: α : Type u_2
inst✝ : Bornology α
⊢ cobounded α = ⊥ ↔ BoundedSpace α

Tactic:
by
  rw [← isBounded_univ, isBounded_def, compl_univ, empty_mem_iff_bot]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : DiscreteTopology α
⊢ SeparableSpace α ↔ Countable α

Tactic:
by
  simp [separableSpace_iff, countable_univ_iff]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
⊢ Pi.topologicalSpace = Pi.topologicalSpace

Tactic:
simp +instances only [generateFrom_setOfPred_isOpen]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
X : Type u_9
f : X → (i : ι) → A i
⊢ induced f Pi.topologicalSpace = ⨅ i, induced (fun x ↦ f x i) inferInstance

Tactic:
simp_rw [Pi.topologicalSpace, induced_iInf, induced_compose, Function.comp_def]

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hc : S.Countable
hcomp : ∀ (s : ↑S), IsSigmaCompact ↑s
⊢ IsSigmaCompact (⋃₀ S)

Tactic:
have : Countable S := countable_coe_iff.mpr hc
  apply sUnion_eq_iUnion.symm ▸ isSigmaCompact_iUnion _ hcomp

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hf : S.Finite
hc : ∀ s ∈ S, IsCompact s
⊢ IsCompact (⋃₀ S)

Tactic:
rw [sUnion_eq_biUnion]; exact hf.isCompact_biUnion hc

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : x ∉ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}
h : x ∈ closure[inst✝²] {a | p a}ᶜ
⊢ x ∉ interior {a | p a}

Tactic:
closure_compl

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : x ∉ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}
h : x ∈ (interior {a | p a})ᶜ
⊢ x ∉ interior {a | p a}
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
H : StableUnderSpecialization s
| s

Tactic:
← H.Union_eq

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
H : StableUnderSpecialization s
| ⋃ x ∈ s, closure[inst✝] {x}
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
t : Set (SeparationQuotient X)
⊢ comap mk (𝓝ˢ t) = 𝓝ˢ (mk ⁻¹' t)

Tactic:
conv_lhs => rw [← image_preimage_eq t surjective_mk, comap_mk_nhdsSet_image]

Goal state after: