mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Mul M
inst✝ : ContinuousMul M
⊢ Continuous[instTopologicalSpaceProd, inst✝²] ((fun p ↦ p.1 * p.2) ∘ Prod.swap ∘ Prod.map MulOpposite.unop id)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: α : Type u_6
β : Type u_7
F : Type u_8
inst✝⁴ : FunLike F α β
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : MulHomClass F α β
tβ : TopologicalSpace β
inst✝ : ContinuousMul β
f : F
tα : TopologicalSpace α := TopologicalSpace.induced (⇑f) tβ
⊢ Continuous[instTopologicalSpaceProd, tβ] fun x ↦ f x.1 * f x.2

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: case hf
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace M
inst✝⁴ : Mul M
inst✝³ : ContinuousMul M
inst✝² : TopologicalSpace N
inst✝¹ : Mul N
inst✝ : ContinuousMul N
⊢ Continuous[instTopologicalSpaceProd, inst✝⁵] fun x ↦ x.1.1 * x.2.1

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: case hg
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace M
inst✝⁴ : Mul M
inst✝³ : ContinuousMul M
inst✝² : TopologicalSpace N
inst✝¹ : Mul N
inst✝ : ContinuousMul N
⊢ Continuous[instTopologicalSpaceProd, inst✝²] fun x ↦ x.1.2 * x.2.2

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: case hf
ι : Type u_1
α : Type u_2
M✝ : Type u_3
N✝ : Type u_4
X : Type u_5
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace M✝
inst✝⁷ : Mul M✝
inst✝⁶ : ContinuousMul M✝
M : Type u_6
N : Type u_7
inst✝⁵ : TopologicalSpace M
inst✝⁴ : Mul M
inst✝³ : SeparatelyContinuousMul M
inst✝² : TopologicalSpace N
inst✝¹ : Mul N
inst✝ : SeparatelyContinuousMul N
x✝ : M × N
⊢ Continuous[instTopologicalSpaceProd, inst✝⁵] fun x ↦ x✝.1 * x.1

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: case hg
ι : Type u_1
α : Type u_2
M✝ : Type u_3
N✝ : Type u_4
X : Type u_5
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace M✝
inst✝⁷ : Mul M✝
inst✝⁶ : ContinuousMul M✝
M : Type u_6
N : Type u_7
inst✝⁵ : TopologicalSpace M
inst✝⁴ : Mul M
inst✝³ : SeparatelyContinuousMul M
inst✝² : TopologicalSpace N
inst✝¹ : Mul N
inst✝ : SeparatelyContinuousMul N
x✝ : M × N
⊢ Continuous[instTopologicalSpaceProd, inst✝²] fun x ↦ x✝.2 * x.2

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: case hf
ι : Type u_1
α : Type u_2
M✝ : Type u_3
N✝ : Type u_4
X : Type u_5
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace M✝
inst✝⁷ : Mul M✝
inst✝⁶ : ContinuousMul M✝
M : Type u_6
N : Type u_7
inst✝⁵ : TopologicalSpace M
inst✝⁴ : Mul M
inst✝³ : SeparatelyContinuousMul M
inst✝² : TopologicalSpace N
inst✝¹ : Mul N
inst✝ : SeparatelyContinuousMul N
x✝ : M × N
⊢ Continuous[instTopologicalSpaceProd, inst✝⁵] fun x ↦ x.1 * x✝.1

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: case hg
ι : Type u_1
α : Type u_2
M✝ : Type u_3
N✝ : Type u_4
X : Type u_5
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace M✝
inst✝⁷ : Mul M✝
inst✝⁶ : ContinuousMul M✝
M : Type u_6
N : Type u_7
inst✝⁵ : TopologicalSpace M
inst✝⁴ : Mul M
inst✝³ : SeparatelyContinuousMul M
inst✝² : TopologicalSpace N
inst✝¹ : Mul N
inst✝ : SeparatelyContinuousMul N
x✝ : M × N
⊢ Continuous[instTopologicalSpaceProd, inst✝²] fun x ↦ x.2 * x✝.2

