mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case neg.convert_8
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
h : ¬v.headI = 0
this :
  natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
s' : Cfg'
h₁ : TrCfg (stepNormal f (Cont.fix f k) v.tail) s'
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal f (trCont (Cont.fix f k))), var := some Γ'.cons,
      stk := elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) }
    s'
⊢ Option.elim'
    (update (elim (trList v) [] [] (trContStack (Cont.fix f k))) main (trList v).tail main = (trNat v.headI).tail ∧
      trList v.tail = [])
    (fun a ↦
      natEnd a = true ∧
        update (elim (trList v) [] [] (trContStack (Cont.fix f k))) main (trList v).tail main =
          (trNat v.headI).tail ++ a :: trList v.tail)
    (some Γ'.cons)

Tactic:
· exact ⟨rfl, this.2⟩

Goal state after:
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: J : Type v
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
inhabit α
  obtain ⟨j, gg, h⟩ := exists_locallyConstant_finite_aux _ hC f
  classical
  let ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
  let σ : (α → Fin 2) → α := fun f => if h : ∃ a : α, ι a = f then h.choose else default
  refine ⟨j, gg.map σ, ?_⟩
  ext x
  simp only [LocallyConstant.coe_comap, LocallyConstant.map_apply,
    Function.comp_apply]
  dsimp [σ]
  have h1 : ι (f x) = gg (C.π.app j x) := by
    change f.map (fun a b => if a = b then (0 : Fin 2) else 1) x = _
    rw [h]
    rfl
  have h2 : ∃ a : α, ι a = gg (C.π.app j x) := ⟨f x, h1⟩
  rw [dif_pos]
  swap
  · assumption
  apply_fun ι
  · rw [h2.choose_spec]
    exact h1
  · intro a b hh
    have hhh := congr_fun hh a
    dsimp [ι] at hhh
    rw [if_pos rfl] at hhh
    split_ifs at hhh with hh1
    · exact hh1.symm
    · exact False.elim (bot_ne_top hhh)

Goal state after:
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case inl
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
ff : Quotient S.toSetoid → α := ⇑f.lift
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (j : J), Nonempty ↑(F.obj j).toTop
this : ∀ (j : J), Nonempty ↑((F ⋙ toTopCat).obj j)
⊢ False

Tactic:
have : ∀ j : J, T2Space ((F ⋙ Profinite.toTopCat).obj j) := fun j =>
      (inferInstance : T2Space (F.obj j))

Goal state after:
case inl
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
ff : Quotient S.toSetoid → α := ⇑f.lift
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (j : J), Nonempty ↑(F.obj j).toTop
this✝ : ∀ (j : J), Nonempty ↑((F ⋙ toTopCat).obj j)
this : ∀ (j : J), T2Space ↑((F ⋙ toTopCat).obj j)
⊢ False
Module: Mathlib.Condensed.Light.Epi

Goal state before:
pp: case hF
R : Type u_1
inst✝ : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ ∀ (n : ℕ), Epi ((F ⋙ forget R).map (homOfLE ⋯).op)

Tactic:
exact fun _ ↦ (forget R).map_epi _

Goal state after:
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X✝ X : CondensedSet
x✝² x✝¹ : CompHausᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ (X.obj.map x✝ ≫
      ↾fun x ↦
        { toFun := fun s ↦ (ConcreteCategory.hom (X.obj.map (CompHausLike.const (of PUnit.{u + 1}) s).op)) x,
          continuous_toFun := ⋯ }) =
    (↾fun x ↦
        { toFun := fun s ↦ (ConcreteCategory.hom (X.obj.map (CompHausLike.const (of PUnit.{u + 1}) s).op)) x,
          continuous_toFun := ⋯ }) ≫
      X.toTopCat.toCondensedSet.obj.map x✝

Tactic:
by
      ext
      simp only [TypeCat.Fun.toFun_apply,
        comp_apply, TopCat.toSheafCompHausLike_obj_map, ConcreteCategory.hom_ofHom,
        TypeCat.Fun.coe_mk, ← Functor.map_comp_apply]
      rfl

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : TopologicalSpace T
inst✝³ : TopologicalSpace X
inst✝² : DiscreteTopology X
inst✝¹ : T2Space T
inst✝ : CompactSpace S
π : T → S × OnePoint X
hπ : Continuous π
σ : Option X → S → T
hσ : ∀ (x : Option X), Continuous (σ x)
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
⊢ IsOpen (fibres π σ)ᶜ

Tactic:
rw [fibres_compl_eq_iUnion π σ hσ']

Goal state after:
S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : TopologicalSpace T
inst✝³ : TopologicalSpace X
inst✝² : DiscreteTopology X
inst✝¹ : T2Space T
inst✝ : CompactSpace S
π : T → S × OnePoint X
hπ : Continuous π
σ : Option X → S → T
hσ : ∀ (x : Option X), Continuous (σ x)
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
⊢ IsOpen (⋃ i, (Set.range (σ (Option.some i)))ᶜ ∩ Prod.snd ∘ π ⁻¹' {↑i})
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : T2Space S
inst✝³ : TopologicalSpace T
inst✝² : CompactSpace T
inst✝¹ : TopologicalSpace X
inst✝ : T1Space (OnePoint X)
π : T → S × OnePoint X
hπ : Continuous π
⊢ IsCompact (S' π)

Tactic:
show S' π =
    ⋂ (n : OnePoint X) (m : OnePoint X), {x | (π (x n).val).1 = (π (x m).val).1} by aesop

Goal state after:
S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : T2Space S
inst✝³ : TopologicalSpace T
inst✝² : CompactSpace T
inst✝¹ : TopologicalSpace X
inst✝ : T1Space (OnePoint X)
π : T → S × OnePoint X
hπ : Continuous π
⊢ IsCompact (⋂ n, ⋂ m, {x | (π ↑(x n)).1 = (π ↑(x m)).1})
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ #(Ioc f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i)) - 1

Tactic:
card_Ioc_eq_card_Icc_sub_one,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ #(Icc f g) - 1 = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i)) - 1
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : List (Sigma β)
⊢ lookup a s.toAList = dlookup a s

Tactic:
by
  rw [List.toAList, lookup, dlookup_dedupKeys]

Goal state after:
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : AList β
⊢ ∀ (x : α) (y : β x), y ∈ dlookup x (s₁ ∪ s₂ ∪ s₃).entries ↔ y ∈ dlookup x (s₁ ∪ (s₂ ∪ s₃)).entries

Tactic:
simp [not_or, or_assoc, and_or_left, and_assoc]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s✝ : Finmap β
s : AList β
h : a ∉ ⟦s⟧
⊢ (insert a b ⟦s⟧).entries = ⟨a, b⟩ ::ₘ ⟦s⟧.entries

Tactic:
simp [AList.entries_insert_of_notMem (mt mem_toFinmap.1 h), -entries_insert]

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
h₁ : a = ah
h₂ : ¬a' = ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)

pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
h₁ : ¬a = ah
h₂ : a' = ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)

pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
h₁ : ¬a = ah
h₂ : ¬a' = ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)

Tactic:
· subst h₁
      simp [h₂]

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
h₁ : ¬a = ah
h₂ : a' = ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
h₁ : ¬a = ah
h₂ : ¬a' = ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a₁ a₂ : α
l : List (Sigma β)
h : ¬a₁ = a₂
ha₂ : a₂ ∈ l.keys
b₁ : β a₁
l₁ l₂ : List (Sigma β)
a₁_nin_l₁ : ¬a₁ ∈ l₁.keys
x✝ : a₂ ∈ (l₁ ++ ⟨a₁, b₁⟩ :: l₂).keys
ha₁ : a₁ ∈ (l₁ ++ ⟨a₁, b₁⟩ :: l₂).keys
h' : a₂ ∈ l₁.keys
⊢ kerase a₂ (l₁ ++ l₂) = kerase a₁ (kerase a₂ (l₁ ++ ⟨a₁, b₁⟩ :: l₂))

Tactic:
simp [kerase_append_left h',
              kerase_append_right (mt (mem_keys_kerase_of_ne h).mp a₁_nin_l₁)]

Goal state after:
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: a b : ℤ
⊢ a.natAbs ≤ b.natAbs ↔ a ^ 2 ≤ b ^ 2

Tactic:
rw [sq, sq]
  exact natAbs_le_iff_mul_self_le

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: ⊢ bitwise and = land

Tactic:
by
  funext m n
  rcases m with m | m <;> rcases n with n | n <;> try {rfl}
    <;> simp only [bitwise, natBitwise, Bool.not_false,
      cond_false, cond_true, Bool.and_true,
      Bool.and_false]
  · rw [Nat.bitwise_swap, Function.swap]
    congr
    funext x y
    cases x <;> cases y <;> rfl
  · congr
    simp

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ (bit a m).lor (bit b n) = bit (a || b) (m.lor n)

Tactic:
by
  rw [← bitwise_or, bitwise_bit]

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n : ℕ
⊢ ↑m >>> ↑n = ↑(m >>> n)

Tactic:
cases n <;> rfl

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n : ℕ
⊢ -[m+1] >>> ↑n = -[m >>> n+1]

Tactic:
cases n <;> rfl

Goal state after:
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case mp
a b r v : ℕ
x : ℤ
y : ℕ
⊢ ((a ≤ y ∧ y < b) ∧ ↑y ≡ ↑v [ZMOD ↑r]) ∧ ↑y = x → (↑a ≤ x ∧ x < ↑b) ∧ x ≡ ↑v [ZMOD ↑r]

Tactic:
⟨h, c⟩

Goal state after:
case mp
a b r v : ℕ
x : ℤ
y : ℕ
h : (a ≤ y ∧ y < b) ∧ ↑y ≡ ↑v [ZMOD ↑r]
c : ↑y = x
⊢ (↑a ≤ x ∧ x < ↑b) ∧ x ≡ ↑v [ZMOD ↑r]
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case mp
a b r v : ℕ
x : ℤ
y : ℕ
⊢ ((a < y ∧ y ≤ b) ∧ ↑y ≡ ↑v [ZMOD ↑r]) ∧ ↑y = x → (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r]

Tactic:
⟨h, c⟩

Goal state after:
case mp
a b r v : ℕ
x : ℤ
y : ℕ
h : (a < y ∧ y ≤ b) ∧ ↑y ≡ ↑v [ZMOD ↑r]
c : ↑y = x
⊢ (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r]
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ↑(count (fun x ↦ x ≡ v [MOD r]) b) = ⌈(↑b - ↑(v % r)) / ↑r⌉

Tactic:
count_eq_card_filter_range,

Goal state after:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ↑(#({x ∈ range b | x ≡ v [MOD r]})) = ⌈(↑b - ↑(v % r)) / ↑r⌉
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ rdropWhile p l = l ↔ ∀ (hl : l ≠ []), ¬p (l.getLast hl) = true

Tactic:
by
  simp [rdropWhile, reverse_eq_iff, getLast_eq_getElem, Nat.pos_iff_ne_zero]

Goal state after:
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
bs : List β
⊢ map₂Right' f [] bs = (map (f none) bs, [])

Tactic:
by cases bs <;> rfl

Goal state after:
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
bs : List β
⊢ map₂Right f [] bs = map (f none) bs

Tactic:
by cases bs <;> rfl

Goal state after:
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case inr.nil
α : Type u_1
r : α → α → Prop
s₁ s₂ : List α
h : Shortlex r s₁ s₂
h2 : s₁.length = s₂.length ∧ Lex r s₁ s₂
⊢ Shortlex r s₁ (s₂ ++ [])

Tactic:
rw [List.append_nil]

Goal state after:
case inr.nil
α : Type u_1
r : α → α → Prop
s₁ s₂ : List α
h : Shortlex r s₁ s₂
h2 : s₁.length = s₂.length ∧ Lex r s₁ s₂
⊢ Shortlex r s₁ s₂
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case inr.nil
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
h2 : t₁.length = t₂.length ∧ Lex r t₁ t₂
⊢ Shortlex r ([] ++ t₁) ([] ++ t₂)

Tactic:
rw [List.nil_append, List.nil_append]
    exact h

Goal state after:
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
q k : ℕ
w : List α
per_q : ∀ i < w.length - q, w[i]? = w[i + q]?
per_plus : ∀ i < w.length - (k + q), w[i]? = w[i + (k + q)]?
i : ℕ
i_lt : i < w.length - q - k
⊢ w[q + i]? = w[q + (i + k)]?

Tactic:
calc
     w[q + i]? = w[i + q]? := congrArg (getElem? w) (add_comm q i)
     _ = w[i]? := (per_q i (by lia)).symm
     _ = w[i + (k + q)]? := per_plus i (by lia)
     _ = w[q + (i + k)]? := congr_arg (getElem? w) (by lia)

Goal state after:
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: case succ
A : Type u_1
inst✝ : Semiring A
k : ℕ
ih : ∀ {m : ℕ}, IsUnit ↑(m + k)! → IsUnit ↑m !
m : ℕ
hn_fac : IsUnit ↑(m + 1 + k)!
this : IsUnit ↑(m + 1) ∧ IsUnit ↑m !
⊢ IsUnit ↑m !

Tactic:
exact this.2

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ZNum
⊢ - -n = n

Tactic:
cases n <;> rfl

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ZNum
⊢ -n.bit1 = (-n).bitm1

Tactic:
cases n <;> rfl

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ZNum
⊢ -n.bitm1 = (-n).bit1

Tactic:
cases n <;> rfl

Goal state after:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x✝ : α
r : Ordnode α
lo✝ : WithBot α
hi✝ : WithTop α
ol : l.Bounded lo✝ ↑x✝
Or : r.Bounded (↑x✝) hi✝
sl : l.Sized
sr : r.Sized
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
ol' : l.dual.Bounded (↑x✝) lo✝
sl' : l.dual.Sized
bl' : l.dual.Balanced
or' : r.dual.Bounded hi✝ ↑x✝
sr' : r.dual.Sized
br' : r.dual.Balanced
⊢ BalancedSz r.size l.size

Tactic:
exact b.symm

Goal state after:
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
⊢ count p (nth p 0) = 0

Tactic:
count_eq_card_filter_range,

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
⊢ #({x ∈ range (nth p 0) | p x}) = 0
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case succ
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
ihk : (∀ (hf : (Set.ofPred p).Finite), k < #hf.toFinset) → count p (nth p k) = k
hn : ∀ (hf : (Set.ofPred p).Finite), k + 1 < #hf.toFinset
⊢ count p (nth p (k + 1)) = k + 1

Tactic:
count_eq_card_filter_range,

Goal state after:
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
ihk : (∀ (hf : (Set.ofPred p).Finite), k < #hf.toFinset) → count p (nth p k) = k
hn : ∀ (hf : (Set.ofPred p).Finite), k + 1 < #hf.toFinset
⊢ #({x ∈ range (nth p (k + 1)) | p x}) = k + 1
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
n : ℕ
hp : ∀ n' ≤ n, p n'
⊢ nth p n = n

Tactic:
classical nth_rw 1 [← count_of_forall (hp · ·.le), nth_count (hp n le_rfl)]

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ZNum
⊢ n + 0 = n

Tactic:
cases n <;> rfl

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ZNum
⊢ 0 + n = n

Tactic:
cases n <;> rfl

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case inl.zero
l r₁ : ℕ
H : l + r₁ ≤ 1
h₁ : r₁ ≤ 0
h₂ : l + 0 ≤ 1 ∨ 0 ≤ delta * l
h : ¬l + 0 ≤ 1
⊢ l ≤ delta * 0

Tactic:
cases h (le_trans (Nat.add_le_add_left (Nat.zero_le _) _) H)

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
size✝ : ℕ
l : Ordnode α
x✝ : α
r : Ordnode α
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
⊢ BalancedSz r.size l.size

Tactic:
exact b.symm

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ZNum
⊢ n.div 0 = 0

Tactic:
cases n <;> rfl

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case mpr.succ.step.f.f.refl
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
y_a : F.A
y_f : F.B y_a → F.M
a✝¹ : M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩
a✝ : M.mk ⟨a, x'⟩ = M.mk ⟨a, x'⟩
⊢ Agree (CofixA.intro a fun j ↦ (x' j).approx n✝) (CofixA.intro y_a fun j ↦ (y_f j).approx (n✝ + 1))

Tactic:
replace h_a_2 := mk_inj ‹M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩›

Goal state after:
case mpr.succ.step.f.f.refl
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
y_a : F.A
y_f : F.B y_a → F.M
a✝¹ : M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩
a✝ : M.mk ⟨a, x'⟩ = M.mk ⟨a, x'⟩
h_a_2 : ⟨y_a, y_f⟩ = ⟨a, y'⟩
⊢ Agree (CofixA.intro a fun j ↦ (x' j).approx n✝) (CofixA.intro y_a fun j ↦ (y_f j).approx (n✝ + 1))
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
t : Ordnode α
h : t.dual.Sized
⊢ t.Sized

Tactic:
rw [← dual_dual t]

Goal state after:
α : Type u_1
t : Ordnode α
h : t.dual.Sized
⊢ t.dual.dual.Sized
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: ⊢ Repr PrimeMultiset

Tactic:
by delta PrimeMultiset; infer_instance

Goal state after:
Module: Mathlib.Data.PNat.Interval

Goal state before:
pp: a b : ℕ+
⊢ #(Ico a b) = #(Ico ↑a ↑b)

Tactic:
← map_subtype_embedding_Ico,

Goal state after:
a b : ℕ+
⊢ #(Ico a b) = #(map (Embedding.subtype fun n ↦ 0 < n) (Ico a b))
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case a
m n : ℕ+
⊢ (m.factorMultiset ⊓ n.factorMultiset).prod ∣ m.gcd n

Tactic:
apply dvd_gcd <;> rw [PrimeMultiset.prod_dvd_iff']

Goal state after:
case a.hm
m n : ℕ+
⊢ m.factorMultiset ⊓ n.factorMultiset ≤ m.factorMultiset

case a.hn
m n : ℕ+
⊢ m.factorMultiset ⊓ n.factorMultiset ≤ n.factorMultiset
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case a
m n : ℕ+
⊢ m.factorMultiset ⊓ n.factorMultiset ≤ (m.gcd n).factorMultiset

Tactic:
rw [← PrimeMultiset.prod_dvd_iff, prod_factorMultiset]
    apply dvd_gcd <;> rw [PrimeMultiset.prod_dvd_iff']
    · exact inf_le_left
    · exact inf_le_right

Goal state after:
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this✝ : u = n.factorMultiset
this : v = m.factorMultiset
⊢ (n.factorMultiset ⊔ m.factorMultiset).prod = n.lcm m

Tactic:
rw [← PNat.factorMultiset_lcm n m, PNat.prod_factorMultiset]

Goal state after:
Module: Mathlib.Data.Pi.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
⊢ #(Ioc a b) = ∏ i, #(Icc (a i) (b i)) - 1

Tactic:
card_Ioc_eq_card_Icc_sub_one,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
⊢ #(Icc a b) - 1 = ∏ i, #(Icc (a i) (b i)) - 1
Module: Mathlib.Data.Pi.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderBot (α i)
b✝ b x : (i : ι) → α i
⊢ (∀ (a : ι), x a ∈ Iic (b a)) ↔ x ≤ b

Tactic:
mem_Iic,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderBot (α i)
b✝ b x : (i : ι) → α i
⊢ (∀ (a : ι), x a ≤ b a) ↔ x ≤ b
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x : α
t : Ordnode α
h : t.Valid
⊢ (Ordnode.insert x t).Valid

Tactic:
rw [insert_eq_insertWith]; exact insertWith.valid _ _ (fun _ _ => ⟨le_rfl, le_rfl⟩) h

Goal state after:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.gt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ Raised (erase x t_r).size t_r.size ∧ BalancedSz t_l.size t_r.size

Tactic:
exact And.intro t_r_size h.bal.1

Goal state after:
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mk.a
F : Type u → Type v
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
this : Wrepr (WType.mk a f) = PFunctor.W.mk (repr (abs ((P F).map Wrepr ⟨a, f⟩)))
⊢ abs (PFunctor.W.mk (repr (abs ((P F).map Wrepr ⟨a, f⟩)))).dest = abs (PFunctor.W.mk ((P F).map Wrepr ⟨a, f⟩)).dest

Tactic:
PFunctor.W.dest_mk,

Goal state after:
case mk.a
F : Type u → Type v
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
this : Wrepr (WType.mk a f) = PFunctor.W.mk (repr (abs ((P F).map Wrepr ⟨a, f⟩)))
⊢ abs (repr (abs ((P F).map Wrepr ⟨a, f⟩))) = abs (PFunctor.W.mk ((P F).map Wrepr ⟨a, f⟩)).dest
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
this : recF g ∘ fixToW = rec g
a : (P F).A
f : (P F).B a → Fix F
h : repr x = ⟨a, f⟩
⊢ g (abs ((P F).map (recF g) (PFunctor.W.mk ((P F).map fixToW ⟨a, f⟩)).dest)) = g (rec g <$> x)

Tactic:
PFunctor.W.dest_mk,

Goal state after:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
this : recF g ∘ fixToW = rec g
a : (P F).A
f : (P F).B a → Fix F
h : repr x = ⟨a, f⟩
⊢ g (abs ((P F).map (recF g) ((P F).map fixToW ⟨a, f⟩))) = g (rec g <$> x)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
⊢ abs (PFunctor.W.mk ((P F).map fixToW (repr (abs ⟨a, fun x ↦ ⟦f x⟧⟩)))).dest = abs (Wrepr (WType.mk a f)).dest

Tactic:
PFunctor.W.dest_mk,

Goal state after:
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
⊢ abs ((P F).map fixToW (repr (abs ⟨a, fun x ↦ ⟦f x⟧⟩))) = abs (Wrepr (WType.mk a f)).dest