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

Goal state before:
pp: case inr
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
H : ∀ (b : Ordinal.{u}), 0 < veblenWith f 0 b
h : 0 < o
⊢ 0 < veblenWith f o a

Tactic:
← veblenWith_veblenWith_of_lt hf h

Goal state after:
case inr
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
H : ∀ (b : Ordinal.{u}), 0 < veblenWith f 0 b
h : 0 < o
⊢ 0 < veblenWith f 0 (veblenWith f o a)
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
h : o₁ < o₂
| cmp (veblenWith f o₁ a) (veblenWith f o₂ b)

Tactic:
← veblenWith_veblenWith_of_lt hf h

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
h : o₁ < o₂
| cmp (veblenWith f o₁ a) (veblenWith f o₁ (veblenWith f o₂ b))
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
h : o₂ < o₁
| cmp (veblenWith f o₁ a) (veblenWith f o₂ b)

Tactic:
← veblenWith_veblenWith_of_lt hf h

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
h : o₂ < o₁
| cmp (veblenWith f o₂ (veblenWith f o₁ a)) (veblenWith f o₂ b)
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case inl
⊢ 0 < veblen 0 0

pp: case inr
a : Ordinal.{u_1}
h : 0 < a
⊢ a < veblen a a

Tactic:
· simp

Goal state after:
case inr
a : Ordinal.{u_1}
h : 0 < a
⊢ a < veblen a a
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case a.inl
a : Ordinal.{u}
h : a < veblen 0 a
⊢ ω ^ veblen 0 a ∈ range (veblen 0)

pp: case a.inr
o a : Ordinal.{u}
h : a < veblen o a
ho : 0 < o
⊢ ω ^ veblen o a ∈ range (veblen o)

Tactic:
· simp

Goal state after:
case a.inr
o a : Ordinal.{u}
h : a < veblen o a
ho : 0 < o
⊢ ω ^ veblen o a ∈ range (veblen o)
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: a x : Ordinal.{u}
⊢ x.invVeblen₂ < a ↔ ω ^ x < veblen x.invVeblen₁ a

Tactic:
by
  rw [← veblen_lt_veblen_iff_right (o := x.invVeblen₁), veblen_invVeblen₁_invVeblen₂]

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

Goal state before:
pp: a x : Ordinal.{u}
⊢ a < x.invVeblen₂ ↔ veblen x.invVeblen₁ a < ω ^ x

Tactic:
by
  rw [← veblen_lt_veblen_iff_right (o := x.invVeblen₁), veblen_invVeblen₁_invVeblen₂]

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

Goal state before:
pp: x y : Class.{u}
h : Set.Nonempty x
H : ∀ z ∈ x, y ∈ z
⊢ y ∈ ⋂₀ x

Tactic:
simp_rw [mem_def, sInter_apply]

Goal state after:
x y : Class.{u}
h : Set.Nonempty x
H : ∀ z ∈ x, y ∈ z
⊢ ∃ x_1, ↑x_1 = y ∧ ∀ (z : ZFSet.{u}), x z → x_1 ∈ z
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: x : ZFSet.{u}
⊢ Function.Injective fun x ↦ ⟨↑x, ⋯⟩

Tactic:
by intro _ _; simp

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

Goal state before:
pp: x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ∈ y ∨ x = y ∨ y ∈ x

Tactic:
rw [eq_comm, ← subset_iff_eq_or_mem hy hx]

Goal state after:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ∈ y ∨ y ⊆ x
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case eq.succ
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
n✝ : ℕ
mn : ↑n₁ - ↑n₂ = n✝ + 1
⊢ ω ^ e₁.repr * ↑(succ n✝) + a₁.repr = ω ^ e₁.repr * ↑(↑n₂ + (n✝ + 1)) + a₁.repr - (ω ^ e₁.repr * ↑↑n₂ + a₂.repr)

Tactic:
Nat.cast_add,

Goal state after:
case eq.succ
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
n✝ : ℕ
mn : ↑n₁ - ↑n₂ = n✝ + 1
⊢ ω ^ e₁.repr * ↑(succ n✝) + a₁.repr = ω ^ e₁.repr * (↑↑n₂ + ↑(n✝ + 1)) + a₁.repr - (ω ^ e₁.repr * ↑↑n₂ + a₂.repr)
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: case limit.refine_2
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ lift.{u + 1, u} o.card ≤ lift.{u + 1, u} (⨆ i, (V_ ↑i).card)

Tactic:
lift_le

Goal state after:
case limit.refine_2
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ o.card ≤ ⨆ i, (V_ ↑i).card
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a.toZFSet ⊆ b.toZFSet ↔ a ≤ b

Tactic:
refine ⟨?_, fun h ↦ toZFSet_monotone h⟩
  contrapose!
  exact fun h ↦ not_subset_of_mem (toZFSet_mem_toZFSet_of_lt h)

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

Goal state before:
pp: case refine_1
x : ZFSet.{u}
h : x.IsOrdinal
⊢ x ∈ Set.range toZFSet

pp: case refine_2
x : ZFSet.{u}
⊢ x ∈ Set.range toZFSet → x.IsOrdinal

Tactic:
· rw [← h.toZFSet_rank_eq]
    exact Set.mem_range_self _

Goal state after:
case refine_2
x : ZFSet.{u}
⊢ x ∈ Set.range toZFSet → x.IsOrdinal
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case succ
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
⊢ (k + 1 ≠ 0 → R' < (ω ^ a0.repr) ^ succ ↑(k + 1)) ∧
    (ω ^ a0.repr) ^ ↑(k + 1) * (ω ^ a0.repr * ↑↑n + a'.repr) + R' = (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ succ ↑(k + 1)

Tactic:
have α0 : 0 < α' := by simpa [lt_def, repr] using oadd_pos a0 n a'

Goal state after:
case succ
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 < α'
⊢ (k + 1 ≠ 0 → R' < (ω ^ a0.repr) ^ succ ↑(k + 1)) ∧
    (ω ^ a0.repr) ^ ↑(k + 1) * (ω ^ a0.repr * ↑↑n + a'.repr) + R' = (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ succ ↑(k + 1)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: f g : ℝ → ℝ
basis_begin : List (ℝ → ℝ)
basis_end : ℝ → ℝ
h_comp : (Real.log ∘ f) =o[atTop] (Real.log ∘ basis_end)
hg : g ∈ basis_begin
h :
  List.Pairwise (fun x y ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) (basis_begin ++ [basis_end]) ∧
    ∀ (f : ℝ → ℝ), f ∈ basis_begin ∨ f = basis_end → Tendsto f atTop atTop
⊢ (Real.log ∘ basis_end) =o[atTop] (Real.log ∘ g)

Tactic:
by grind

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

Goal state before:
pp: f g basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_comp : (Real.log ∘ basis_hd) =o[atTop] (Real.log ∘ f)
hg : g ∈ basis_tl
h :
  ((∀ a' ∈ basis_tl, (Real.log ∘ a') =o[atTop] (Real.log ∘ basis_hd)) ∧
      List.Pairwise (fun x y ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) basis_tl) ∧
    Tendsto basis_hd atTop atTop ∧ ∀ a ∈ basis_tl, Tendsto a atTop atTop
⊢ (Real.log ∘ g) =o[atTop] (Real.log ∘ basis_hd)

Tactic:
by grind

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

Goal state before:
pp: left right : Basis
f : ℝ → ℝ
h : WellFormedBasis (left ++ right)
hf_tendsto : Tendsto f atTop atTop
hf_comp_right : ∀ (g : ℝ → ℝ), List.head? right = some g → (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
this : WellFormedBasis (f :: right)
hf_comp_left : ∀ g ∈ left, (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
g : ℝ → ℝ
hg : g ∈ left
⊢ ∀ (g_1 : ℝ → ℝ), (f :: right).head? = some g_1 → (Real.log ∘ g_1) =o[atTop] (Real.log ∘ g)

Tactic:
by grind

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
h : WellFormedBasis (basis_hd :: basis_tl)
⊢ ∀ (x : ℝ), (basis_hd ∈ basis_hd :: basis_tl → 0 < basis_hd x) → 0 < basis_hd x

Tactic:
by grind

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) = ω ^ b'.repr * (↑m + 1) ^ ↑k

pp: 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

pp: 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 < ω

Tactic:
· simp

Goal state after:
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.Monomial.Basic

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

Tactic:
induction m1 generalizing m2 basis with
  | nil =>
    symm at h_length
    simp_all
  | cons exp1 exps1 ih =>
    cases m2 with
    | nil => simp at h_length
    | cons exp2 exps2 =>
    cases basis with
    | nil => simp
    | cons basis_hd basis_tl =>
      simp only [List.zipWith_cons_cons, List.prod_cons] at ih ⊢
      have h1 : exps1.length = exps2.length := by grind
      have h2 : ∀ f ∈ basis_tl, 0 < f x := by grind
      have h3 : 0 < basis_hd x := h_pos _ (by simp)
      rw [ih h_basis.tail h1 h2, Real.rpow_add h3]
      grind

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

Goal state before:
pp: exps_hd : ℝ
basis_hd : ℝ → ℝ
h_nonzero : exps_hd ≠ 0
e : ℝ
es : List ℝ
ih :
  ∀ {basis_tl : Basis},
    (∀ b ∈ basis_tl, (log ∘ b) =o[atTop] (log ∘ basis_hd)) → toLogFun es basis_tl =o[atTop] (log ∘ basis_hd)
b : ℝ → ℝ
bs : List (ℝ → ℝ)
hlo : ∀ b_1 ∈ b :: bs, (log ∘ b_1) =o[atTop] (log ∘ basis_hd)
⊢ ∀ b ∈ bs, (log ∘ b) =o[atTop] (log ∘ basis_hd)

Tactic:
by grind

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

Goal state before:
pp: case h_Pairwise
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
h_coef : coef.Sorted
⊢ Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (cons exp coef Multiseries.nil) 0).seq

Tactic:
· simp

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

Goal state before:
pp: case cons
m1 m2 : UnitMonomial
h_lt : m1 < m2
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h1 : List.length m1 = (basis_hd :: basis_tl).length
h2 : List.length m2 = (basis_hd :: basis_tl).length
⊢ m1.toFun (basis_hd :: basis_tl) =o[atTop] m2.toFun (basis_hd :: basis_tl)

Tactic:
obtain _ | ⟨exp1, m1⟩ := m1

Goal state after:
case cons.nil
m2 : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h2 : List.length m2 = (basis_hd :: basis_tl).length
h_lt : [] < m2
h1 : [].length = (basis_hd :: basis_tl).length
⊢ toFun [] (basis_hd :: basis_tl) =o[atTop] m2.toFun (basis_hd :: basis_tl)

case cons.cons
m2 : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h2 : List.length m2 = (basis_hd :: basis_tl).length
exp1 : ℝ
m1 : List ℝ
h_lt : exp1 :: m1 < m2
h1 : (exp1 :: m1).length = (basis_hd :: basis_tl).length
⊢ toFun (exp1 :: m1) (basis_hd :: basis_tl) =o[atTop] m2.toFun (basis_hd :: basis_tl)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case a
α : Type u_1
γ : Type u_3
s t : Stream'.Seq α
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
base : motive s t
step :
  ∀ (u v : Stream'.Seq α),
    motive u v → u = v ∨ ∃ hd u' v' c, u = Seq.cons hd (op c u') ∧ v = Seq.cons hd (op c v') ∧ motive u' v'
this : ∀ (n : ℕ), dist s t ≤ 2⁻¹ ^ n
⊢ 0 ≤ dist s t

Tactic:
· simp

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

Goal state before:
pp: case oadd.inl.none.inl.none.zero.left
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
⊢ 1 = succ 0

pp: case oadd.inl.none.inl.none.zero.right
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
⊢ (oadd 0 1 0).NF → NF 0

Tactic:
· simp

Goal state after:
case oadd.inl.none.inl.none.zero.right
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
⊢ (oadd 0 1 0).NF → NF 0
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: 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'
⊢ ms.replaceFun f = ms.replaceFun f ∧ ms.Approximates ∧ ms.toFun =ᶠ[atTop] f

Tactic:
by grind

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

Goal state before:
pp: n k d m : ℕ
h_right : m ^ d < (k + 1) ^ d
h_left : k ^ d < m ^ d
h : n = m ^ d
⊢ False

Tactic:
have : k < m := lt_of_pow_lt_pow_left' d h_left

Goal state after:
n k d m : ℕ
h_right : m ^ d < (k + 1) ^ d
h_left : k ^ d < m ^ d
h : n = m ^ d
this : k < m
⊢ False
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case h.some
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬(List.dlookup a A.dedupKeys).getD 0 = 0
val✝ : β
haA : List.dlookup a A.dedupKeys = some val✝
⊢ some val✝ = some ((some val✝).getD 0) ∧ decide True = true

Tactic:
· simp

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

Goal state before:
pp: case cons.zero.cons
α : Type u
inst✝ : DecidableEq α
y x' : α
xs : List α
h₀ : (x' :: xs).Nodup
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x' → (applyId (xs.zip ys) x' = y ↔ ys[i]? = some y)
head✝ : α
tail✝ : List α
h₁ : (x' :: xs).length = (head✝ :: tail✝).length
⊢ applyId ((x' :: xs).zip (head✝ :: tail✝)) x' = y ↔ (head✝ :: tail✝)[0]? = some y

Tactic:
· simp

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: case inl
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
f : X → α
⊢ Tendsto (⇑UniformFun.ofFun ∘ F) ⊥ (𝓝 (UniformFun.ofFun f)) ↔ Tendsto F ⊥ (𝓝 f)

pp: case inr
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
⊢ Tendsto (⇑UniformFun.ofFun ∘ F) ℱ (𝓝 (UniformFun.ofFun f)) ↔ Tendsto F ℱ (𝓝 f)

Tactic:
· simp

Goal state after:
case inr
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
⊢ Tendsto (⇑UniformFun.ofFun ∘ F) ℱ (𝓝 (UniformFun.ofFun f)) ↔ Tendsto F ℱ (𝓝 f)
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 → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
H1 :
  UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α)
H2 :
  UniformSpace.comap ((⋃₀ 𝔖).domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α)
H3 :
  ∀ K ∈ 𝔖,
    UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α) =
      UniformSpace.comap (K.domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α)
⊢ ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α)

Tactic:
iInf_congr fun K ↦ iInf_congr fun hK ↦ H3 K hK

Goal state after:
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
x : M
⊢ (1, x) ∈ mulFiber x

Tactic:
by grind

Goal state after:
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
x : M
⊢ (x, 1) ∈ mulFiber x

Tactic:
by grind

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

Goal state before:
pp: 𝕜₁ : Type u_1
E : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜₁
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜₁ E
t₁ t₂ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : ContinuousSMul 𝕜₁ E
V : Set E
𝓕₁ : Filter E := 𝓝 0
V_mem : V ∈ 𝓕₁
𝓕₂ : Filter E := 𝓝 0
H : 𝓕₁ = 𝓕₂ ⊓ 𝓟 V
c : 𝕜₁
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
⊢ V ∈ 𝓕₂

Tactic:
have c_ne : c ≠ 0 := norm_pos_iff.mp hc₀

Goal state after:
𝕜₁ : Type u_1
E : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜₁
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜₁ E
t₁ t₂ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : ContinuousSMul 𝕜₁ E
V : Set E
𝓕₁ : Filter E := 𝓝 0
V_mem : V ∈ 𝓕₁
𝓕₂ : Filter E := 𝓝 0
H : 𝓕₁ = 𝓕₂ ⊓ 𝓟 V
c : 𝕜₁
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
c_ne : c ≠ 0
⊢ V ∈ 𝓕₂
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)
⊢ ↑this.unit⁻¹ * (-(1 + x) + 1) = -↑this.unit⁻¹ * x

Tactic:
· simp

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.WithZeroMulInt

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : MulArchimedean Γ₀
inst✝ : Valued R Γ₀
x : R
hx : v x < 1
⊢ Tendsto (fun n ↦ x ^ n) atTop (𝓝 0)

Tactic:
by
  simp only [(hasBasis_nhds_zero _ _).tendsto_right_iff, mem_ofPred_eq, map_pow, eventually_atTop,
    forall_const]
  intro y
  let v : Valuation R Γ₀ := Valued.v
  obtain ⟨n, hn⟩ := exists_pow_lt₀ hx
    (Units.map (MonoidWithZeroHom.ValueGroup₀.embedding (f := (.ofClass v))) y)
  refine ⟨n, fun m hm ↦ ?_⟩
  rw [← map_pow, Valuation.restrict_lt_iff_lt_embedding]
  refine hn.trans_le' ?_
  rw [map_pow]
  exact pow_le_pow_right_of_le_one' hx.le hm

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : cell C n
hi : i ∈ E.I n
⊢ closure[t] (openCell n i) ⊆ ↑E

Tactic:
E.closed.closure_subset_iff,

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : cell C n
hi : i ∈ E.I n
⊢ openCell n i ⊆ ↑E
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
⊢ IsClosed[inst✝¹] (derivedSet a)

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
⊢ IsClosed[inst✝¹] (derivedSet b)

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

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).Nonempty

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 b).Nonempty

Tactic:
· simp

Goal state after:
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
⊢ IsClosed[inst✝¹] (derivedSet b)

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

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).Nonempty

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 b).Nonempty