Tactic:
fun_prop

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

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
g : Y → Z
hg : IsProperMap g
hf : IsProperMap f
⊢ Continuous[inst✝², inst✝] (g ∘ f)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M₁ : Type u_6
M₂ : Type u_7
inst✝⁴ : TopologicalSpace M₂
inst✝³ : T2Space M₂
inst✝² : Mul M₁
inst✝¹ : Mul M₂
inst✝ : ContinuousMul M₂
x y : M₁
⊢ Continuous[Pi.topologicalSpace, inst✝⁴] fun x_1 ↦ x_1 x * x_1 y

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: case refine_1
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace M
inst✝² : Semigroup M
inst✝¹ : SeparatelyContinuousMul M
inst✝ : T2Space M
s : Subsemigroup M
hs : ∀ (x y : ↥s), x * y = y * x
this : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
x✝¹ x✝ : ↥s.topologicalClosure
x : M
hx : x ∈ s.topologicalClosure
y : M
hy : y ∈ s.topologicalClosure
⊢ ∀ (x : M), Continuous[inst✝³, inst✝³] (HMul.hMul x)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: case refine_2
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace M
inst✝² : Semigroup M
inst✝¹ : SeparatelyContinuousMul M
inst✝ : T2Space M
s : Subsemigroup M
hs : ∀ (x y : ↥s), x * y = y * x
this : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
x✝¹ x✝ : ↥s.topologicalClosure
x : M
hx : x ∈ s.topologicalClosure
y : M
hy : y ∈ s.topologicalClosure
⊢ ∀ (y : M), Continuous[inst✝³, inst✝³] fun x ↦ x * y

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: case refine_3
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace M
inst✝² : Semigroup M
inst✝¹ : SeparatelyContinuousMul M
inst✝ : T2Space M
s : Subsemigroup M
hs : ∀ (x y : ↥s), x * y = y * x
this : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
x✝¹ x✝ : ↥s.topologicalClosure
x : M
hx : x ∈ s.topologicalClosure
y : M
hy : y ∈ s.topologicalClosure
⊢ ∀ (x : M), Continuous[inst✝³, inst✝³] fun y ↦ y * x

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: case refine_4
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace M
inst✝² : Semigroup M
inst✝¹ : SeparatelyContinuousMul M
inst✝ : T2Space M
s : Subsemigroup M
hs : ∀ (x y : ↥s), x * y = y * x
this : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
x✝¹ x✝ : ↥s.topologicalClosure
x : M
hx : x ∈ s.topologicalClosure
y : M
hy : y ∈ s.topologicalClosure
⊢ ∀ (y : M), Continuous[inst✝³, inst✝³] fun x ↦ y * x

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Monoid M
inst✝⁵ : ContinuousMul M
R : Type u_6
A : Type u_7
inst✝⁴ : Monoid A
inst✝³ : SMul R A
inst✝² : IsScalarTower R A A
inst✝¹ : TopologicalSpace A
inst✝ : SeparatelyContinuousMul A
q : R
⊢ Continuous[inst✝¹, inst✝¹] fun x ↦ q • 1 * x

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Monoid M
inst✝⁵ : ContinuousMul M
R : Type u_6
A : Type u_7
inst✝⁴ : Monoid A
inst✝³ : SMul R A
inst✝² : SMulCommClass R A A
inst✝¹ : TopologicalSpace A
inst✝ : SeparatelyContinuousMul A
q : R
⊢ Continuous[inst✝¹, inst✝¹] fun x ↦ x * q • 1

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case refine_1
M : Type u_1
s : Set M
inst✝³ : Mul M
inst✝² : TopologicalSpace M
inst✝¹ : SeparatelyContinuousMul M
inst✝ : T2Space M
m : M
⊢ Continuous[inst✝², inst✝²] (HMul.hMul m)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case refine_2
M : Type u_1
s : Set M
inst✝³ : Mul M
inst✝² : TopologicalSpace M
inst✝¹ : SeparatelyContinuousMul M
inst✝ : T2Space M
m : M
⊢ Continuous[inst✝², inst✝²] fun x ↦ x * m

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : MonoidHomClass F α β
tβ : TopologicalSpace β
inst✝ : ContinuousInv β
f : F
_tα : TopologicalSpace α := TopologicalSpace.induced (⇑f) tβ
⊢ Continuous[TopologicalSpace.induced (⇑f) tβ, tβ] fun x ↦ (f x)⁻¹

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
U : Set G
hU : U ∈ 𝓝 1
x : G
hx : ∀ t ∈ 𝓝 x, (t ∩ U).Nonempty
⊢ ContinuousAt (fun y ↦ x / y) x

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : ContinuousMul A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen[inst✝⁵] U
this : ⇑φ ⁻¹' ⇑φ '' U = ⋃ k ∈ (↑φ).ker, (fun x ↦ x * k) ⁻¹' U
k : A
x✝ : k ∈ ↑(↑φ).ker
⊢ Continuous[inst✝⁵, inst✝⁵] fun x ↦ x * k

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Div G
inst✝ : ContinuousDiv G
a : G
⊢ Continuous[inst✝², inst✝²] fun x ↦ a / x

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Div G
inst✝ : ContinuousDiv G
a : G
⊢ Continuous[inst✝², inst✝²] fun x ↦ x / a

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
g₀ : G
hg₀ : g₀ ∈ interior V
g : G
x✝ : g ∈ K
⊢ Continuous[inst✝², inst✝²] fun x ↦ g₀ * g⁻¹ * x

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this :
  (fun x ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹)) = (fun p ↦ p.1 * p.2⁻¹) ∘ fun p ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ p.1 * p.2⁻¹

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case refine_1
G : Type w
H : Type x
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
inst✝¹ : SeparableSpace G
inst✝ : WeaklyLocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : L ∈ 𝓝 1
n : ℕ
⊢ IsCompact ((fun n ↦ (fun x ↦ x * denseSeq G n) ⁻¹' L) n)

Tactic:
exact (Homeomorph.mulRight _).isCompact_preimage.mpr hLc

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case refine_1
α : Type u
inst✝³ : Monoid α
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : ContinuousMul α
⊢ Continuous[instTopologicalSpaceProd, inst✝²] fun p ↦ p.1 * unop p.2

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case refine_2
α : Type u
inst✝³ : Monoid α
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : ContinuousMul α
⊢ Continuous[instTopologicalSpaceProd, inst✝²] fun p ↦ unop p.2 * p.1

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Group.GroupTopology

Goal state before:
pp: G : Type w
H : Type x
α : Type u
β : Type v
inst✝ : Group α
_t : TopologicalSpace α := ⊥
this : DiscreteTopology α
⊢ Continuous[instTopologicalSpaceProd, _t] fun p ↦ p.1 * p.2

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.GroupWithZero

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : ContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt ↿h (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))
hga : ¬g a = 0
⊢ ContinuousAt (↿h ∘ fun x ↦ (x, f x / g x)) a

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.ContinuousMonoidHom

Goal state before:
pp: F✝ : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹⁰ : Monoid A
inst✝⁹ : Monoid B
inst✝⁸ : Monoid C
inst✝⁷ : Monoid D
inst✝⁶ : TopologicalSpace A
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : TopologicalSpace D
F : Type u_7
inst✝² : FunLike F A B
inst✝¹ : MonoidHomClass F A B
inst✝ : ContinuousMapClass F A B
f : F
⊢ Continuous[inst✝⁶, inst✝⁵] ⇑f

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.ContinuousMonoidHom

Goal state before:
pp: G : Type u
inst✝⁵ : TopologicalSpace G
H : Type v
inst✝⁴ : TopologicalSpace H
M : Type u_1
N : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace N
inst✝¹ : Mul M
inst✝ : Mul N
⊢ Continuous id

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Field

Goal state before:
pp: K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
R : Type u_2
inst✝⁵ : DivisionSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : PosMulReflectLT R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousInv₀ R
⊢ Continuous (Units.val ∘ (unitsEquivPos R).invFun)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Field

Goal state before:
pp: K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
R : Type u_2
inst✝⁵ : DivisionSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : PosMulReflectLT R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousInv₀ R
x : { r // 0 < r }
⊢ ContinuousAt Subtype.val x

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
⊢ {x | 𝓝[>] x = ⊥}.Countable

Tactic:
simp only [nhdsGT_eq_bot_iff, ofPred_or]
  exact (subsingleton_isTop α).countable.union countable_setOfPred_covBy_right

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
inst✝¹ : (i : α) → Decidable (i ∈ s)
inst✝ : (i : β) → Decidable (i ∈ t)
h : e.IsImage s t
h' : e'.IsImage s t
⊢ LeftInvOn (t.piecewise ↑e.symm ↑e'.symm) (s.piecewise ↑e ↑e') (s.ite e.source e'.source)

Tactic:
rintro x (⟨he, hs⟩ | ⟨he, hs : x ∉ s⟩)
  · rw [piecewise_eq_of_mem _ _ _ hs, piecewise_eq_of_mem _ _ _ ((h he).2 hs), e.left_inv he]
  · rw [piecewise_eq_of_notMem _ _ _ hs, piecewise_eq_of_notMem _ _ _ ((h'.compl he).2 hs),
      e'.left_inv he]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
⊢ 𝓝 a ≤ 𝓝 a

Tactic:
simp only [nhds_eq_order, nhds_induced, comap_inf, comap_iInf, comap_principal]

Goal state after:
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
⊢ (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤
    (⨅ i ∈ Iio (f a), 𝓟 (f ⁻¹' Ioi i)) ⊓ ⨅ i ∈ Ioi (f a), 𝓟 (f ⁻¹' Iio i)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
⊢ {x | ∃ y < x, Ioo y x = ∅}.Countable

Tactic:
by
  simpa only [← covBy_iff_Ioo_eq] using countable_setOfPred_covBy_left

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ico a (a + p)
⊢ liftIco p a f ↑x = f x

Tactic:
by
  simp [liftIco, equivIco_coe_eq hx]

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
m : ℕ
hn : m < n
h0 : 0 < m
k : ℕ
hk : n * k = m
⊢ False

Tactic:
exact (Nat.le_of_dvd h0 ⟨_, hk.symm⟩).not_gt hn

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
m : ℤ
n : ℕ
hn : 0 < n
h : m.natAbs.gcd n = 1
⊢ addOrderOf ↑(↑m / ↑n * p) = n

Tactic:
cases m
  · simp only [Int.ofNat_eq_natCast, Int.cast_natCast, Int.natAbs_natCast] at h ⊢
    exact addOrderOf_div_of_gcd_eq_one hn h
  · simp only [Int.cast_negSucc, neg_div, neg_mul, coe_neg, addOrderOf_neg]
    exact addOrderOf_div_of_gcd_eq_one hn h

Goal state after:
Module: Mathlib.Algebra.Category.HopfAlgCat.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y : HopfAlgCat R
f : X ⟶ Y
x✝ : IsIso ((forget (HopfAlgCat R)).map f)
⊢ IsIso f

Tactic:
let i := asIso ((forget (HopfAlgCat.{v} R)).map f)

Goal state after:
R : Type u
inst✝ : CommRing R
X Y : HopfAlgCat R
f : X ⟶ Y
x✝ : IsIso ((forget (HopfAlgCat R)).map f)
i : (forget (HopfAlgCat R)).obj X ≅ (forget (HopfAlgCat R)).obj Y := asIso ((forget (HopfAlgCat R)).map f)
⊢ IsIso f
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
A : C
z₂ : A ⟶ S.cycles
⊢ z₂ ≫ S.homologyπ = 0 ↔ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ z₂ = x₁ ≫ S.toCycles

Tactic:
obtain ⟨x₂, hx₂, rfl⟩ : ∃ (x₂ : A ⟶ S.X₂) (hx₂ : x₂ ≫ S.g = 0), z₂ = S.liftCycles x₂ hx₂ :=
    ⟨z₂ ≫ S.iCycles, by simp, by simp [← cancel_mono S.iCycles, liftCycles_i]⟩

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
A : C
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ S.liftCycles x₂ hx₂ ≫ S.homologyπ = 0 ↔ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ S.liftCycles x₂ hx₂ = x₁ ≫ S.toCycles
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
r : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ ((r • f).sum fun f' s ↦ sum g fun g' t ↦ single (f' ≫ g') (s * t)) =
    r • sum f fun f' s ↦ sum g fun g' t ↦ single (f' ≫ g') (s * t)

Tactic:
Finsupp.sum_smul_index

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
r : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (sum f fun i a ↦ sum g fun g' t ↦ single (i ≫ g') (r * a * t)) =
    r • sum f fun f' s ↦ sum g fun g' t ↦ single (f' ≫ g') (s * t)

R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
r : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (i : X ⟶ Y), (sum g fun g' t ↦ single (i ≫ g') (0 * t)) = 0
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case e_g
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
h : X ⟶ Y
s : R
a✝ : X ⟶ Z
⊢ ((r • g).sum fun g' t ↦ single (h ≫ g') (s * t)) a✝ = (sum g fun a b ↦ r • single (h ≫ a) (s * b)) a✝

Tactic:
Finsupp.sum_smul_index

Goal state after:
case e_g
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
h : X ⟶ Y
s : R
a✝ : X ⟶ Z
⊢ (sum g fun i a ↦ single (h ≫ i) (s * (r * a))) a✝ = (sum g fun a b ↦ r • single (h ≫ a) (s * b)) a✝

case e_g
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
h : X ⟶ Y
s : R
a✝ : X ⟶ Z
⊢ ∀ (i : Y ⟶ Z), single (h ≫ i) (s * 0) = 0
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y : Free R C
f : X ⟶ Y
r : R
⊢ (sum (r • f) fun f' r ↦ r • F.map f') = r • sum f fun f' r ↦ r • F.map f'

Tactic:
Finsupp.sum_smul_index

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y : Free R C
f : X ⟶ Y
r : R
⊢ (sum f fun i a ↦ (r * a) • F.map i) = r • sum f fun f' r ↦ r • F.map f'

R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y : Free R C
f : X ⟶ Y
r : R
⊢ ∀ (i : X ⟶ Y), 0 • F.map i = 0
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y : Free R C
f : X ⟶ Y
r : R
⊢ (lift R F).map (r • f) = r • (lift R F).map f

Tactic:
by
    dsimp
    rw [Finsupp.sum_smul_index] <;> simp [Finsupp.smul_sum, mul_smul]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S S₁ S₂ S₃ X✝ Y✝ Z✝ : SnakeInput C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ pullback.map X✝.L₁.g X✝.v₀₁.τ₃ Z✝.L₁.g Z✝.v₀₁.τ₃ (x✝¹ ≫ x✝).f₁.τ₂ (x✝¹ ≫ x✝).f₀.τ₃ (x✝¹ ≫ x✝).f₁.τ₃ ⋯ ⋯ =
    pullback.map X✝.L₁.g X✝.v₀₁.τ₃ Y✝.L₁.g Y✝.v₀₁.τ₃ x✝¹.f₁.τ₂ x✝¹.f₀.τ₃ x✝¹.f₁.τ₃ ⋯ ⋯ ≫
      pullback.map Y✝.L₁.g Y✝.v₀₁.τ₃ Z✝.L₁.g Z✝.v₀₁.τ₃ x✝.f₁.τ₂ x✝.f₀.τ₃ x✝.f₁.τ₃ ⋯ ⋯

Tactic:
by dsimp [P]; cat_disch

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case single
R : Type u_1
inst✝⁸ : CommRing R
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u
inst✝⁶ : Category.{v, u} D
inst✝⁵ : Preadditive D
inst✝⁴ : Linear R D
F G : Free R C ⥤ D
inst✝³ : F.Additive
inst✝² : Functor.Linear R F
inst✝¹ : G.Additive
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f' : X ⟶ Y
r : R
⊢ r • F.map (single f' 1) ≫ α.hom.app Y = r • α.hom.app X ≫ G.map (single f' 1)

Tactic:
change r • (embedding R C ⋙ F).map f' ≫ _ = r • _ ≫ (embedding R C ⋙ G).map f'

Goal state after:
case single
R : Type u_1
inst✝⁸ : CommRing R
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u
inst✝⁶ : Category.{v, u} D
inst✝⁵ : Preadditive D
inst✝⁴ : Linear R D
F G : Free R C ⥤ D
inst✝³ : F.Additive
inst✝² : Functor.Linear R F
inst✝¹ : G.Additive
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f' : X ⟶ Y
r : R
⊢ r • (embedding R C ⋙ F).map f' ≫ α.hom.app Y = r • α.hom.app X ≫ (embedding R C ⋙ G).map f'
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w v)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
F : J → C
inst✝¹ : HasProduct F
inst✝ : PreservesLimit (Discrete.functor F) (forget C)
x : (j : J) → ToType (F j)
j : J
⊢ (productEquiv F) ((productEquiv F).symm x) j = x j

Tactic:
Equiv.apply_symm_apply

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w v)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
F : J → C
inst✝¹ : HasProduct F
inst✝ : PreservesLimit (Discrete.functor F) (forget C)
x : (j : J) → ToType (F j)
j : J
⊢ x j = x j