mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case a
x y : PSet.{u_1}
⊢ (insert x y).rank ≤ max (succ x.rank) y.rank

pp: case a
x y : PSet.{u_1}
⊢ max (succ x.rank) y.rank ≤ (insert x y).rank

Tactic:
· simp_rw [rank_le_iff, mem_insert_iff]
    rintro _ (h | h)
    · simp [rank_congr h]
    · simp [rank_lt_of_mem h]

Goal state after:
case a
x y : PSet.{u_1}
⊢ max (succ x.rank) y.rank ≤ (insert x y).rank
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: H : ∀ (x : ZFSet.{u}), Acc (fun x1 x2 ↦ x1 ∈ x2) ↑x
⊢ ∀ (a : Class.{u}), Acc (fun x1 x2 ↦ x1 ∈ x2) a

Tactic:
refine fun A => ⟨A, ?_⟩

Goal state after:
H : ∀ (x : ZFSet.{u}), Acc (fun x1 x2 ↦ x1 ∈ x2) ↑x
A : Class.{u}
⊢ ∀ y ∈ A, Acc (fun x1 x2 ↦ x1 ∈ x2) y
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: s : Set ZFSet.{u}
hs : Small.{u, u + 1} ↑s
⊢ ↑(mk (PSet.mk (Shrink.{u, u + 1} ↑s) fun x ↦ Quotient.out ↑((equivShrink ↑s).symm x))) = s

Tactic:
ext x

Goal state after:
s : Set ZFSet.{u}
hs : Small.{u, u + 1} ↑s
x : ZFSet.{u}
⊢ x ∈ ↑(mk (PSet.mk (Shrink.{u, u + 1} ↑s) fun x ↦ Quotient.out ↑((equivShrink ↑s).symm x))) ↔ x ∈ s
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: a b : Ordinal.{u_1}
h : a < b
⊢ ∃ a_1 < b, a_1.toZFSet = a.toZFSet

Tactic:
exact ⟨a, h, rfl⟩

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
Rl : R < ω ^ (a0.repr * succ ↑k)
αd : ω ∣ α'
⊢ ¬α' = ⊥

Tactic:
exact α0.ne'

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case nil.nil
α : Type u_1
h : nil.head = nil.head
⊢ dist nil nil = 2⁻¹ * dist nil.tail nil.tail

Tactic:
simp at h

Goal state after:
case nil.nil
α : Type u_1
h : True
⊢ dist nil nil = 2⁻¹ * dist nil.tail nil.tail
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case nil.cons
α : Type u_1
x✝ : α
s✝ : Stream'.Seq α
h : nil.head = (Seq.cons x✝ s✝).head
⊢ dist nil (Seq.cons x✝ s✝) = 2⁻¹ * dist nil.tail (Seq.cons x✝ s✝).tail

Tactic:
simp at h

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case cons.nil
α : Type u_1
x✝ : α
s✝ : Stream'.Seq α
h : (Seq.cons x✝ s✝).head = nil.head
⊢ dist (Seq.cons x✝ s✝) nil = 2⁻¹ * dist (Seq.cons x✝ s✝).tail nil.tail

Tactic:
simp at h

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case cons.cons
α : Type u_1
x✝¹ : α
s✝¹ : Stream'.Seq α
x✝ : α
s✝ : Stream'.Seq α
h : (Seq.cons x✝¹ s✝¹).head = (Seq.cons x✝ s✝).head
⊢ dist (Seq.cons x✝¹ s✝¹) (Seq.cons x✝ s✝) = 2⁻¹ * dist (Seq.cons x✝¹ s✝¹).tail (Seq.cons x✝ s✝).tail

Tactic:
simp at h

Goal state after:
case cons.cons
α : Type u_1
x✝¹ : α
s✝¹ : Stream'.Seq α
x✝ : α
s✝ : Stream'.Seq α
h : x✝¹ = x✝
⊢ dist (Seq.cons x✝¹ s✝¹) (Seq.cons x✝ s✝) = 2⁻¹ * dist (Seq.cons x✝¹ s✝¹).tail (Seq.cons x✝ s✝).tail
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α :=
  fun f b ↦
    match F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
f g : β →ᵤ Stream'.Seq α
b : β
a : α
c : γ
b' : β
⊢ dist (op c (f b')) (op c (g b')) ≤ dist f g

Tactic:
calc
        _ ≤ dist (f b') (g b') := by
          have := h.friend c
          rw [FriendlyOperation, lipschitzWith_iff_dist_le_mul] at this
          specialize this (f b') (g b')
          simpa using this
        _ ≤ _ := by
          simp only [UniformFun.dist_def]
          apply le_ciSup (f := fun b ↦ dist (f b) (g b))
          have : ∃ C, ∀ (a b : Seq α), dist a b ≤ C := by
            rw [← Metric.boundedSpace_iff]
            infer_instance
          obtain ⟨C, hC⟩ := this
          use C
          simp [upperBounds]
          grind

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: basis : Basis
⊢ toFun [] basis = 1

Tactic:
ext x

Goal state after:
basis : Basis
x : ℝ
⊢ toFun [] basis x = 1 x
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: m : UnitMonomial
⊢ m.toFun [] = 1

Tactic:
ext x

Goal state after:
m : UnitMonomial
x : ℝ
⊢ m.toFun [] x = 1 x
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: exp : ℝ
tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ toFun (exp :: tl) (basis_hd :: basis_tl) = basis_hd ^ exp * tl.toFun basis_tl

Tactic:
ext x

Goal state after:
exp : ℝ
tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
x : ℝ
⊢ toFun (exp :: tl) (basis_hd :: basis_tl) x = (basis_hd ^ exp * tl.toFun basis_tl) x
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: basis : Basis
⊢ toLogFun [] basis = 0

Tactic:
ext x

Goal state after:
basis : Basis
x : ℝ
⊢ toLogFun [] basis x = 0 x
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: m : UnitMonomial
⊢ m.toLogFun [] = 0

Tactic:
ext x

Goal state after:
m : UnitMonomial
x : ℝ
⊢ m.toLogFun [] x = 0 x
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: exp : ℝ
tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ toLogFun (exp :: tl) (basis_hd :: basis_tl) = exp • log ∘ basis_hd + tl.toLogFun basis_tl

Tactic:
ext x

Goal state after:
exp : ℝ
tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
x : ℝ
⊢ toLogFun (exp :: tl) (basis_hd :: basis_tl) x = (exp • log ∘ basis_hd + tl.toLogFun basis_tl) x
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.cons
x e : ℝ
es : List ℝ
ih :
  ∀ {basis : Basis},
    WellFormedBasis basis →
      (∀ f ∈ basis, 0 < f x) → 0 < toFun es basis x ∧ (log ∘ toFun es basis) x = toLogFun es basis x
b : ℝ → ℝ
bs : List (ℝ → ℝ)
h_basis : WellFormedBasis (b :: bs)
hx : ∀ f ∈ b :: bs, 0 < f x
⊢ 0 < toFun (e :: es) (b :: bs) x ∧ (log ∘ toFun (e :: es) (b :: bs)) x = toLogFun (e :: es) (b :: bs) x

Tactic:
simp only [toFun_cons, Pi.mul_apply, Pi.pow_apply, Function.comp_apply, toLogFun_cons,
        Pi.add_apply, Pi.smul_apply, smul_eq_mul]
      obtain ⟨hpos, heq⟩ := ih h_basis.tail (hx · <| by simp [·])
      refine ⟨mul_pos (Real.rpow_pos_of_pos (hx b (by simp)) _) hpos, ?_⟩
      rw [Real.log_mul (Real.rpow_pos_of_pos (hx b (by simp)) _).ne' hpos.ne',
            Real.log_rpow (hx b (by simp)), ← heq]
      rfl

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: a : ONote
m : ℕ+
b : ONote
iha : a = 0
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
e' : m.natPred = 0
⊢ m = 1

Tactic:
have := PNat.natPred_add_one m

Goal state after:
a : ONote
m : ℕ+
b : ONote
iha : a = 0
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
e' : m.natPred = 0
this : m.natPred + 1 = ↑m
⊢ m = 1
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: a : ONote
m : ℕ+
b : ONote
iha : a = 0
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
m' : ℕ
e' : m.natPred = m' + 1
⊢ m = 1

Tactic:
have := PNat.natPred_add_one m

Goal state after:
a : ONote
m : ℕ+
b : ONote
iha : a = 0
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
m' : ℕ
e' : m.natPred = m' + 1
this : m.natPred + 1 = ↑m
⊢ m = 1
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: 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')
e' : m.natPred = 0
⊢ m = 1

Tactic:
have := PNat.natPred_add_one m

Goal state after:
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')
e' : m.natPred = 0
this : m.natPred + 1 = ↑m
⊢ m = 1
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: exps_hd : ℝ
exps_tl : List ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_length : (exps_hd :: exps_tl).length = (basis_hd :: basis_tl).length
h : exps_hd = 0 ∧ FirstNonzeroIsPos exps_tl
⊢ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) = toFun exps_tl basis_tl

Tactic:
ext x

Goal state after:
exps_hd : ℝ
exps_tl : List ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_length : (exps_hd :: exps_tl).length = (basis_hd :: basis_tl).length
h : exps_hd = 0 ∧ FirstNonzeroIsPos exps_tl
x : ℝ
⊢ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) x = toFun exps_tl basis_tl x
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: 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
⊢ m = 1

Tactic:
have := PNat.natPred_add_one m

Goal state after:
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 : m.natPred + 1 = ↑m
⊢ m = 1
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: exps_hd : ℝ
exps_tl : List ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_length : (exps_hd :: exps_tl).length = (basis_hd :: basis_tl).length
h : exps_hd = 0 ∧ FirstNonzeroIsNeg exps_tl
⊢ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) = toFun exps_tl basis_tl

Tactic:
ext x

Goal state after:
exps_hd : ℝ
exps_tl : List ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_length : (exps_hd :: exps_tl).length = (basis_hd :: basis_tl).length
h : exps_hd = 0 ∧ FirstNonzeroIsNeg exps_tl
x : ℝ
⊢ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) x = toFun exps_tl basis_tl x
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: exps_hd : ℝ
exps_tl : List ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_allZero : exps_hd = 0 ∧ AllZero exps_tl
⊢ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) = toFun exps_tl basis_tl

Tactic:
ext x

Goal state after:
exps_hd : ℝ
exps_tl : List ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_allZero : exps_hd = 0 ∧ AllZero exps_tl
x : ℝ
⊢ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) x = toFun exps_tl basis_tl x
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
e' : m.natPred = 0
⊢ m = 1

Tactic:
have := PNat.natPred_add_one m

Goal state after:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
e' : m.natPred = 0
this : m.natPred + 1 = ↑m
⊢ m = 1
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
⊢ m = 1

Tactic:
have := PNat.natPred_add_one m

Goal state after:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
this : m.natPred + 1 = ↑m
⊢ m = 1
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: coef : ℝ
basis : Basis
⊢ { coef := coef, unit := [] }.toFun basis = fun x ↦ coef

Tactic:
ext x

Goal state after:
coef : ℝ
basis : Basis
x : ℝ
⊢ { coef := coef, unit := [] }.toFun basis x = coef
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: coef exp : ℝ
m : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ { coef := coef, unit := exp :: m }.toFun (basis_hd :: basis_tl) =
    basis_hd ^ exp * { coef := coef, unit := m }.toFun basis_tl

Tactic:
ext x

Goal state after:
coef exp : ℝ
m : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
x : ℝ
⊢ { coef := coef, unit := exp :: m }.toFun (basis_hd :: basis_tl) x =
    (basis_hd ^ exp * { coef := coef, unit := m }.toFun basis_tl) x
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: t : Monomial
basis : Basis
⊢ t.toFun basis = -t.neg.toFun basis

Tactic:
ext x

Goal state after:
t : Monomial
basis : Basis
x : ℝ
⊢ t.toFun basis x = (-t.neg.toFun basis) x
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: t : Monomial
basis : Basis
c : ℝ
⊢ (t.smul c).toFun basis = c • t.toFun basis

Tactic:
ext x

Goal state after:
t : Monomial
basis : Basis
c x : ℝ
⊢ (t.smul c).toFun basis x = (c • t.toFun basis) x
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f : ℝ → ℝ
h : (mk (Multiseries.cons exp coef tl) f).Trimmed
⊢ coef.Trimmed ∧ ¬coef.IsZero

Tactic:
simp only [trimmed_iff_seq_trimmed, mk_seq] at h
  exact h.elim_cons

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case eq
a : ONote
ha : a.NF
b : ONote
hb : b.NF
h : a.cmp b = Ordering.eq
this : Ordering.eq.Compares a b
⊢ Ordering.eq.Compares ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
exact Subtype.mk_eq_mk.2 this

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

Goal state before:
pp: a b x y : ℕ
hab : a.Coprime b
hxy : x.Coprime y
h : a * x = b * y
⊢ y * b = x * a

Tactic:
by rw [mul_comm, ← h, mul_comm]

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

Goal state before:
pp: a b : ℕ
r : ℤ
ha : a % 4 = 3
hb : b % 4 = 3
hr : jacobiSymNat b a = r
⊢ jacobiSym (↑a) b = -r

Tactic:
jacobiSym.quadratic_reciprocity_three_mod_four ha hb,

Goal state after:
a b : ℕ
r : ℤ
ha : a % 4 = 3
hb : b % 4 = 3
hr : jacobiSymNat b a = r
⊢ -jacobiSym (↑b) a = -r
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case some
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x val : α
h₃ : dlookup x (map Prod.toSigma (xs.zip ys)) = some val
⊢ (some val).getD x ∈ ys ↔ x ∈ xs

Tactic:
have h₂ : ys.Nodup := h₁.nodup_iff.1 h₀

Goal state after:
case some
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x val : α
h₃ : dlookup x (map Prod.toSigma (xs.zip ys)) = some val
h₂ : ys.Nodup
⊢ (some val).getD x ∈ ys ↔ x ∈ xs
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✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ { toTopologicalSpace := TopologicalSpace.induced F (Pi.uniformSpace fun i ↦ α).toTopologicalSpace,
      uniformity := comap (fun p ↦ (F p.1, F p.2)) (𝓤 (X → α)), symm := ⋯, comp := ⋯, nhds_eq_comap_uniformity := ⋯ } ≤
    { toTopologicalSpace := TopologicalSpace.induced F (UniformFun.uniformSpace X α).toTopologicalSpace,
      uniformity := comap (fun p ↦ (F p.1, F p.2)) (𝓤 (X → α)), symm := ⋯, comp := ⋯, nhds_eq_comap_uniformity := ⋯ }

Tactic:
UniformSpace.le_def,

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ 𝓤 ι ≤ 𝓤 ι
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
⊢ (interior (V • {x})).Nonempty

Tactic:
rw [smul_assoc, interior_smul] at I
    exact smul_set_nonempty.1 I

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
P : ProfiniteGrp.{u}
f g : completion G ⟶ P
h : eta G ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map f = eta G ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map g
⊢ f = g

Tactic:
ext x

Goal state after:
G : GrpCat
P : ProfiniteGrp.{u}
f g : completion G ⟶ P
h : eta G ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map f = eta G ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map g
x : ↑(completion G).toProfinite.toTop
⊢ (Hom.hom f) x = (Hom.hom g) x
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst✝⁶ : Monoid M
inst✝⁵ : CommSemiring S
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid F
inst✝² : Module S E
inst✝¹ : Module S F
inst✝ : TopologicalSpace F
L : E →ₗ[S] F →ₗ[S] F
e : E
f : M → F
hL : ∀ (y : F), (L e) y = y
⊢ ({1}.indicator fun x ↦ e) ⋆[L] f = f

Tactic:
ext x

Goal state after:
M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst✝⁶ : Monoid M
inst✝⁵ : CommSemiring S
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid F
inst✝² : Module S E
inst✝¹ : Module S F
inst✝ : TopologicalSpace F
L : E →ₗ[S] F →ₗ[S] F
e : E
f : M → F
hL : ∀ (y : F), (L e) y = y
x : M
⊢ (({1}.indicator fun x ↦ e) ⋆[L] f) x = f x
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst✝⁶ : Monoid M
inst✝⁵ : CommSemiring S
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid F
inst✝² : Module S E
inst✝¹ : Module S F
inst✝ : TopologicalSpace F
L : F →ₗ[S] E →ₗ[S] F
f : M → F
e : E
hL : ∀ (y : F), (L y) e = y
⊢ (f ⋆[L] {1}.indicator fun x ↦ e) = f

Tactic:
ext x

Goal state after:
M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst✝⁶ : Monoid M
inst✝⁵ : CommSemiring S
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid F
inst✝² : Module S E
inst✝¹ : Module S F
inst✝ : TopologicalSpace F
L : F →ₗ[S] E →ₗ[S] F
f : M → F
e : E
hL : ∀ (y : F), (L y) e = y
x : M
⊢ (f ⋆[L] {1}.indicator fun x ↦ e) x = f x
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'
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExists L f g
hfg' : ConvolutionExists L f g'
⊢ f ⋆[L] (g + g') = f ⋆[L] g + f ⋆[L] g'

Tactic:
ext x

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'
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExists L f g
hfg' : ConvolutionExists L f g'
x : M
⊢ (f ⋆[L] (g + g')) x = (f ⋆[L] g + f ⋆[L] g') x
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'
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExists L f g
hfg' : ConvolutionExists L f' g
⊢ (f + f') ⋆[L] g = f ⋆[L] g + f' ⋆[L] g

Tactic:
ext x

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'
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExists L f g
hfg' : ConvolutionExists L f' g
x : M
⊢ ((f + f') ⋆[L] g) x = (f ⋆[L] g + f' ⋆[L] g) x
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
inst✝⁴ : CommMonoid M
inst✝³ : CommSemiring S
inst✝² : AddCommMonoid E
inst✝¹ : Module S E
inst✝ : TopologicalSpace E
L : E →ₗ[S] E →ₗ[S] E
f g : M → E
hL : ∀ (x y : E), (L x) y = (L y) x
⊢ (fun x ↦ ∑' (ab : ↑(mulFiber x)), (L (f (↑ab).1)) (g (↑ab).2)) = fun x ↦
    ∑' (ab : ↑(mulFiber x)), (L (g (↑ab).1)) (f (↑ab).2)

Tactic:
ext x

Goal state after:
M : Type u_1
S : Type u_2
E : Type u_3
inst✝⁴ : CommMonoid M
inst✝³ : CommSemiring S
inst✝² : AddCommMonoid E
inst✝¹ : Module S E
inst✝ : TopologicalSpace E
L : E →ₗ[S] E →ₗ[S] E
f g : M → E
hL : ∀ (x y : E), (L x) y = (L y) x
x : M
⊢ ∑' (ab : ↑(mulFiber x)), (L (f (↑ab).1)) (g (↑ab).2) = ∑' (ab : ↑(mulFiber x)), (L (g (↑ab).1)) (f (↑ab).2)
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
A B : Set X
⊢ derivedSet (A ∪ B) = derivedSet A ∪ derivedSet B

Tactic:
ext x

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
A B : Set X
x : X
⊢ x ∈ derivedSet (A ∪ B) ↔ x ∈ derivedSet A ∪ derivedSet B
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: case pos.a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
⊢ U ⊆ derivedSet a ∪ derivedSet b

Tactic:
trans derivedSet U

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
⊢ U ⊆ derivedSet U

X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
⊢ derivedSet U ⊆ derivedSet a ∪ derivedSet b
Module: Mathlib.Topology.Convenient.Category

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
X✝ Y✝ : TopCat
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : (TopCat.toContinuousGeneratedByCat X).map a₁✝ = (TopCat.toContinuousGeneratedByCat X).map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
ext x

Goal state after:
ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
X✝ Y✝ : TopCat
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : (TopCat.toContinuousGeneratedByCat X).map a₁✝ = (TopCat.toContinuousGeneratedByCat X).map a₂✝
x : ↑X✝
⊢ (ConcreteCategory.hom a₁✝) x = (ConcreteCategory.hom a₂✝) x