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

Goal state before:
pp: case inl
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
nh : ↑n₁ < ↑n₂ ∧ Ordering.lt = Ordering.gt
⊢ (Ordering.eq.then (Ordering.gt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

Tactic:
cases nh; contradiction

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

Goal state before:
pp: case inr.inr
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
left✝ : ↑n₂ ≤ ↑n₁
nh : ¬↑n₂ < ↑n₁ ∧ Ordering.eq = Ordering.gt
⊢ (Ordering.eq.then (Ordering.gt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

Tactic:
cases nh; contradiction

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

Goal state before:
pp: case eq.inl
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
nh : ↑n₁ < ↑n₂ ∧ Ordering.lt = Ordering.eq
⊢ (Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

Tactic:
cases nh; contradiction

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

Goal state before:
pp: case zero
b : Ordinal.{0}
x✝ : NFBelow 0 b
h₂ : zero.NF
⊢ (0 - zero).NFBelow b

Tactic:
exact NFBelow.zero

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

Goal state before:
pp: case oadd
b : Ordinal.{0}
x✝ : NFBelow 0 b
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
h₂ : (a✝².oadd a✝¹ a✝).NF
⊢ (0 - a✝².oadd a✝¹ a✝).NFBelow b

Tactic:
exact NFBelow.zero

Goal state after:
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x : PSet.{u}
⊢ lift.{u + 1, u} x.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) x

Tactic:
induction x using mem_wf.induction with | _ x ih

Goal state after:
case h
x✝ x : PSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
⊢ lift.{u + 1, u} x.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) x
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h' : (a₁.sub a₂).NFBelow e₁.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
en : ¬n₁ = n₂
⊢ NFBelow 0 b

Tactic:
exact NFBelow.zero

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

Goal state before:
pp: o : Ordinal.{u}
h : ω ^ o ≤ o
⊢ ε_ 0 ≤ o

Tactic:
by
  rw [epsilon_zero_eq_nfp]
  exact nfp_le_fp (fun _ _ ↦ (opow_le_opow_iff_right one_lt_omega0).2) zero_le h

Goal state after:
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: a b : Ordinal.{u}
h : a ≤ b
⊢ a = b → V_ a ⊆ V_ b

Tactic:
simp_all

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

Goal state before:
pp: x y : ZFSet.{u_1}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x.rank = y.rank ↔ x = y

Tactic:
le_antisymm_iff,

Goal state after:
x y : ZFSet.{u_1}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x.rank ≤ y.rank ∧ y.rank ≤ x.rank ↔ x = y
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o e : ONote
n : ℕ+
a : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (e.oadd n a, m)
h₁ : (e.oadd n a).NF
h₂ : o.repr = (e.oadd n a).repr + ↑m
e0 : e.repr ≠ 0
d : ω ∣ a.repr
⊢ a.repr + ↑m < ω ^ e.repr

Tactic:
apply isPrincipal_add_omega0_opow _ h₁.snd'.repr_lt (lt_of_lt_of_le (natCast_lt_omega0 _) _)

Goal state after:
o e : ONote
n : ℕ+
a : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (e.oadd n a, m)
h₁ : (e.oadd n a).NF
h₂ : o.repr = (e.oadd n a).repr + ↑m
e0 : e.repr ≠ 0
d : ω ∣ a.repr
⊢ ω ≤ ω ^ e.repr
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: basis : Basis
f : ℝ → ℝ
h : WellFormedBasis basis
h_comp : ∀ (g : ℝ → ℝ), List.getLast? basis = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
⊢ ∀ g ∈ basis, (Real.log ∘ f) =o[atTop] (Real.log ∘ g)

Tactic:
intro g hg
  rcases basis.eq_nil_or_concat with rfl | ⟨basis_begin, basis_end, rfl⟩
  · simp at hg
  simp only [List.concat_eq_append, List.mem_append, List.mem_cons, List.not_mem_nil, or_false,
    List.getLast?_append, List.getLast?_singleton, Option.some_or, Option.some.injEq,
    forall_eq'] at hg h_comp
  rcases hg with hg | hg
  · simp only [WellFormedBasis, List.concat_eq_append, List.mem_append, List.mem_cons,
      List.not_mem_nil, or_false] at h
    exact h_comp.trans (by grind)
  · grind

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

Goal state before:
pp: α : Type u_1
s t : Stream' α
⊢ dist s t ≤ 1

Tactic:
by_cases h : s = t

Goal state after:
case pos
α : Type u_1
s t : Stream' α
h : s = t
⊢ dist s t ≤ 1

case neg
α : Type u_1
s t : Stream' α
h : ¬s = t
⊢ dist s t ≤ 1
Module: Mathlib.SetTheory.Ordinal.Notation

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

Tactic:
apply add_of_omega0_opow_le Rl

Goal state after:
case succ.refine_2.e_a.succ.ba
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
ω0 : Ordinal.{0} := ⋯
α' : Ordinal.{0} := ⋯
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
n✝ : ℕ
h : a'.repr + ↑(n✝ + 1) < ω ^ a0.repr
R' : Ordinal.{0} := ⋯
R : Ordinal.{0} := ⋯
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑(n✝ + 1)) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑(n✝ + 1)) + R
Rl : R < ω ^ (a0.repr * succ ↑k)
⊢ ω ^ (a0.repr * succ ↑k) ≤ ω0 ^ ↑k * α'
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case h
α : 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'))
hT : LipschitzWith 2⁻¹ T
f : β → Stream'.Seq α
hf : Function.IsFixedPt T f
b : β
⊢ match F b with
  | none => f b = nil
  | some (a, c, b') => f b = Seq.cons a (op c (f b'))

Tactic:
← hf

Goal state after:
case h
α : 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'))
hT : LipschitzWith 2⁻¹ T
f : β → Stream'.Seq α
hf : Function.IsFixedPt T f
b : β
⊢ match F b with
  | none => T f b = nil
  | some (a, c, b') => T f b = Seq.cons a (op c (T f b'))
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

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

