mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case h
basis_hd : ℝ → ℝ
basis_tl : Basis
op✝ : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
motive : (Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl) → Prop
h_base : motive op✝
h_step :
  ∀ (op : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl),
    motive op →
      ∃ T,
        ∀ (s : Multiseries basis_hd basis_tl),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (exp, coef, opf, op') => (exp, coef, ↑op' (↑opf s.tail)))
              (T s.head)
op : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl) → Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h_op : motive op
T :
  Option (ℝ × MultiseriesExpansion basis_tl) →
    Option (ℝ × MultiseriesExpansion basis_tl × Subtype FriendlyOperation × Subtype motive)
hT :
  ∀ (s : Multiseries basis_hd basis_tl),
    destruct (op s) =
      Option.map
        (fun x ↦
          match x with
          | (exp, coef, opf, op') => (exp, coef, ↑op' (↑opf s.tail)))
        (T s.head)
⊢ ∀ (s : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)),
    (op s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
        ((fun hd? ↦
            Option.map
              (fun x ↦
                match x with
                | (exp, coef, opf, op') => ((exp, coef), opf, op'))
              (T hd?))
          s.head)

Tactic:
intro s

Goal state after:
case h
basis_hd : ℝ → ℝ
basis_tl : Basis
op✝ : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
motive : (Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl) → Prop
h_base : motive op✝
h_step :
  ∀ (op : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl),
    motive op →
      ∃ T,
        ∀ (s : Multiseries basis_hd basis_tl),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (exp, coef, opf, op') => (exp, coef, ↑op' (↑opf s.tail)))
              (T s.head)
op : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl) → Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h_op : motive op
T :
  Option (ℝ × MultiseriesExpansion basis_tl) →
    Option (ℝ × MultiseriesExpansion basis_tl × Subtype FriendlyOperation × Subtype motive)
hT :
  ∀ (s : Multiseries basis_hd basis_tl),
    destruct (op s) =
      Option.map
        (fun x ↦
          match x with
          | (exp, coef, opf, op') => (exp, coef, ↑op' (↑opf s.tail)))
        (T s.head)
s : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
⊢ (op s).destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
      ((fun hd? ↦
          Option.map
            (fun x ↦
              match x with
              | (exp, coef, opf, op') => ((exp, coef), opf, op'))
            (T hd?))
        s.head)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case h
α : Type u_1
op✝ : Stream'.Seq α → Stream'.Seq α
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_base : motive op✝
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑opf (↑op' s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop := ⋯
opf op : Stream'.Seq α → Stream'.Seq α
h_opf : FriendlyOperation opf
h_op : motive op
T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive)
hT :
  ∀ (s : Stream'.Seq α),
    (op s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, opf, op') => (hd, ↑opf (↑op' s.tail)))
        (T s.head)
⊢ ∀ (s : Stream'.Seq α),
    ((opf ∘ op) s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, op') => (hd, ↑op' s.tail))
        ((fun hd? ↦
            match T hd? with
            | none =>
              Option.map
                (fun x ↦
                  match x with
                  | (hd, opf') => (hd, ⟨(fun x ↦ ↑opf' nil) ∘ op, ⋯⟩))
                (h_opf.unfold none)
            | some (hd, opf', op') =>
              Option.map
                (fun x ↦
                  match x with
                  | (hd', opf'') => (hd', ⟨(↑opf'' ∘ ↑opf') ∘ ↑op', ⋯⟩))
                (h_opf.unfold (some hd)))
          s.head)

Tactic:
intro s

Goal state after:
case h
α : Type u_1
op✝ : Stream'.Seq α → Stream'.Seq α
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_base : motive op✝
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑opf (↑op' s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop :=
  fun op ↦ ∃ opf op', op = opf ∘ op' ∧ FriendlyOperation opf ∧ motive op'
opf op : Stream'.Seq α → Stream'.Seq α
h_opf : FriendlyOperation opf
h_op : motive op
T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive)
hT :
  ∀ (s : Stream'.Seq α),
    (op s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, opf, op') => (hd, ↑opf (↑op' s.tail)))
        (T s.head)
s : Stream'.Seq α
⊢ ((opf ∘ op) s).destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, op') => (hd, ↑op' s.tail))
      ((fun hd? ↦
          match T hd? with
          | none =>
            Option.map
              (fun x ↦
                match x with
                | (hd, opf') => (hd, ⟨(fun x ↦ ↑opf' nil) ∘ op, ⋯⟩))
              (h_opf.unfold none)
          | some (hd, opf', op') =>
            Option.map
              (fun x ↦
                match x with
                | (hd', opf'') => (hd', ⟨(↑opf'' ∘ ↑opf') ∘ ↑op', ⋯⟩))
              (h_opf.unfold (some hd)))
        s.head)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case h
α : Type u_1
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop := ⋯
opf op : Stream'.Seq α → Stream'.Seq α
h_opf : FriendlyOperation opf
h_op : motive op
T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive)
hT :
  ∀ (s : Stream'.Seq α),
    (op s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
        (T s.head)
⊢ ∀ (s : Stream'.Seq α),
    ((op ∘ opf) s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, op') => (hd, ↑op' s.tail))
        ((fun hd? ↦
            match h_opf.unfold hd? with
            | none =>
              Option.map
                (fun x ↦
                  match x with
                  | (hd, opf', op') => (hd, ⟨↑op' ∘ fun x ↦ ↑opf' nil, ⋯⟩))
                (T none)
            | some (hd, opf') =>
              Option.map
                (fun x ↦
                  match x with
                  | (hd', opf'', op') => (hd', ⟨↑op' ∘ ↑opf'' ∘ ↑opf', ⋯⟩))
                (T (some hd)))
          s.head)

Tactic:
intro s

Goal state after:
case h
α : Type u_1
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop :=
  fun op ↦ ∃ opf op', op = op' ∘ opf ∧ FriendlyOperation opf ∧ motive op'
opf op : Stream'.Seq α → Stream'.Seq α
h_opf : FriendlyOperation opf
h_op : motive op
T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive)
hT :
  ∀ (s : Stream'.Seq α),
    (op s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
        (T s.head)
s : Stream'.Seq α
⊢ ((op ∘ opf) s).destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, op') => (hd, ↑op' s.tail))
      ((fun hd? ↦
          match h_opf.unfold hd? with
          | none =>
            Option.map
              (fun x ↦
                match x with
                | (hd, opf', op') => (hd, ⟨↑op' ∘ fun x ↦ ↑opf' nil, ⋯⟩))
              (T none)
          | some (hd, opf') =>
            Option.map
              (fun x ↦
                match x with
                | (hd', opf'', op') => (hd', ⟨↑op' ∘ ↑opf'' ∘ ↑opf', ⋯⟩))
              (T (some hd)))
        s.head)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case seq.right.cons
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
tl_tl : Multiseries basis_hd basis_tl
h_coef : ∀ x ∈ (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq, x.2.Sorted
h_Pairwise :
  Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq
⊢ (Multiseries.cons tl_exp tl_coef tl_tl).leadingExp < ↑exp ∧ (Multiseries.cons tl_exp tl_coef tl_tl).Sorted

Tactic:
| cons tl_exp tl_coef tl_tl =>

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

Goal state before:
pp: case cons
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f✝ : ℝ → ℝ
h_equiv : ms.toFun =ᶠ[atTop] f✝
h_approx✝ : ms.Approximates
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop :=
  fun ms ↦ ∃ ms' f', ms = ms'.replaceFun f' ∧ ms'.Approximates ∧ ms'.toFun =ᶠ[atTop] f'
f : ℝ → ℝ
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
g : ℝ → ℝ
h_approx : (mk (Multiseries.cons exp coef tl) g).Approximates
h_eq : (mk (Multiseries.cons exp coef tl) g).toFun =ᶠ[atTop] f
h_coef : coef.Approximates
h_maj : Majorized g basis_hd exp
h_tl : (mk tl (g - basis_hd ^ exp * coef.toFun)).Approximates
⊢ ((mk (Multiseries.cons exp coef tl) g).replaceFun f).seq = Multiseries.nil ∧
      ((mk (Multiseries.cons exp coef tl) g).replaceFun f).toFun =ᶠ[atTop] 0 ∨
    ∃ exp_1 coef_1 tl_1,
      ((mk (Multiseries.cons exp coef tl) g).replaceFun f).seq = Multiseries.cons exp_1 coef_1 tl_1 ∧
        coef_1.Approximates ∧
          Majorized ((mk (Multiseries.cons exp coef tl) g).replaceFun f).toFun basis_hd exp_1 ∧
            motive
              (mk tl_1 (((mk (Multiseries.cons exp coef tl) g).replaceFun f).toFun - basis_hd ^ exp_1 * coef_1.toFun))

Tactic:
refine .inr ⟨exp, coef, tl, ?_⟩

Goal state after:
case cons
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f✝ : ℝ → ℝ
h_equiv : ms.toFun =ᶠ[atTop] f✝
h_approx✝ : ms.Approximates
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop :=
  fun ms ↦ ∃ ms' f', ms = ms'.replaceFun f' ∧ ms'.Approximates ∧ ms'.toFun =ᶠ[atTop] f'
f : ℝ → ℝ
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
g : ℝ → ℝ
h_approx : (mk (Multiseries.cons exp coef tl) g).Approximates
h_eq : (mk (Multiseries.cons exp coef tl) g).toFun =ᶠ[atTop] f
h_coef : coef.Approximates
h_maj : Majorized g basis_hd exp
h_tl : (mk tl (g - basis_hd ^ exp * coef.toFun)).Approximates
⊢ ((mk (Multiseries.cons exp coef tl) g).replaceFun f).seq = Multiseries.cons exp coef tl ∧
    coef.Approximates ∧
      Majorized ((mk (Multiseries.cons exp coef tl) g).replaceFun f).toFun basis_hd exp ∧
        motive (mk tl (((mk (Multiseries.cons exp coef tl) g).replaceFun f).toFun - basis_hd ^ exp * coef.toFun))
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case cons
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f✝ : ℝ → ℝ
h_equiv : ms.toFun =ᶠ[atTop] f✝
h_approx✝ : ms.Approximates
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop :=
  fun ms ↦ ∃ ms' f', ms = ms'.replaceFun f' ∧ ms'.Approximates ∧ ms'.toFun =ᶠ[atTop] f'
f : ℝ → ℝ
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
g : ℝ → ℝ
h_approx : (mk (Multiseries.cons exp coef tl) g).Approximates
h_eq : (mk (Multiseries.cons exp coef tl) g).toFun =ᶠ[atTop] f
h_coef : coef.Approximates
h_maj : Majorized g basis_hd exp
h_tl : (mk tl (g - basis_hd ^ exp * coef.toFun)).Approximates
⊢ Majorized f basis_hd exp ∧ motive (mk tl (f - basis_hd ^ exp * coef.toFun))

Tactic:
simp only [mk_toFun] at h_eq

Goal state after:
case cons
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f✝ : ℝ → ℝ
h_equiv : ms.toFun =ᶠ[atTop] f✝
h_approx✝ : ms.Approximates
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop :=
  fun ms ↦ ∃ ms' f', ms = ms'.replaceFun f' ∧ ms'.Approximates ∧ ms'.toFun =ᶠ[atTop] f'
f : ℝ → ℝ
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
g : ℝ → ℝ
h_approx : (mk (Multiseries.cons exp coef tl) g).Approximates
h_eq : g =ᶠ[atTop] f
h_coef : coef.Approximates
h_maj : Majorized g basis_hd exp
h_tl : (mk tl (g - basis_hd ^ exp * coef.toFun)).Approximates
⊢ Majorized f basis_hd exp ∧ motive (mk tl (f - basis_hd ^ exp * coef.toFun))
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
hf0 : f 0 = 0
⊢ ∃ m, n = m ^ q

Tactic:
refine ⟨f.prod (· ^ ·), Nat.factorization_inj hn (by simp [hf0]) ?_⟩

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
hf0 : f 0 = 0
⊢ n.factorization = ((f.prod fun x1 x2 ↦ x1 ^ x2) ^ q).factorization
Module: Mathlib.Tactic.ReduceModChar

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n : ℕ
inst : CharP α n
b : α
a : ℕ
a' : α
p : IsNat (↑n - 1) a
pa : ↑a = a'
⊢ -b = a' * b

Tactic:
rw [← pa, ← p.out, ← neg_one_mul]

Goal state after:
α : Type u_1
inst✝ : Ring α
n : ℕ
inst : CharP α n
b : α
a : ℕ
a' : α
p : IsNat (↑n - 1) a
pa : ↑a = a'
⊢ -1 * b = (↑n - 1) * b
Module: Mathlib.Tactic.ReduceModChar

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n : ℕ
inst : CharP α n
a b : α
na : ℕ
na' : α
p : IsNat ((↑n - 1) * a) na
pa : ↑na = na'
⊢ -(a * b) = na' * b

Tactic:
rw [← pa, ← p.out, ← neg_one_mul]

Goal state after:
α : Type u_1
inst✝ : Ring α
n : ℕ
inst : CharP α n
a b : α
na : ℕ
na' : α
p : IsNat ((↑n - 1) * a) na
pa : ↑na = na'
⊢ -1 * (a * b) = (↑n - 1) * a * b
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Ioc 1 1 = ∅

Tactic:
by simp only [Ioc_ofNat_ofNat]

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Ioc 1 2 = {2}

Tactic:
by simp only [Ioc_ofNat_ofNat]

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Ioc 1 3 = {2, 3}

Tactic:
by simp only [Ioc_ofNat_ofNat]

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : 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
⊢ List.dlookup a A = some od

Tactic:
· simpa [List.dlookup_dedupKeys]

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case nil
α : Type u
inst✝ : DecidableEq α
⊢ [] =
    map
      (fun x ↦
        match x with
        | (a, b) => ⟨a, b⟩)
      ((map Sigma.fst []).zip (map Sigma.snd []))

Tactic:
simp only [List.zip_nil_right, List.map_nil]

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

Goal state before:
pp: G : GrpCat
⊢ ∀ (U : Set ↑(completion G).toProfinite.toTop), IsOpen U → U.Nonempty → (U ∩ Set.range (etaFn G)).Nonempty

Tactic:
rintro U ⟨s, hsO, hsv⟩ ⟨⟨spc, hspc⟩, uDefaultSpec⟩

Goal state after:
G : GrpCat
U : Set ↑(completion G).toProfinite.toTop
s : Set ((j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (diagram G)
uDefaultSpec : ⟨spc, hspc⟩ ∈ U
⊢ (U ∩ Set.range (etaFn G)).Nonempty
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)
⊢ IsCompact ((⋃₀ 𝔖).domRestrict ∘ F '' univ)

Tactic:
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.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
⊢ 𝓝 1 ≤ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))

Tactic:
intro s

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
⊢ s ∈ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1)) → s ∈ 𝓝 1
Module: Mathlib.Topology.Algebra.Module.EmbeddingOfLocal

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
f : E →ₛₗ[σ] F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : RingHomIsometric σ
V : Set E
V_mem : V ∈ 𝓝 0
H : IsInducing (V.domRestrict ⇑f)
this✝ : IsTopologicalAddGroup E
this : ContinuousSMul 𝕜₁ E
⊢ TopologicalSpace.induced Subtype.val inst✝⁶ = instTopologicalSpaceSubtype

Tactic:
← IsInducing.subtypeVal.eq_induced

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
f : E →ₛₗ[σ] F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : RingHomIsometric σ
V : Set E
V_mem : V ∈ 𝓝 0
H : IsInducing (V.domRestrict ⇑f)
this✝ : IsTopologicalAddGroup E
this : ContinuousSMul 𝕜₁ E
⊢ instTopologicalSpaceSubtype = instTopologicalSpaceSubtype
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: case mp
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
⊢ G ∈ basic (A ∩ B) → G ∈ basic A ∩ basic B

Tactic:
intro hG

Goal state after:
case mp
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
hG : G ∈ basic (A ∩ B)
⊢ G ∈ basic A ∩ basic B
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
U : Set Y
hU : IsOpen[tY] U
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y)), IsOpen[inst✝ i] (⇑f ⁻¹' ⇑equiv.symm ⁻¹' ⇑equiv ⁻¹' U)

Tactic:
intro i f

Goal state after:
ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
U : Set Y
hU : IsOpen[tY] U
i : ι
f : C(X i, Y)
⊢ IsOpen[inst✝ i] (⇑f ⁻¹' ⇑equiv.symm ⁻¹' ⇑equiv ⁻¹' U)
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝¹ : TopologicalSpace Z
inst✝ : IsGeneratedBy X Y
g : Y → Z
hg : Continuous[tY, inst✝¹] g
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous[inst✝² i, _] ((⇑WithGeneratedByTopology.equiv.symm ∘ g) ∘ ⇑f)

Tactic:
intro i f

Goal state after:
ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝¹ : TopologicalSpace Z
inst✝ : IsGeneratedBy X Y
g : Y → Z
hg : Continuous[tY, inst✝¹] g
i : ι
f : C(X i, Y)
⊢ Continuous[inst✝² i, _] ((⇑WithGeneratedByTopology.equiv.symm ∘ g) ∘ ⇑f)
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
U : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))
hU :
  ∀ ⦃i : ι⦄ (f : C(X i, WithGeneratedByTopology X Y)),
    IsOpen[inst✝¹ i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y)),
    IsOpen[inst✝¹ i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)

Tactic:
intro i f

Goal state after:
ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
U : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))
hU :
  ∀ ⦃i : ι⦄ (f : C(X i, WithGeneratedByTopology X Y)),
    IsOpen[inst✝¹ i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
i : ι
f : C(X i, Y)
⊢ IsOpen[inst✝¹ i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
Module: Mathlib.Topology.Convenient.ContinuousMapGeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝¹ : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous[inst✝² i, _] (⇑equiv.symm ∘ ⇑f)

Tactic:
intro i f

Goal state after:
ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝¹ : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
i : ι
f : C(X i, Y)
⊢ Continuous[inst✝² i, _] (⇑equiv.symm ∘ ⇑f)
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case hi.inl
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
n : ℕ
hn : ∀ m ≤ n, ∀ (j : cell C m), IsClosed[t] (A ∩ closedCell m j)
j : cell C (n + 1)
h1 : IsClosed[t] (A ∩ openCell n.succ j)
⊢ IsClosed[t] (A ∩ closedCell (n + 1) j)

Tactic:
rw [← cellFrontier_union_openCell_eq_closedCell, inter_union_distrib_left]
      exact (isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell hn j hDA).union h1

Goal state after: