mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Condensed.Discrete.LocallyConstant

Goal state before:
pp: P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S✝ : CompHausLike P
Y✝ : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝³ : HasProp P PUnit.{u + 1}
f✝ : LocallyConstant (↑S✝.toTop) (Y✝.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g✝ : T ⟶ S✝
X✝ : TopCat
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X Y : Sheaf (coherentTopology (CompHausLike P)) (Type (max u w))
g : X ⟶ Y
this : Preregular (CompHausLike P)
S : (CompHausLike P)ᵒᵖ
f : LocallyConstant (↑(unop S).toTop) (X.obj.obj (op (of P PUnit.{u + 1})))
a : Fiber ⇑(map (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1}))))) f)
⊢ counitAppAppImage (map (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1}))))) f) a =
    (ConcreteCategory.hom
        (Y.obj.map (sigmaIncl (map (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1}))))) f) a).op))
      ((ConcreteCategory.hom (g.hom.app S)) ((ConcreteCategory.hom (counitAppApp (unop S) X.obj)) f))

Tactic:
apply presheaf_ext (f.comap (sigmaIncl _ _).hom.hom)

Goal state after:
P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S✝ : CompHausLike P
Y✝ : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝³ : HasProp P PUnit.{u + 1}
f✝ : LocallyConstant (↑S✝.toTop) (Y✝.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g✝ : T ⟶ S✝
X✝ : TopCat
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X Y : Sheaf (coherentTopology (CompHausLike P)) (Type (max u w))
g : X ⟶ Y
this : Preregular (CompHausLike P)
S : (CompHausLike P)ᵒᵖ
f : LocallyConstant (↑(unop S).toTop) (X.obj.obj (op (of P PUnit.{u + 1})))
a : Fiber ⇑(map (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1}))))) f)
⊢ ∀
    (a_1 :
      Fiber
        ⇑(comap
            (TopCat.Hom.hom (sigmaIncl (map (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1}))))) f) a).hom)
            f)),
    (ConcreteCategory.hom
          (Y.obj.map
            (sigmaIncl
                (comap
                  (TopCat.Hom.hom
                    (sigmaIncl (map (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1}))))) f) a).hom)
                  f)
                a_1).op))
        (counitAppAppImage (map (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1}))))) f) a) =
      (ConcreteCategory.hom
          (Y.obj.map
            (sigmaIncl
                (comap
                  (TopCat.Hom.hom
                    (sigmaIncl (map (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1}))))) f) a).hom)
                  f)
                a_1).op))
        ((ConcreteCategory.hom
            (Y.obj.map (sigmaIncl (map (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1}))))) f) a).op))
          ((ConcreteCategory.hom (g.hom.app S)) ((ConcreteCategory.hom (counitAppApp (unop S) X.obj)) f)))
Module: Mathlib.Condensed.Explicit

Goal state before:
pp: A : Type u_1
inst✝² : Category.{v_1, u_1} A
inst✝¹ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X profiniteToCompHaus.op) A
F : Profiniteᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts F
hF : EqualizerCondition F
⊢ IsSheaf (coherentTopology Profinite) F

Tactic:
rw [isSheaf_iff_preservesFiniteProducts_and_equalizerCondition F]
      exact ⟨⟨fun _ ↦ inferInstance⟩, hF⟩

Goal state after:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : Profinite
F✝ F : Profiniteᵒᵖ ⥤ Type (u + 1)
X : Profinite
inst✝ : Finite ↑X.toTop
x✝¹ : Cofan fun x ↦ Profinite.of PUnit.{?u.15 + 1}
x✝ : (fintypeCatAsCofan X).pt ⟶ x✝¹.pt
h : ∀ (j : ↑X.toTop), (fintypeCatAsCofan X).inj j ≫ x✝ = x✝¹.inj j
x : ↑(fintypeCatAsCofan X).pt.toTop
⊢ (ConcreteCategory.hom x✝) x =
    (ConcreteCategory.hom
        (ConcreteCategory.ofHom
          { toFun := fun x ↦ (ConcreteCategory.hom (x✝¹.inj x)) PUnit.unit, continuous_toFun := ⋯ }))
      x

Tactic:
exact CategoryTheory.congr_fun (h x) _

Goal state after:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : LightProfinite
F✝ F : LightProfiniteᵒᵖ ⥤ Type u
X : LightProfinite
inst✝ : Finite ↑X.toTop
x✝¹ : Cofan fun x ↦ LightProfinite.of PUnit.{?u.15 + 1}
x✝ : (fintypeCatAsCofan X).pt ⟶ x✝¹.pt
h : ∀ (j : ↑X.toTop), (fintypeCatAsCofan X).inj j ≫ x✝ = x✝¹.inj j
x : ↑(fintypeCatAsCofan X).pt.toTop
⊢ (ConcreteCategory.hom x✝) x =
    (ConcreteCategory.hom
        (ConcreteCategory.ofHom
          { toFun := fun x ↦ (ConcreteCategory.hom (x✝¹.inj x)) PUnit.unit, continuous_toFun := ⋯ }))
      x

Tactic:
exact CategoryTheory.congr_fun (h x) _

Goal state after:
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst✝⁸] (Z i)
Z_disj : univ.PairwiseDisjoint Z
D : S → Set Y := fun i ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : ⋃ i, D i ⊆ ⋃ i, C i
C_disj : univ.PairwiseDisjoint C
D_cover_univ : univ ⊆ ⋃ i, D i
C_cover_univ : ⋃ i, C i = univ
h_glue : ∀ (i j : S), ∀ x ∈ C i, x ∈ C j → i = j
⊢ f' ∘ liftCover C (fun i x ↦ i) h_glue C_cover_univ = g'

Tactic:
ext y
    -- y is contained in C i for some i
    have hy : y ∈ ⋃ i, C i := by simp [C_cover_univ]
    obtain ⟨i, hi⟩ := mem_iUnion.mp hy
    simpa [liftCover_of_mem hi] using symm (C_subset_D i hi)

Goal state after:
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: X Y S T : Profinite
inst✝² : Finite ↑S.toTop
f : X ⟶ Y
inst✝¹ : Mono f
f' : S ⟶ T
inst✝ : Epi f'
g : X ⟶ S
g' : Y ⟶ T
h_comm : f ≫ g' = g ≫ f'
k_fun : (fun X ↦ ↑X.toTop) Y → (fun X ↦ ↑X.toTop) S
k_cont : Continuous k_fun
h₁ : ⇑(ConcreteCategory.hom f') ∘ k_fun = ⇑(ConcreteCategory.hom g')
h₂ : k_fun ∘ ⇑(ConcreteCategory.hom f) = ⇑(ConcreteCategory.hom g)
a✝ : ↑Y.toTop
⊢ (ConcreteCategory.hom
        (CompHausLike.ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := k_fun, continuous_toFun := k_cont } ≫ f'))
      a✝ =
    (ConcreteCategory.hom g') a✝

Tactic:
simp [← h₁]

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
⊢ ((fun i t ↦ (↑t).1) <$$> u✝ = x ∧ (fun i t ↦ (↑t).2) <$$> u✝ = y) =
    ((fun i x ↦ (↑(f' rr n α i x)).1) <$$> u✝ = x ∧ (fun i x ↦ (↑(f' rr n α i x)).2) <$$> u✝ = y)

Tactic:
congr <;> ext i ⟨x, _⟩ <;> cases i <;> rfl

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

Goal state before:
pp: case none
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
hπ : Function.Surjective π
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
s : S
⊢ ∃ a, (fun x ↦ π ↑x) a = (s, none)

pp: case some
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
hπ : Function.Surjective π
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
s : S
x : X
⊢ ∃ a, (fun x ↦ π ↑x) a = (s, Option.some x)

Tactic:
· obtain ⟨y, hy⟩ := hπ (s, none)
    exact ⟨⟨y, by grind⟩, hy⟩

Goal state after:
case some
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
hπ : Function.Surjective π
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
s : S
x : X
⊢ ∃ a, (fun x ↦ π ↑x) a = (s, Option.some x)
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
α : Type u
x : t' α
⊢ Equiv.traverse eqv pure x = pure x

Tactic:
Equiv.traverse,

Goal state after:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
α : Type u
x : t' α
⊢ ⇑(eqv α) <$> traverse pure ((eqv α).symm x) = pure x
Module: Mathlib.Data.ENat.BigOperators

Goal state before:
pp: α : Type u_1
ι : Type u_2
s : Finset α
f : α → ι → ℕ∞
hf : ∀ (i j : ι), ∃ k, ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
⊢ ∑ a ∈ s, ⨆ i, f a i = ⨆ i, ∑ a ∈ s, f a i

Tactic:
induction s using Finset.cons_induction with

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: case hf
α : Type u
inst✝ : FinEnum α
⊢ Injective ⇑equiv.symm

Tactic:
apply Equiv.injective

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: case e_3
α : Type u
β : α → Type v
inst✝ : IsEmpty α
e : FinEnum α
⊢ equiv ≍ Equiv.equivOfIsEmpty α (Fin 0)

Tactic:
refine heq_of_cast_eq ?_ (Subsingleton.allEq _ _)
      exact congrArg (α ≃ Fin ·) <| card_eq_zero

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: case e_2
α : Type u
β : α → Type v
inst✝ : Unique α
e : FinEnum α
⊢ card α = 1

Tactic:
exact card_eq_one α

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

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

Tactic:
by rw [entries_insert, kerase_of_notMem_keys h]

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

Goal state before:
pp: case mp.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝
⊢ (some y✝).isSome = true

Tactic:
exact rfl

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

Goal state before:
pp: case mpr.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
h'' : x✝ ∈ s₁.entries.keys
⊢ (some y✝).isSome = true

Tactic:
exact rfl

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
f : (x : α) → β x → Bool
s : Finmap β
x✝³ : Bool
x✝² : α
x✝¹ : β x✝²
x✝ : α
⊢ ∀ (b₂ : β x✝), (x✝³ || (f x✝² x✝¹ || f x✝ b₂)) = (x✝³ || (f x✝ b₂ || f x✝² x✝¹))

Tactic:
Bool.or_comm,

Goal state after:
α : Type u
β : α → Type v
f : (x : α) → β x → Bool
s : Finmap β
x✝³ : Bool
x✝² : α
x✝¹ : β x✝²
x✝ : α
⊢ ∀ (b₂ : β x✝), True
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Finmap β
⊢ a ∉ erase a s

Tactic:
by
  rw [mem_erase, not_and_or, not_not]
  left
  rfl

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd₁ : l₁.NodupKeys
p : l₁ ~ l₂
⊢ lookupAll a l₁ = lookupAll a l₂

Tactic:
by
  have nd₂ := (perm_nodupKeys p).mp nd₁
  simp [lookupAll_eq_dlookup, nd₁, nd₂, perm_dlookup a nd₁ p]

Goal state after:
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Multiset (ι →₀ M)
⊢ s.sum.support ⊆ (map Finsupp.support s).sup

Tactic:
induction s using Quot.inductionOn
  simpa only [Multiset.quot_mk_to_coe'', Multiset.sum_coe, Multiset.map_coe, Multiset.sup_coe,
    List.foldr_map] using! List.support_sum_subset _

Goal state after:
Module: Mathlib.Data.Finset.PiInduction

Goal state before:
pp: case intro.a.inr
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hne : (univ.sigma f).Nonempty
⊢ p f

Tactic:
· rcases sigma_nonempty.1 hne with ⟨i, -, hi⟩
    rcases H_ex i (f i) hi with ⟨x, x_mem, hr⟩
    set g := update f i ((f i).erase x) with hg
    clear_value g
    have hx' : x ∉ g i := by
      rw [hg, update_self]
      apply notMem_erase
    rw [show f = update g i (insert x (g i)) by
      rw [hg, update_idem, update_self, insert_erase x_mem, update_eq_self]] at hr ihs ⊢
    clear hg
    rw [update_self, erase_insert hx'] at hr
    refine step _ _ _ hr (ihs (univ.sigma g) ?_ _ rfl)
    rw [ssubset_iff_of_subset (sigma_mono (Subset.refl _) _)]
    exacts [⟨⟨i, x⟩, mem_sigma.2 ⟨mem_univ _, by simp⟩, by simp [hx']⟩,
      (@le_update_iff _ _ _ _ g g i _).2 ⟨subset_insert _ _, fun _ _ ↦ le_rfl⟩]

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

Goal state before:
pp: n : ℕ
⊢ (bif -[n+1].bodd then 1 else 0) + 2 * -[n+1].div2 = -[n.bodd.toNat + 2 * n.div2+1]

Tactic:
dsimp [bodd]

Goal state after:
n : ℕ
⊢ (bif !n.bodd then 1 else 0) + 2 * -[n+1].div2 = -[n.bodd.toNat + 2 * n.div2+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n✝ k i n : ℕ
⊢ Nat.shiftLeft' true m i = Nat.shiftLeft' true m (n + i) >>> n

Tactic:
← Nat.shiftLeft'_sub,

Goal state after:
m n✝ k i n : ℕ
⊢ Nat.shiftLeft' true m i = Nat.shiftLeft' true m (n + i - n)

case a
m n✝ k i n : ℕ
⊢ n ≤ n + i
Module: Mathlib.Data.List.Palindrome

Goal state before:
pp: case nil
α : Type u_1
l : List α
⊢ [].reverse = []

Tactic:
exact rfl

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

Goal state before:
pp: case singleton
α : Type u_1
l : List α
x✝ : α
⊢ [x✝].reverse = [x✝]

Tactic:
exact rfl

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

Goal state before:
pp: case cons_concat
α : Type u_1
l : List α
x✝ : α
l✝ : List α
a✝ : l✝.Palindrome
a_ih✝ : l✝.reverse = l✝
⊢ (x✝ :: (l✝ ++ [x✝])).reverse = x✝ :: (l✝ ++ [x✝])

Tactic:
exact rfl

Goal state after:
case cons_concat
α : Type u_1
l : List α
x✝ : α
l✝ : List α
a✝ : l✝.Palindrome
a_ih✝ : l✝.reverse = l✝
⊢ (x✝ :: (l✝ ++ [x✝])).reverse = x✝ :: (l✝ ++ [x✝])
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
⊢ (u ++ (v ++ w))[j + u.length]? = v[j]?

Tactic:
getElem?_append_right,

Goal state after:
α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
⊢ (v ++ w)[j + u.length - u.length]? = v[j]?

α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
⊢ u.length ≤ j + u.length
Module: Mathlib.Data.Multiset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ #(Finset.Iic s) = ∏ i ∈ s.toFinset, (count i s + 1)

Tactic:
simp_rw [Iic_eq_Icc, card_Icc, bot_eq_zero, toFinset_zero, empty_union, count_zero, tsub_zero]

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

Goal state before:
pp: case inl
q : ℚ
hq : q ≤ 0
⊢ q⁻¹.toNNRat = q.toNNRat⁻¹

Tactic:
rw [toNNRat_eq_zero.mpr hq, inv_zero, toNNRat_eq_zero.mpr (inv_nonpos.mpr hq)]

Goal state after:
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: R : Type u_1
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
r : R
n d : ℕ
h : IsRat r (Int.negOfNat n) d
⊢ ⌈r⌉₊ = ↑0

Tactic:
simp [h.neg_to_eq, div_nonneg]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case mp
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
h : k = (x₁, x₂).1 + p * (x₁, x₂).2
hx : x₁ < n % p + 1 ∧ x₂ < n / p + 1
h' : x₁ < p
⊢ (x₁, x₂).1 % p = x₁ ∧ x₂ = (x₁, x₂).1 / p + (x₁, x₂).2

Tactic:
exact ⟨mod_eq_of_lt h', right_eq_add.mpr (div_eq_of_lt h')⟩

Goal state after:
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: ⊢ [].IsZeckendorfRep

Tactic:
simp [IsZeckendorfRep]

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

Goal state before:
pp: case refine_2
p : ℕ → Prop
n : ℕ
⊢ (p 0 ∧ n = 0 ∨ ∃ (hf : (Set.ofPred p).Finite), #hf.toFinset ≤ n) → nth p n = 0

Tactic:
· rintro (⟨h₀, rfl⟩ | ⟨hf, hle⟩)
    exacts [nth_zero_of_zero h₀, nth_of_card_le hf hle]

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

Goal state before:
pp: case inl.inl
p : ℕ → Prop
k : ℕ
hf : (Set.ofPred p).Finite
n : ℕ
hn : n < #hf.toFinset
h : nth p n < nth p (k + 1)
ha : p (nth p n)
hk : k + 1 < #hf.toFinset
⊢ nth p n ≤ nth p k

Tactic:
rwa [(nth_strictMonoOn hf).lt_iff_lt hn hk, Nat.lt_succ_iff,
        ← (nth_strictMonoOn hf).le_iff_le hn (k.lt_succ_self.trans hk)] at h

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

Goal state before:
pp: case nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ Ordnode α

pp: case node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
· rcases id l with _ | ⟨ls, ll, lx, lr⟩
    · exact ι x
    · rcases id ll with _ | lls
      · rcases lr with _ | ⟨_, _, lrx⟩
        · exact node 2 l x nil
        · exact node 3 (ι lx) lrx ι x
      · rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩
        · exact node 3 ll lx ι x
        · exact
            if lrs < ratio * lls then node (ls + 1) ll lx (node (lrs + 1) lr x nil)
            else
              node (ls + 1) (node (lls + size lrl + 1) ll lx lrl) lrx
                (node (size lrr + 1) lrr x nil)

Goal state after:
case node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Nat.Nth

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

Tactic:
rw [count_eq_card_filter_range, card_eq_zero, filter_eq_empty_iff, nth_zero]

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
⊢ ∀ ⦃x : ℕ⦄, x ∈ range (sInf (Set.ofPred p)) → ¬p x
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
⊢ (count p (nth p n) + if p (nth p n) then 1 else 0) = n + 1

Tactic:
count_nth hn,

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
⊢ (n + if p (nth p n) then 1 else 0) = n + 1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: p : PosNum
⊢ ↑p.bit1 = ZNum.pos p.bit1

Tactic:
have := congr_arg ZNum.bit1 (cast_to_znum p)

Goal state after:
p : PosNum
this : (↑p).bit1 = (ZNum.pos p).bit1
⊢ ↑p.bit1 = ZNum.pos p.bit1
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: case h.right.left
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
u : ↑P { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : P.A
f : P.B a → { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ y = ⟨a, fun i ↦ (↑(f i)).2⟩

Tactic:
rw [← yeq, h]

Goal state after:
case h.right.left
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
u : ↑P { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : P.A
f : P.B a → { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ (fun t ↦ (↑t).2) <$> ⟨a, f⟩ = ⟨a, fun i ↦ (↑(f i)).2⟩
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
n : ZNum
⊢ ↑(ofZNum n) = ↑(↑n).toNat

Tactic:
← cast_to_nat,

Goal state after:
α : Type u_1
inst✝ : AddMonoidWithOne α
n : ZNum
⊢ ↑↑(ofZNum n) = ↑(↑n).toNat
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: case h.right.left
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : ↑P α
u : ↑P fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : P.A
f : P.B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ y = ⟨a, fun i j ↦ (↑(f i j)).2⟩

Tactic:
rw [← yeq, h]

Goal state after:
case h.right.left
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : ↑P α
u : ↑P fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : P.A
f : P.B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ (fun i t ↦ (↑t).2) <$$> ⟨a, f⟩ = ⟨a, fun i j ↦ (↑(f i j)).2⟩
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
n : ℕ
x : CofixA F n.succ
y : CofixA F (n.succ + 1)
i : F.B (head' x)
j : F.B (head' y)
h₀ : i ≍ j
h₁ : Agree x y
⊢ Agree (children' x i) (children' y j)

Tactic:
obtain - | ⟨_, _, hagree⟩ := h₁; cases h₀
  apply hagree

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

Goal state before:
pp: case succ.intro
F : PFunctor.{uA, uB}
n : ℕ
n_ih : ∀ (x : CofixA F n) (y : CofixA F n.succ), Agree x y → truncate y = x
a✝ : F.A
f : F.B a✝ → CofixA F n
y : F.B a✝ → CofixA F (n + 1)
h₁ : ∀ (i : F.B a✝), Agree (f i) (y i)
⊢ (CofixA.intro a✝ fun x ↦ truncate (y x)) = CofixA.intro a✝ f

Tactic:
congr with y

Goal state after:
case succ.intro
F : PFunctor.{uA, uB}
n : ℕ
n_ih : ∀ (x : CofixA F n) (y : CofixA F n.succ), Agree x y → truncate y = x
a✝ : F.A
f : F.B a✝ → CofixA F n
y✝ : F.B a✝ → CofixA F (n + 1)
h₁ : ∀ (i : F.B a✝), Agree (f i) (y✝ i)
y : F.B a✝
⊢ truncate (y✝ y) = f y
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case bit1
d n : PosNum
q r : Num
IH : ↑(q, r).2 + ↑d * ↑(q, r).1 = ↑n ∧ ↑(q, r).2 < ↑d
⊢ ↑(match (q, r) with
            | (q, r₁) => d.divModAux q r₁.bit1).2 +
        ↑d *
          ↑(match (q, r) with
              | (q, r₁) => d.divModAux q r₁.bit1).1 =
      ↑n.bit1 ∧
    ↑(match (q, r) with
          | (q, r₁) => d.divModAux q r₁.bit1).2 <
      ↑d

Tactic:
simp only at IH ⊢

Goal state after:
case bit1
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ ↑(d.divModAux q r.bit1).2 + ↑d * ↑(d.divModAux q r.bit1).1 = ↑n.bit1 ∧ ↑(d.divModAux q r.bit1).2 < ↑d
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case bit0
d n : PosNum
q r : Num
IH : ↑(q, r).2 + ↑d * ↑(q, r).1 = ↑n ∧ ↑(q, r).2 < ↑d
⊢ ↑(match (q, r) with
            | (q, r₁) => d.divModAux q r₁.bit0).2 +
        ↑d *
          ↑(match (q, r) with
              | (q, r₁) => d.divModAux q r₁.bit0).1 =
      ↑n.bit0 ∧
    ↑(match (q, r) with
          | (q, r₁) => d.divModAux q r₁.bit0).2 <
      ↑d

Tactic:
simp only at IH ⊢

Goal state after:
case bit0
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ ↑(d.divModAux q r.bit0).2 + ↑d * ↑(d.divModAux q r.bit0).1 = ↑n.bit0 ∧ ↑(d.divModAux q r.bit0).2 < ↑d