Tactic:
let T : (β →ᵤ Seq α) → (β →ᵤ Seq α) := fun f b =>
    match F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
  have hT : LipschitzWith 2⁻¹ T := by
    rw [lipschitzWith_iff_dist_le_mul]
    intro f g
    rw [UniformFun.dist_le (by positivity)]
    intro b
    simp only [UniformFun.toFun, UniformFun.ofFun, Equiv.coe_fn_symm_mk, NNReal.coe_inv,
      NNReal.coe_ofNat, T]
    cases F b with
    | none => simp
    | some v =>
      obtain ⟨a, c, b'⟩ := v
      simp
      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
  obtain ⟨f, hf⟩ := exists_fixed_point_of_contractible T hT
  use f
  intro b
  rw [← hf]
  simp only [T]
  cases hb : F b with
  | none =>
    simp
  | some v =>
    obtain ⟨a, c, b'⟩ := v
    simp only [cons_eq_cons, true_and]
    congr
    change f b' = T f b'
    rw [hf]

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

Goal state before:
pp: case neg
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : ¬m = 0
⊢ ω ^ b'.repr * ↑↑(m.succPNat ^ k) = ((↑m + 1) ^ ω) ^ b'.repr * (↑m + 1) ^ ↑k

Tactic:
opow_omega0

Goal state after:
case neg
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : ¬m = 0
⊢ ω ^ b'.repr * ↑↑(m.succPNat ^ k) = ω ^ b'.repr * (↑m + 1) ^ ↑k

case neg.a1
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : ¬m = 0
⊢ 1 < ↑m + 1

case neg.h
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : ¬m = 0
⊢ ↑m + 1 < ω
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case cons.cons.cons
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s_hd : α
s_tl : Stream'.Seq α
x✝¹ : α
s✝¹ : Stream'.Seq α
ht0 : op (Seq.cons s_hd nil) = Seq.cons x✝¹ s✝¹
x✝ : α
s✝ : Stream'.Seq α
ht : op (Seq.cons s_hd s_tl) = Seq.cons x✝ s✝
this : (Seq.cons x✝¹ s✝¹).head = (Seq.cons x✝ s✝).head
⊢ (Seq.cons x✝ s✝).destruct =
    Option.map (fun x ↦ (x.1, ↑x.2 s_tl))
      (match (Seq.cons x✝¹ s✝¹).destruct with
      | none => none
      | some (t_hd, snd) => some (t_hd, ⟨fun s_tl ↦ (op (Seq.cons s_hd s_tl)).tail, ⋯⟩))

Tactic:
simp_all

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

Goal state before:
pp: case nil
x : ℝ
m2 : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length m2 = [].length
h_pos : ∀ f ∈ basis, 0 < f x
⊢ (List.zipWith (fun exp b ↦ b x ^ exp) (List.zipWith (fun x1 x2 ↦ x1 + x2) [] m2) basis).prod =
    (List.zipWith (fun exp b ↦ b x ^ exp) [] basis).prod * (List.zipWith (fun exp b ↦ b x ^ exp) m2 basis).prod

Tactic:
simp_all

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

Goal state before:
pp: β : Type u_1
γ : Type u_2
basis_hd : ℝ → ℝ
basis_tl : Basis
F : β → Option (ℝ × MultiseriesExpansion basis_tl × γ × β)
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
inst✝ : FriendlyOperationClass op
b : β
h : F b = none
⊢ Seq.gcorec
      (fun a ↦
        Option.map
          (fun x ↦
            match x with
            | (exp, coef, c, next) => ((exp, coef), c, next))
          (F a))
      op b =
    nil

Tactic:
Seq.gcorec_nil

Goal state after:
β : Type u_1
γ : Type u_2
basis_hd : ℝ → ℝ
basis_tl : Basis
F : β → Option (ℝ × MultiseriesExpansion basis_tl × γ × β)
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
inst✝ : FriendlyOperationClass op
b : β
h : F b = none
⊢ Seq.nil = nil

β : Type u_1
γ : Type u_2
basis_hd : ℝ → ℝ
basis_tl : Basis
F : β → Option (ℝ × MultiseriesExpansion basis_tl × γ × β)
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
inst✝ : FriendlyOperationClass op
b : β
h : F b = none
⊢ Option.map
      (fun x ↦
        match x with
        | (exp, coef, c, next) => ((exp, coef), c, next))
      (F b) =
    none
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: 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
h_all : ∀ x ∈ Multiseries.cons tl_exp tl_coef tl_tl, (exp, coef) > x
h_Pairwise : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (Multiseries.cons tl_exp tl_coef tl_tl)
x : ℝ × MultiseriesExpansion basis_tl
hx : x ∈ (mk (Multiseries.cons tl_exp tl_coef tl_tl) 0).seq
⊢ x ∈ (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq

Tactic:
simp_all

Goal state after:
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: case ind
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
⊢ (S.decode n).encode = n

Tactic:
| _ n ih =>

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

Goal state before:
pp: case inl
a : ℤ
n : ℕ
h : IsInt a (Int.negOfNat n)
x✝ : IsSquare a
hb : -↑n = 0 * 0
⊢ n = 0

Tactic:
simp_all

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

Goal state before:
pp: case inl
a : ℚ
n : ℕ
h : IsInt a (Int.negOfNat n)
x✝ : IsSquare a
hb : -↑n = 0 * 0
⊢ n = 0

Tactic:
simp_all

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

Goal state before:
pp: case hb0
a : ℚ
n d : ℕ
hn : ¬IsSquare n
ha : IsNNRat a n d
hnd : ↑d ≤ 0
this : n ≠ 1
⊢ n.gcd d ≠ 1

Tactic:
simp_all

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

Goal state before:
pp: case hb0
a : ℚ
n d : ℕ
hd : ¬IsSquare d
ha : IsNNRat a n d
hnd : ↑d ≤ 0
⊢ n.gcd d ≠ 1

Tactic:
simp_all

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

Goal state before:
pp: a b m : ℕ
⊢ a ^ (2 * b + 1) % m = a ^ b % m * (a ^ b % m * a % m) % m

Tactic:
rw [pow_add, two_mul, pow_add, pow_one, Nat.mul_mod (a ^ b % m) a, Nat.mod_mod,
      ← Nat.mul_mod (a ^ b) a, ← Nat.mul_mod, mul_assoc]

Goal state after:
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
x✝ : ↑x_num = 0
⊢ False

Tactic:
simp_all

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

Goal state before:
pp: A : Type u_1
inst✝³ : DivisionRing A
inst✝² : TopologicalSpace A
inst✝¹ : SeparatelyContinuousMul A
inst✝ : CharZero A
r : ℚ
⊢ Continuous fun x ↦ r • x

Tactic:
by simpa only [Algebra.smul_def] using! continuous_id.const_mul _

Goal state after:
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 : β
⊢ (∃ x, ⟨a, x⟩ ∈ A.dedupKeys ∧ (decide ¬x = 0) = true) → ¬(List.dlookup a A).getD 0 = 0

pp: case mpr
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
⊢ ¬(List.dlookup a A).getD 0 = 0 → ∃ x, ⟨a, x⟩ ∈ A.dedupKeys ∧ (decide ¬x = 0) = true

Tactic:
· rintro ⟨od, hval, hod⟩
      have := List.mem_dlookup (List.nodupKeys_dedupKeys A) hval
      rw [(_ : List.dlookup a A = od)]
      · simpa using hod
      · simpa [List.dlookup_dedupKeys]

Goal state after:
case mpr
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
⊢ ¬(List.dlookup a A).getD 0 = 0 → ∃ x, ⟨a, x⟩ ∈ A.dedupKeys ∧ (decide ¬x = 0) = true
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: X : Type u_7
Y : Type u_8
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group X
inst✝⁵ : IsTopologicalGroup X
inst✝⁴ : UniformSpace Y
inst✝³ : CommGroup Y
inst✝² : IsUniformGroup Y
inst✝¹ : T0Space Y
inst✝ : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : V ∈ 𝓝 1
W : Set Y
hWo : W ∈ 𝓝 1
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f | Set.MapsTo (⇑f) U W}
S2 : Set (X →ₜ* Y) := {f | Set.MapsTo (⇑f) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe '' S3
h : Equicontinuous fun x ↦ ⇑↑x
hS4 : S4 = DFunLike.coe '' S1
⊢ LocallyCompactSpace (X →ₜ* Y)

Tactic:
replace h : Equicontinuous ((↑) : S3 → X → Y) := by
    rw [equicontinuous_iff_range, ← Set.image_eq_range] at h ⊢
    rwa [← hS4] at h

Goal state after:
X : Type u_7
Y : Type u_8
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group X
inst✝⁵ : IsTopologicalGroup X
inst✝⁴ : UniformSpace Y
inst✝³ : CommGroup Y
inst✝² : IsUniformGroup Y
inst✝¹ : T0Space Y
inst✝ : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : V ∈ 𝓝 1
W : Set Y
hWo : W ∈ 𝓝 1
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f | Set.MapsTo (⇑f) U W}
S2 : Set (X →ₜ* Y) := {f | Set.MapsTo (⇑f) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe '' S3
hS4 : S4 = DFunLike.coe '' S1
h : Equicontinuous fun x ↦ ⇑↑x
⊢ LocallyCompactSpace (X →ₜ* Y)
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: X : Type u_7
Y : Type u_8
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group X
inst✝⁵ : IsTopologicalGroup X
inst✝⁴ : UniformSpace Y
inst✝³ : CommGroup Y
inst✝² : IsUniformGroup Y
inst✝¹ : T0Space Y
inst✝ : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : V ∈ 𝓝 1
W : Set Y
hWo : W ∈ 𝓝 1
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f | Set.MapsTo (⇑f) U W}
S2 : Set (X →ₜ* Y) := {f | Set.MapsTo (⇑f) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe '' S3
hS4 : S4 = DFunLike.coe '' S1
h : Equicontinuous fun x ↦ ⇑↑x
⊢ DFunLike.coe '' S1 = (U.pi fun x ↦ W) ∩ Set.range DFunLike.coe

Tactic:
Set.ext_iff,

Goal state after:
X : Type u_7
Y : Type u_8
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group X
inst✝⁵ : IsTopologicalGroup X
inst✝⁴ : UniformSpace Y
inst✝³ : CommGroup Y
inst✝² : IsUniformGroup Y
inst✝¹ : T0Space Y
inst✝ : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : V ∈ 𝓝 1
W : Set Y
hWo : W ∈ 𝓝 1
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f | Set.MapsTo (⇑f) U W}
S2 : Set (X →ₜ* Y) := {f | Set.MapsTo (⇑f) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe '' S3
hS4 : S4 = DFunLike.coe '' S1
h : Equicontinuous fun x ↦ ⇑↑x
⊢ ∀ (x : X → Y), x ∈ DFunLike.coe '' S1 ↔ x ∈ (U.pi fun x ↦ W) ∩ Set.range DFunLike.coe
Module: Mathlib.Topology.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝⁵ : Monoid R
inst✝⁴ : StarMul R
inst✝³ : TopologicalSpace R
inst✝² : T1Space R
inst✝¹ : ContinuousStar R
inst✝ : ContinuousMul R
f : R → R × R := fun u ↦ (star u * u, u * star u)
hf : f ⁻¹' {(1, 1)} = ↑(unitary R)
⊢ IsClosed ↑(unitary R)

Tactic:
← hf

Goal state after:
R : Type u_1
inst✝⁵ : Monoid R
inst✝⁴ : StarMul R
inst✝³ : TopologicalSpace R
inst✝² : T1Space R
inst✝¹ : ContinuousStar R
inst✝ : ContinuousMul R
f : R → R × R := fun u ↦ (star u * u, u * star u)
hf : f ⁻¹' {(1, 1)} = ↑(unitary R)
⊢ IsClosed (f ⁻¹' {(1, 1)})
Module: Mathlib.Topology.CWComplex.Classical.Graph

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
e : cell C 1
h : (cellFrontier 1 e).Subsingleton
x : cell C 0
hxy : cellFrontier 1 e = {↑(map 0 x) ![], ↑(map 0 x) ![]}
⊢ cellFrontier 1 e = closedCell 0 x

Tactic:
simp [hxy, closedCell_zero_eq_singleton]

Goal state after:
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: case neg
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
x : X
hx : U = {x}
⊢ (U ∩ (derivedSet a ∩ derivedSet b)).Nonempty

Tactic:
simp_all

Goal state after:
Module: Mathlib.Topology.CantorBendixson

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ Preperfect s ↔ ∀ (a : Ordinal.{u}), sᵈ[a] = s

Tactic:
rw [preperfect_iff_eq_relDerivedSet, eq_comm,
    ← (gfpApprox_eq_all_of_fixedPoint relDerivedSet (relDerivedSet_subset))]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ (o : Ordinal.{u}), gfpApprox relDerivedSet s o = s) ↔ ∀ (a : Ordinal.{u}), sᵈ[a] = s
Module: Mathlib.Topology.CWComplex.Classical.Finite

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
finite : _root_.Finite ((n : ℕ) × cell C n)
h✝ : IsEmpty ((n : ℕ) × cell C n)
⊢ ∀ (b : ℕ), 0 ≤ b → IsEmpty (cell C b)

Tactic:
simp_all

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C n
⊢ ∃ I, cellFrontier n i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j

Tactic:
by
  rcases mapsTo n i with ⟨I, hI⟩
  use I
  rw [mapsTo_iff_image_subset] at hI
  exact hI

Goal state after:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: case h
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
S : Set (Ultrafilter X.A)
hS : S ∈ T2
x✝ : Ultrafilter X.A
⊢ x✝ ∈ Set.univ → x✝ ∈ basic Set.univ

Tactic:
intro
          apply Filter.univ_sets

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝¹ : CWComplex C
inst✝ : T2Space X
A : Set X
asubc : A ⊆ C
this : IsClosed[t] A ↔ (∀ (n : ℕ) (j : cell C n), IsClosed[t] (A ∩ closedCell n j)) ∧ IsClosed[t] (A ∩ ∅)
⊢ IsClosed[t] A ↔ ∀ (n : ℕ) (j : cell C n), IsClosed[t] (A ∩ closedCell n j)

Tactic:
simp_all

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case e_s
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
e : cell C 1
f : Fin 1 → ℝ
⊢ f 0 = 1 ∨ f 0 = -1 ↔ f = -1 ∨ f = 1

Tactic:
eq_const_of_unique (f := f),

Goal state after:
case e_s
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
e : cell C 1
f : Fin 1 → ℝ
⊢ const (Fin 1) (f default) 0 = 1 ∨ const (Fin 1) (f default) 0 = -1 ↔
    const (Fin 1) (f default) = -1 ∨ const (Fin 1) (f default) = 1
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
x : I → Bool
i : I
⊢ (if J i then if K i then x i else false else false) = if J i then x i else false

Tactic:
simp_all

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
this : D ∪ ⋃ n, ⋃ j, openCell n j = D ∪ ⋃ m, ⋃ (_ : ↑m < ⊤), ⋃ j, closedCell m j
⊢ D ∪ ⋃ n, ⋃ j, openCell n j = C

Tactic:
simpa [union] using this

Goal state after: