mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.none.inl.some.succ.refine_2
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
this : 0 < ω ^ a'.repr
i : ℕ
H : (a.oadd (m' + 1).succPNat 0).NF
⊢ (a'.oadd i.succPNat 0).repr < ω ^ a.repr

Tactic:
rw [repr, repr_zero, add_zero, iha.1, opow_succ]

Goal state after:
case oadd.inl.none.inl.some.succ.refine_2
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
this : 0 < ω ^ a'.repr
i : ℕ
H : (a.oadd (m' + 1).succPNat 0).NF
⊢ ω ^ a'.repr * ↑↑i.succPNat < ω ^ a'.repr * ω
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: case inl
p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
h : ∀ (m : ℕ), 0 ≠ m ^ q
⊢ 0 ^ p ≠ m ^ q

Tactic:
simpa using

Goal state after:
case inl
p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
h : ∀ (m : ℕ), 0 ≠ m ^ q
⊢ ¬0 ^ p = m ^ q
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
hn : n ≠ 0
h : n ^ p = m ^ q
f : ℕ →₀ ℕ := Finsupp.mapRange (fun x ↦ x / q) ⋯ n.factorization
hf : n.factorization = q • f
⊢ f 0 = 0

Tactic:
simpa using

Goal state after:
n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
hn : n ≠ 0
h : n ^ p = m ^ q
f : ℕ →₀ ℕ := Finsupp.mapRange (fun x ↦ x / q) ⋯ n.factorization
hf : n.factorization = q • f
⊢ f 0 = 0
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: case inr
n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
hn : n ≠ 0
h : n ^ p = m ^ q
f : ℕ →₀ ℕ := Finsupp.mapRange (fun x ↦ x / q) ⋯ n.factorization
z : ℕ
⊢ q ∣ n.factorization z

Tactic:
simpa using

Goal state after:
case inr
n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
hn : n ≠ 0
h : n ^ p = m ^ q
f : ℕ →₀ ℕ := Finsupp.mapRange (fun x ↦ x / q) ⋯ n.factorization
z : ℕ
⊢ q ∣ n.factorization z
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
hn : n ≠ 0
h : n ^ p = m ^ q
f : ℕ →₀ ℕ := Finsupp.mapRange (fun x ↦ x / q) ⋯ n.factorization
z : ℕ
⊢ p * n.factorization z = q * ?m.185

Tactic:
simpa using

Goal state after:
n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
hn : n ≠ 0
h : n ^ p = m ^ q
f : ℕ →₀ ℕ := Finsupp.mapRange (fun x ↦ x / q) ⋯ n.factorization
z : ℕ
⊢ p * n.factorization z = q * ?m.185
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: b : ℕ
hb : (b / 2).beq 0 = false
⊢ jacobiSymNat 0 b = 0

Tactic:
by
  rw [jacobiSymNat, Nat.cast_zero, jacobiSym.zero_left ?_]
  calc
    1 < 2 * 1       := by decide
    _ ≤ 2 * (b / 2) :=
      Nat.mul_le_mul_left _ (Nat.succ_le_of_lt (Nat.pos_of_ne_zero (Nat.ne_of_beq_eq_false hb)))
    _ ≤ b           := Nat.mul_div_le b 2

Goal state after:
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: case inr
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 ↑a = 1
hc' : c ≠ 0
⊢ jacobiSymNat a b = r

Tactic:
have : NeZero c := ⟨hc'⟩

Goal state after:
case inr
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 ↑a = 1
hc' : c ≠ 0
this : NeZero c
⊢ jacobiSymNat a b = r
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := ⋯
y : ℕ := ⋯
x : ℕ
ha : a ≠ x ^ d
hx' : x' = ↑x
h : a * y ^ d = b * x ^ d
⊢ x.Coprime y

Tactic:
simpa using

Goal state after:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := ⋯
y : ℕ := ⋯
x : ℕ
ha : a ≠ x ^ d
hx' : x' = ↑x
h : a * y ^ d = b * x ^ d
⊢ x.Coprime y
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: x y : ℝ
x_num x_den y_num y_den k_den : ℕ
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hd1 : k_den ^ y_den < x_den
hd2 : x_den < (k_den + 1) ^ y_den
hx_inv : Invertible ↑x_den
hx_eq : x = ↑x_num * ⅟↑x_den
⊢ Irrational (x ^ y)⁻¹

Tactic:
rw [← Real.inv_rpow (by simp only [hx_eq, invOf_eq_inv]; positivity)]

Goal state after:
x y : ℝ
x_num x_den y_num y_den k_den : ℕ
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hd1 : k_den ^ y_den < x_den
hd2 : x_den < (k_den + 1) ^ y_den
hx_inv : Invertible ↑x_den
hx_eq : x = ↑x_num * ⅟↑x_den
⊢ Irrational (x⁻¹ ^ y)
Module: Mathlib.Tactic.NormNum.RealSqrt

Goal state before:
pp: num denom : ℕ
inv : Invertible ↑denom
h₁ : 0 ≤ ↑↑num * ⅟↑denom
⊢ √(↑(Int.negOfNat num) * ⅟↑denom) = ↑0

Tactic:
simpa using

Goal state after:
num denom : ℕ
inv : Invertible ↑denom
h₁ : 0 ≤ ↑↑num * ⅟↑denom
⊢ 0 ≤ ↑num * (↑denom)⁻¹
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℕ
hnm : n.blt m = true
⊢ Icc m n = ∅

Tactic:
simpa using

Goal state after:
m n : ℕ
hnm : n.blt m = true
⊢ n < m
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℕ
s : Finset ℕ
hmn : m.ble n = true
hs : Icc (m + 1) n = s
⊢ m ≤ n

Tactic:
simpa using

Goal state after:
m n : ℕ
s : Finset ℕ
hmn : m.ble n = true
hs : Icc (m + 1) n = s
⊢ m ≤ n
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℤ
hnm : n < m
⊢ Icc m n = ∅

Tactic:
simpa using

Goal state after:
m n : ℤ
hnm : n < m
⊢ n < m
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℤ
s : Finset ℤ
hmn : m ≤ n
hs : Icc (m + 1) n = s
⊢ m ≤ n

Tactic:
simpa using

Goal state after:
m n : ℤ
s : Finset ℤ
hmn : m ≤ n
hs : Icc (m + 1) n = s
⊢ m ≤ n
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case mp
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y od : β
hval : ⟨a, od⟩ ∈ A.dedupKeys
hod : (decide ¬od = 0) = true
this : od ∈ List.dlookup a A.dedupKeys
⊢ ¬(some od).getD 0 = 0

Tactic:
simpa using

Goal state after:
case mp
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y od : β
hval : ⟨a, od⟩ ∈ A.dedupKeys
hod : (decide ¬od = 0) = true
this : od ∈ List.dlookup a A.dedupKeys
⊢ ¬od = 0
Module: Mathlib.Topology.Algebra.Group.OpenMapping

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
U : Set G
hU : U ∈ 𝓝 1
x : X
V : Set G
V_mem : V ∈ 𝓝 1
V_closed : IsClosed[inst✝⁹] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : ⋃ g ∈ s, g • V = univ
K : ℕ → Set G := compactCovering G
F : ℕ × ↑s → Set X := fun p ↦ (K p.1 ∩ ↑p.2 • V) • {x}
this✝ : Nonempty X
this : Encodable ↑s
n : ℕ
g : G
hg : g ∈ s
H : IsCompact ((fun g ↦ g • x) '' (K n ∩ g • V))
⊢ IsCompact (F (n, ⟨g, hg⟩))

Tactic:
simpa using

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
U : Set G
hU : U ∈ 𝓝 1
x : X
V : Set G
V_mem : V ∈ 𝓝 1
V_closed : IsClosed[inst✝⁹] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : ⋃ g ∈ s, g • V = univ
K : ℕ → Set G := compactCovering G
F : ℕ × ↑s → Set X := fun p ↦ (K p.1 ∩ ↑p.2 • V) • {x}
this✝ : Nonempty X
this : Encodable ↑s
n : ℕ
g : G
hg : g ∈ s
H : IsCompact ((fun g ↦ g • x) '' (K n ∩ g • V))
⊢ IsCompact ((fun x_1 ↦ x_1 • x) '' (K n ∩ g • V))
Module: Mathlib.Topology.Algebra.Group.OpenMapping

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
U : Set G
hU : U ∈ 𝓝 1
x : X
V : Set G
V_mem : V ∈ 𝓝 1
V_closed : IsClosed[inst✝⁹] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : ⋃ g ∈ s, g • V = univ
K : ℕ → Set G := compactCovering G
F : ℕ × ↑s → Set X := fun p ↦ (K p.1 ∩ ↑p.2 • V) • {x}
n : ℕ
g : G
hg : g ∈ s
hi : (interior (F (n, ⟨g, hg⟩))).Nonempty
I : (interior ((g • V) • {x})).Nonempty
y : X
hy : y ∈ interior (V • {x})
⊢ ∃ g' ∈ V, g' • x = y

Tactic:
simpa using

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
U : Set G
hU : U ∈ 𝓝 1
x : X
V : Set G
V_mem : V ∈ 𝓝 1
V_closed : IsClosed[inst✝⁹] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : ⋃ g ∈ s, g • V = univ
K : ℕ → Set G := compactCovering G
F : ℕ × ↑s → Set X := fun p ↦ (K p.1 ∩ ↑p.2 • V) • {x}
n : ℕ
g : G
hg : g ∈ s
hi : (interior (F (n, ⟨g, hg⟩))).Nonempty
I : (interior ((g • V) • {x})).Nonempty
y : X
hy : y ∈ interior (V • {x})
⊢ ∃ g' ∈ V, g' • x = y
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_ind : IsInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F)
F_cl : IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
F_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q
this : IsInducing ((⋃₀ 𝔖).domRestrict ∘ F)
⊢ CompactSpace ι

Tactic:
rw [← isCompact_univ_iff, this.isCompact_iff, image_univ]

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_ind : IsInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F)
F_cl : IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
F_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q
this : IsInducing ((⋃₀ 𝔖).domRestrict ∘ F)
⊢ IsCompact (range ((⋃₀ 𝔖).domRestrict ∘ F))
Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
⊢ MapClusterPt 1 atTop fun x_1 ↦ x ^ x_1

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
⊢ MapClusterPt 1 atTop fun x_1 ↦ x ^ x_1
Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
⊢ MapClusterPt x atTop fun x_1 ↦ x ^ x_1

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
⊢ MapClusterPt x atTop fun x_1 ↦ x ^ x_1
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x ↦ ⇑↑x
⊢ IsCompact S

Tactic:
suffices h : IsInducing (Equiv.Set.image _ S DFunLike.coe_injective) by
    rw [isCompact_iff_compactSpace] at hS1 ⊢
    exact (Equiv.toHomeomorphOfIsInducing _ h).symm.compactSpace

Goal state after:
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x ↦ ⇑↑x
⊢ IsInducing ⇑(Equiv.Set.image DFunLike.coe S ⋯)
Module: Mathlib.Topology.Algebra.Group.OpenMapping

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
x : X
g : G
U : Set G
hU : U ∈ 𝓝 g
this : (fun x_1 ↦ x_1 • x) = (fun x_1 ↦ x_1 • g • x) ∘ fun x ↦ x * g⁻¹
⊢ (fun x ↦ x * g⁻¹) '' U ∈ 𝓝 1

Tactic:
simpa using

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
x : X
g : G
U : Set G
hU : U ∈ 𝓝 g
this : (fun x_1 ↦ x_1 • x) = (fun x_1 ↦ x_1 • g • x) ∘ fun x ↦ x * g⁻¹
⊢ (fun x ↦ x * g) ⁻¹' U ∈ 𝓝 1
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_6
inst✝¹⁰ : Monoid M
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid E'
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module S E
inst✝⁴ : Module S E'
inst✝³ : Module S F
inst✝² : TopologicalSpace F
inst✝¹ : T2Space F
inst✝ : ContinuousAdd F
f : M → E
g g' : M → E'
x : M
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExistsAt L f g x
hfg' : ConvolutionExistsAt L f g' x
⊢ (f ⋆[L] (g + g')) x = (f ⋆[L] g) x + (f ⋆[L] g') x

Tactic:
simpa using

Goal state after:
M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_6
inst✝¹⁰ : Monoid M
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid E'
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module S E
inst✝⁴ : Module S E'
inst✝³ : Module S F
inst✝² : TopologicalSpace F
inst✝¹ : T2Space F
inst✝ : ContinuousAdd F
f : M → E
g g' : M → E'
x : M
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExistsAt L f g x
hfg' : ConvolutionExistsAt L f g' x
⊢ ∑' (ab : ↑(mulFiber x)), ((L (f (↑ab).1)) (g (↑ab).2) + (L (f (↑ab).1)) (g' (↑ab).2)) =
    ∑' (ab : ↑(mulFiber x)), (L (f (↑ab).1)) (g (↑ab).2) + ∑' (ab : ↑(mulFiber x)), (L (f (↑ab).1)) (g' (↑ab).2)
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_6
inst✝¹⁰ : Monoid M
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid E'
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module S E
inst✝⁴ : Module S E'
inst✝³ : Module S F
inst✝² : TopologicalSpace F
inst✝¹ : T2Space F
inst✝ : ContinuousAdd F
f f' : M → E
g : M → E'
x : M
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExistsAt L f g x
hfg' : ConvolutionExistsAt L f' g x
⊢ ((f + f') ⋆[L] g) x = (f ⋆[L] g) x + (f' ⋆[L] g) x

Tactic:
simpa using

Goal state after:
M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_6
inst✝¹⁰ : Monoid M
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid E'
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module S E
inst✝⁴ : Module S E'
inst✝³ : Module S F
inst✝² : TopologicalSpace F
inst✝¹ : T2Space F
inst✝ : ContinuousAdd F
f f' : M → E
g : M → E'
x : M
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExistsAt L f g x
hfg' : ConvolutionExistsAt L f' g x
⊢ ∑' (ab : ↑(mulFiber x)), ((L (f (↑ab).1)) (g (↑ab).2) + (L (f' (↑ab).1)) (g (↑ab).2)) =
    ∑' (ab : ↑(mulFiber x)), (L (f (↑ab).1)) (g (↑ab).2) + ∑' (ab : ↑(mulFiber x)), (L (f' (↑ab).1)) (g (↑ab).2)
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
inst✝¹⁰ : Monoid M
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid E'
inst✝⁶ : Module S E
inst✝⁵ : Module S E'
F : Type u_10
inst✝⁴ : AddCommMonoid F
inst✝³ : Module S F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousConstSMul S F
inst✝ : T2Space F
c : S
f : M → E
g : M → E'
x : M
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExistsAt L f g x
⊢ (c • f ⋆[L] g) x = c • (f ⋆[L] g) x

Tactic:
simpa using

Goal state after:
M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
inst✝¹⁰ : Monoid M
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid E'
inst✝⁶ : Module S E
inst✝⁵ : Module S E'
F : Type u_10
inst✝⁴ : AddCommMonoid F
inst✝³ : Module S F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousConstSMul S F
inst✝ : T2Space F
c : S
f : M → E
g : M → E'
x : M
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExistsAt L f g x
⊢ ∑' (ab : ↑(mulFiber x)), c • (L (f (↑ab).1)) (g (↑ab).2) = c • ∑' (ab : ↑(mulFiber x)), (L (f (↑ab).1)) (g (↑ab).2)
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
inst✝¹⁰ : Monoid M
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid E'
inst✝⁶ : Module S E
inst✝⁵ : Module S E'
F : Type u_10
inst✝⁴ : AddCommMonoid F
inst✝³ : Module S F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousConstSMul S F
inst✝ : T2Space F
c : S
f : M → E
g : M → E'
x : M
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExistsAt L f g x
⊢ (f ⋆[L] c • g) x = c • (f ⋆[L] g) x

Tactic:
simpa using

Goal state after:
M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
inst✝¹⁰ : Monoid M
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid E'
inst✝⁶ : Module S E
inst✝⁵ : Module S E'
F : Type u_10
inst✝⁴ : AddCommMonoid F
inst✝³ : Module S F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousConstSMul S F
inst✝ : T2Space F
c : S
f : M → E
g : M → E'
x : M
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExistsAt L f g x
⊢ ∑' (ab : ↑(mulFiber x)), c • (L (f (↑ab).1)) (g (↑ab).2) = c • ∑' (ab : ↑(mulFiber x)), (L (f (↑ab).1)) (g (↑ab).2)
Module: Mathlib.Topology.Algebra.IsOpenUnits

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
s : Set R
hs : s ∈ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))
H : (𝓝 1).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ 1 + y) '' ↑(I ^ n)
this :
  (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ True) fun i ↦
    ((fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.1)) ×ˢ (⇑MulOpposite.opHomeomorph.symm ⁻¹' (fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.2))
⊢ ∃ n₁ n₂, ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n₁ → -1 + ↑u⁻¹ ∈ I ^ n₂ → ↑u ∈ s

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
s : Set R
hs : s ∈ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))
H : (𝓝 1).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ 1 + y) '' ↑(I ^ n)
this :
  (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ True) fun i ↦
    ((fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.1)) ×ˢ (⇑MulOpposite.opHomeomorph.symm ⁻¹' (fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.2))
⊢ ∃ n₁ n₂, ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n₁ → -1 + ↑u⁻¹ ∈ I ^ n₂ → ↑u ∈ s
Module: Mathlib.Topology.Algebra.IsOpenUnits

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
s : Set R
hs : s ∈ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))
H : (𝓝 1).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ 1 + y) '' ↑(I ^ n)
this✝¹ :
  (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ True) fun i ↦
    ((fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.1)) ×ˢ (⇑MulOpposite.opHomeomorph.symm ⁻¹' (fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.2))
this✝ : ∃ n₁ n₂, ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n₁ → -1 + ↑u⁻¹ ∈ I ^ n₂ → ↑u ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n → -1 + ↑u⁻¹ ∈ I ^ n → ↑u ∈ s
x : R
hx : x ∈ ↑(I ^ n)
this : IsUnit (1 + x)
⊢ -1 + ↑this.unit ∈ I ^ n

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
s : Set R
hs : s ∈ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))
H : (𝓝 1).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ 1 + y) '' ↑(I ^ n)
this✝¹ :
  (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ True) fun i ↦
    ((fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.1)) ×ˢ (⇑MulOpposite.opHomeomorph.symm ⁻¹' (fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.2))
this✝ : ∃ n₁ n₂, ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n₁ → -1 + ↑u⁻¹ ∈ I ^ n₂ → ↑u ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n → -1 + ↑u⁻¹ ∈ I ^ n → ↑u ∈ s
x : R
hx : x ∈ ↑(I ^ n)
this : IsUnit (1 + x)
⊢ x ∈ I ^ n
Module: Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected

Goal state before:
pp: case h
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : NonarchimedeanGroup G
inst✝ : T2Space G
a b : G
h : a ≠ b
u v : Set G
left✝ : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
V : OpenSubgroup G
hV : ↑V ⊆ v
x : Set G
mem_aV : x ⊆ a • ↑V
mem_bV : x ⊆ b • ↑V
s : G
hs : s ∈ x
hsa : a⁻¹ * s ∈ ↑V
hsb : b⁻¹ * s ∈ ↑V
⊢ a⁻¹ * b ∈ ↑V

Tactic:
simpa using

Goal state after:
case h
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : NonarchimedeanGroup G
inst✝ : T2Space G
a b : G
h : a ≠ b
u v : Set G
left✝ : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
V : OpenSubgroup G
hV : ↑V ⊆ v
x : Set G
mem_aV : x ⊆ a • ↑V
mem_bV : x ⊆ b • ↑V
s : G
hs : s ∈ x
hsa : a⁻¹ * s ∈ ↑V
hsb : b⁻¹ * s ∈ ↑V
⊢ a⁻¹ * b ∈ V
Module: Mathlib.Topology.Algebra.PontryaginDual

Goal state before:
pp: case refine_2
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : LocallyCompactSpace H
Vn : ℕ → Set Circle := fun n ↦ Circle.centeredArc (π / 2 ^ (n + 1))
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x).arg| < π / 2 ^ (n + 1)
⊢ (nhds 1).HasBasis (fun x ↦ True) Vn

Tactic:
simpa using

Goal state after:
case refine_2
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : LocallyCompactSpace H
Vn : ℕ → Set Circle := fun n ↦ Circle.centeredArc (π / 2 ^ (n + 1))
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x).arg| < π / 2 ^ (n + 1)
⊢ (nhds 1).HasBasis (fun x ↦ True) fun n ↦ Circle.centeredArc (π / 2 ^ (n + 1))
Module: Mathlib.Topology.Algebra.PontryaginDual

Goal state before:
pp: case refine_1
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : CompactSpace A
V : Set (PontryaginDual A) := {ψ | Set.MapsTo (⇑ψ) Set.univ (Circle.centeredArc (π / 2))}
hVopen : IsOpen V
ψ : PontryaginDual A
hψ : ψ ∈ V
a : A
n : ℕ
hn : n > 0
⊢ ψ a ^ n ∈ Circle.centeredArc (π / 2)

Tactic:
simpa using

Goal state after:
case refine_1
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : CompactSpace A
V : Set (PontryaginDual A) := {ψ | Set.MapsTo (⇑ψ) Set.univ (Circle.centeredArc (π / 2))}
hVopen : IsOpen V
ψ : PontryaginDual A
hψ : ψ ∈ V
a : A
n : ℕ
hn : n > 0
⊢ ψ a ^ n ∈ Circle.centeredArc (π / 2)