mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: ⊢ ∀ {X Y : LightDiagram} (f : X ⟶ Y),
    (lightDiagramToLightProfinite ⋙ lightProfiniteToLightDiagram).map f ≫
        (lightDiagramToProfinite.preimageIso
            (Iso.refl
              (lightDiagramToProfinite.obj
                ((lightDiagramToLightProfinite ⋙ lightProfiniteToLightDiagram).obj Y)))).hom =
      (lightDiagramToProfinite.preimageIso
            (Iso.refl
              (lightDiagramToProfinite.obj
                ((lightDiagramToLightProfinite ⋙ lightProfiniteToLightDiagram).obj X)))).hom ≫
        (𝟭 LightDiagram).map f

Tactic:
intro _

Goal state after:
X✝ : LightDiagram
⊢ ∀ {Y : LightDiagram} (f : X✝ ⟶ Y),
    (lightDiagramToLightProfinite ⋙ lightProfiniteToLightDiagram).map f ≫
        (lightDiagramToProfinite.preimageIso
            (Iso.refl
              (lightDiagramToProfinite.obj
                ((lightDiagramToLightProfinite ⋙ lightProfiniteToLightDiagram).obj Y)))).hom =
      (lightDiagramToProfinite.preimageIso
            (Iso.refl
              (lightDiagramToProfinite.obj
                ((lightDiagramToLightProfinite ⋙ lightProfiniteToLightDiagram).obj X✝)))).hom ≫
        (𝟭 LightDiagram).map f
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case refine_3.refine_2.mpr
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j, ∃ V ∈ {W | IsClopen W}, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J := fun s ↦ Exists.choose ⋯
V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s ↦ ⋯.choose
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i)
hsU : U ⊆ ⋃ i, (fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ i ∈ G, ⇑(ConcreteCategory.hom (C.π.app (j i))) ⁻¹' V i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs ↦ ⋯.some
W : ↑S → Set ↑(F.obj j0).toTop :=
  fun s ↦ if hs : s ∈ G then ⇑(ConcreteCategory.hom (F.map (f s hs))) ⁻¹' V s else Set.univ
x : ↑C.pt.toTop
hx :
  x ∈
    ⇑(ConcreteCategory.hom (C.π.app j0)) ⁻¹'
      ⋃ s ∈ G, if h : s ∈ G then ⇑(ConcreteCategory.hom (F.map (f s ⋯))) ⁻¹' V s else Set.univ
⊢ x ∈ U

Tactic:
Set.preimage_iUnion,

Goal state after:
case refine_3.refine_2.mpr
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j, ∃ V ∈ {W | IsClopen W}, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J := fun s ↦ Exists.choose ⋯
V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s ↦ ⋯.choose
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i)
hsU : U ⊆ ⋃ i, (fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ i ∈ G, ⇑(ConcreteCategory.hom (C.π.app (j i))) ⁻¹' V i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs ↦ ⋯.some
W : ↑S → Set ↑(F.obj j0).toTop :=
  fun s ↦ if hs : s ∈ G then ⇑(ConcreteCategory.hom (F.map (f s hs))) ⁻¹' V s else Set.univ
x : ↑C.pt.toTop
hx :
  x ∈
    ⋃ i ∈ G,
      ⇑(ConcreteCategory.hom (C.π.app j0)) ⁻¹'
        if h : i ∈ G then ⇑(ConcreteCategory.hom (F.map (f i ⋯))) ⁻¹' V i else Set.univ
⊢ x ∈ U
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✝
inst✝¹ : HasExplicitFiniteCoproducts P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝ : PreservesFiniteProducts Y
S T : (CompHausLike P)ᵒᵖ
g : S ⟶ T
f : (functorToPresheaves.obj (Y.obj (op (of P PUnit.{u + 1})))).obj S
a : Fiber ⇑(comap (TopCat.Hom.hom g.unop.hom) f)
⊢ (ConcreteCategory.hom (Y.map (sigmaIncl (comap (TopCat.Hom.hom g.unop.hom) f) a).op))
      ((ConcreteCategory.hom (counitAppApp (unop T) Y)) (comap (TopCat.Hom.hom g.unop.hom) f)) =
    (ConcreteCategory.hom (Y.map (sigmaIncl (comap (TopCat.Hom.hom g.unop.hom) f) a).op))
      ((ConcreteCategory.hom (Y.map g)) ((ConcreteCategory.hom (counitAppApp (unop S) Y)) f))

Tactic:
incl_of_counitAppApp,

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✝
inst✝¹ : HasExplicitFiniteCoproducts P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝ : PreservesFiniteProducts Y
S T : (CompHausLike P)ᵒᵖ
g : S ⟶ T
f : (functorToPresheaves.obj (Y.obj (op (of P PUnit.{u + 1})))).obj S
a : Fiber ⇑(comap (TopCat.Hom.hom g.unop.hom) f)
⊢ counitAppAppImage (comap (TopCat.Hom.hom g.unop.hom) f) a =
    (ConcreteCategory.hom (Y.map (sigmaIncl (comap (TopCat.Hom.hom g.unop.hom) f) a).op))
      ((ConcreteCategory.hom (Y.map g)) ((ConcreteCategory.hom (counitAppApp (unop S) Y)) f))
Module: Mathlib.Condensed.EffectiveEpi

Goal state before:
pp: X✝ Y✝ : CompHaus
f : X✝ ⟶ Y✝
hf : Epi f
S : CompHaus
g : (compHausToCondensed.obj Y✝).obj.obj (Opposite.op S)
y : (fun X ↦ ↑X.toTop) S
⊢ ∃ a, (ConcreteCategory.hom (pullback.snd f g.down)) a = y

Tactic:
CompHaus.epi_iff_surjective

Goal state after:
X✝ Y✝ : CompHaus
f : X✝ ⟶ Y✝
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
S : CompHaus
g : (compHausToCondensed.obj Y✝).obj.obj (Opposite.op S)
y : ↑S.toTop
⊢ ∃ a, (ConcreteCategory.hom (pullback.snd f g.down)) a = y
Module: Mathlib.Condensed.Light.Epi

Goal state before:
pp: n✝ : ℕ
R : Type u
inst✝¹ : Ring R
M N : ℕ → LightCondMod R
f : (n : ℕ) → M n ⟶ N n
inst✝ : ∀ (n : ℕ), Epi (f n)
n : ℕ
⊢ Epi ((Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op)

Tactic:
by
    simp only [Nat.succ_eq_add_one, Functor.ofOpSequence_obj, homOfLE_leOfHom,
      Functor.ofOpSequence_map_homOfLE_succ]
    infer_instance

Goal state after:
Module: Mathlib.Control.Bitraversable.Lemmas

Goal state before:
pp: t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β₀ β₁ β₂ : Type u
g : β₀ → F β₁
g' : β₁ → G β₂
x : t α β₀
⊢ Comp.mk (tsnd g' <$> tsnd g x) = tsnd (Comp.mk ∘ map g' ∘ g) x

Tactic:
rw [← comp_bitraverse]
  simp only [Function.comp_def, map_pure]
  rfl

Goal state after:
Module: Mathlib.Control.Bitraversable.Lemmas

Goal state before:
pp: t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
inst✝ : LawfulBitraversable t
α α' β : Type u
f : α → α'
x : t α β
⊢ tfst (pure ∘ f) x = pure (fst f x)

Tactic:
by
  apply bitraverse_eq_bimap_id

Goal state after:
Module: Mathlib.Control.Bitraversable.Lemmas

Goal state before:
pp: t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
inst✝ : LawfulBitraversable t
α β β' : Type u
f : β → β'
x : t α β
⊢ tsnd (pure ∘ f) x = pure (snd f x)

Tactic:
by
  apply bitraverse_eq_bimap_id

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 (α ::: β)
⊢ f' rr n α ⊚ g' rr n α = TypeVec.id

Tactic:
ext i ⟨x, _⟩ : 2

Goal state after:
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 (α ::: β)
i : Fin2 (n + 1)
x : (α ::: β) i × (α ::: β) i
property✝ : α.RelLast rr x.1 x.2
⊢ (f' rr n α ⊚ g' rr n α) i ⟨x, property✝⟩ = TypeVec.id i ⟨x, property✝⟩
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
n : ↑ℕ∪{∞}.toTop
⊢ Continuous fun x ↦ ↑x n

Tactic:
refine (continuous_apply _).comp ?_

Goal state after:
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
n : ↑ℕ∪{∞}.toTop
⊢ Continuous Subtype.val
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
f : Filter α
F : f.Realizer
⊢ f ≠ ⊥ ↔ ∀ (a : F.σ), (F.F.f a).Nonempty

Tactic:
by
  rw [not_iff_comm, ← le_bot_iff, F.le_iff Realizer.bot, not_forall]
  simp only [Set.not_nonempty_iff_eq_empty]
  exact ⟨fun ⟨x, e⟩ _ ↦ ⟨x, le_of_eq e⟩, fun h ↦
    let ⟨x, h⟩ := h ()
    ⟨x, le_bot_iff.1 h⟩⟩

Goal state after:
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) l
b : Bool
⊢ count (!b) l ≤ count b l + 1

Tactic:
cases l
  · exact zero_le
  grind [hl.count_not_cons]

Goal state after:
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: case neg.nil
b : Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) []
h2 : ¬Even [].length
⊢ 2 * count b [] =
    if Even [].length then [].length else if (some b == [].head?) = true then [].length + 1 else [].length - 1

Tactic:
exact (h2 .zero).elim

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m < n
v : (i : Fin n) → α i
i : Fin m.succ
⊢ take m.succ h v i = snoc (take m ⋯ v) (v ⟨m, h⟩) i

Tactic:
induction m with
  | zero =>
    have h' : i = 0 := by ext; simp
    subst h'
    simp [take, snoc, castLE]
  | succ m _ =>
    induction i using reverseInduction with
    | last => simp [take, snoc]; congr
    | cast i _ => simp

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin n
hi : ↑i ≥ m
x : α i
j : Fin m
⊢ take m h (update v i x) j = take m h v j

Tactic:
have : castLE h j ≠ i := by
    refine ne_of_val_ne ?_
    simp only [val_castLE]
    exact Nat.ne_of_lt (lt_of_lt_of_le j.isLt hi)

Goal state after:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin n
hi : ↑i ≥ m
x : α i
j : Fin m
this : castLE h j ≠ i
⊢ take m h (update v i x) j = take m h v j
Module: Mathlib.Data.Finmap

Goal state before:
pp: case mk
α : Type u
β : α → Type v
C : Finmap β → Prop
H : ∀ (a : AList β), C ⟦a⟧
entries✝ : Multiset (Sigma β)
a : List (Sigma β)
h : Multiset.NodupKeys (Quot.mk (⇑(isSetoid (Sigma β))) a)
⊢ C { entries := Quot.mk (⇑(isSetoid (Sigma β))) a, nodupKeys := h }

Tactic:
exact H ⟨a, h⟩

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

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
l₁ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ (l₁.kunion l₂).keys ↔ a ∈ l₁.keys ∨ a ∈ l₂.keys
l₂ : List (Sigma β)
⊢ a ∈ ((s :: l₁).kunion l₂).keys ↔ a ∈ (s :: l₁).keys ∨ a ∈ l₂.keys

Tactic:
by_cases h : a = s.1

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
l₁ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ (l₁.kunion l₂).keys ↔ a ∈ l₁.keys ∨ a ∈ l₂.keys
l₂ : List (Sigma β)
h : a = s.fst
⊢ a ∈ ((s :: l₁).kunion l₂).keys ↔ a ∈ (s :: l₁).keys ∨ a ∈ l₂.keys

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
l₁ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ (l₁.kunion l₂).keys ↔ a ∈ l₁.keys ∨ a ∈ l₂.keys
l₂ : List (Sigma β)
h : ¬a = s.fst
⊢ a ∈ ((s :: l₁).kunion l₂).keys ↔ a ∈ (s :: l₁).keys ∨ a ∈ l₂.keys
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
l : List (Sigma β)
⊢ (kerase a (s :: tail✝)).kunion (kerase a l) = kerase a ((s :: tail✝).kunion l)

Tactic:
by_cases h : a = s.1

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
l : List (Sigma β)
h : a = s.fst
⊢ (kerase a (s :: tail✝)).kunion (kerase a l) = kerase a ((s :: tail✝).kunion l)

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
l : List (Sigma β)
h : ¬a = s.fst
⊢ (kerase a (s :: tail✝)).kunion (kerase a l) = kerase a ((s :: tail✝).kunion l)
Module: Mathlib.Data.Holor

Goal state before:
pp: case refine_2
α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
⊢ ∀ (a : β) (s : Finset β),
    a ∉ s →
      ∑ x ∈ s, (f x).slice i hid = (∑ x ∈ s, f x).slice i hid →
        ∑ x ∈ insert a s, (f x).slice i hid = (∑ x ∈ insert a s, f x).slice i hid

Tactic:
intro _

Goal state after:
case refine_2
α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
a✝ : β
⊢ ∀ (s : Finset β),
    a✝ ∉ s →
      ∑ x ∈ s, (f x).slice i hid = (∑ x ∈ s, f x).slice i hid →
        ∑ x ∈ insert a✝ s, (f x).slice i hid = (∑ x ∈ insert a✝ s, f x).slice i hid
Module: Mathlib.Data.Int.Bitwise

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

Tactic:
rw [show (cond (bodd n) 1 0 : ℤ) = (cond (bodd n) 1 0 : ℕ) by cases bodd n <;> rfl]

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

Goal state before:
pp: case ofNat.ofNat
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (bitwise f (ofNat a✝¹) (ofNat a✝)).testBit k = f ((ofNat a✝¹).testBit k) ((ofNat a✝).testBit k)

Tactic:
simp only [testBit, bitwise, natBitwise]

Goal state after:
case ofNat.ofNat
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (match bif f false false then -[Nat.bitwise (fun x y ↦ !f x y) a✝¹ a✝+1] else ↑(Nat.bitwise f a✝¹ a✝), k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (a✝¹.testBit k) (a✝.testBit k)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.negSucc
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (bitwise f (ofNat a✝¹) -[a✝+1]).testBit k = f ((ofNat a✝¹).testBit k) (-[a✝+1].testBit k)

Tactic:
simp only [testBit, bitwise, natBitwise]

Goal state after:
case ofNat.negSucc
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (match
      bif f false !false then -[Nat.bitwise (fun x y ↦ !f x !y) a✝¹ a✝+1] else ↑(Nat.bitwise (fun x y ↦ f x !y) a✝¹ a✝),
      k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (a✝¹.testBit k) !a✝.testBit k
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.ofNat
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (bitwise f -[a✝¹+1] (ofNat a✝)).testBit k = f (-[a✝¹+1].testBit k) ((ofNat a✝).testBit k)

Tactic:
simp only [testBit, bitwise, natBitwise]

Goal state after:
case negSucc.ofNat
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (match
      bif f (!false) false then -[Nat.bitwise (fun x y ↦ !f (!x) y) a✝¹ a✝+1]
      else ↑(Nat.bitwise (fun x y ↦ f (!x) y) a✝¹ a✝),
      k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (!a✝¹.testBit k) (a✝.testBit k)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.negSucc
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (bitwise f -[a✝¹+1] -[a✝+1]).testBit k = f (-[a✝¹+1].testBit k) (-[a✝+1].testBit k)

Tactic:
simp only [testBit, bitwise, natBitwise]

Goal state after:
case negSucc.negSucc
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (match
      bif f (!false) !false then -[Nat.bitwise (fun x y ↦ !f (!x) !y) a✝¹ a✝+1]
      else ↑(Nat.bitwise (fun x y ↦ f (!x) !y) a✝¹ a✝),
      k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (!a✝¹.testBit k) !a✝.testBit k
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑b - (↑(v % r) + ↑r * ↑(v / r))) / ↑r⌉ - ⌈(↑0 - (↑(v % r) + ↑r * ↑(v / r))) / ↑r⌉ = ?m.91

Tactic:
simp_rw [← sub_sub, sub_div (_ - _), mul_div_cancel_left₀ _ hr'.ne',
      Int.ceil_sub_natCast]

Goal state after:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑b - ↑(v % r)) / ↑r⌉ - ↑(v / r) - (⌈(↑0 - ↑(v % r)) / ↑r⌉ - ↑(v / r)) = ?m.91
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case cons
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : dropWhile p xs = [] ↔ ∀ (x : α), x ∈ xs → p x = true
⊢ dropWhile p (x :: xs) = [] ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true

Tactic:
| cons x xs IH =>

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

Goal state before:
pp: case cons
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : takeWhile p xs = xs ↔ ∀ (x : α), x ∈ xs → p x = true
⊢ takeWhile p (x :: xs) = x :: xs ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true

Tactic:
| cons x xs IH =>

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

Goal state before:
pp: case cons
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : takeWhile p xs = [] ↔ ∀ (hl : 0 < xs.length), ¬p (xs.get ⟨0, hl⟩) = true
⊢ takeWhile p (x :: xs) = [] ↔ ∀ (hl : 0 < (x :: xs).length), ¬p ((x :: xs).get ⟨0, hl⟩) = true

Tactic:
| cons x xs IH =>

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

Goal state before:
pp: case false
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x ↦ !p x) tail).head?
phh : false = p head
phh' : ¬p head = true
⊢ find? p tail = (dropWhile (fun x ↦ !p x) tail).head?

pp: case false
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x ↦ !p x) tail).head?
phh : false = p head
phh' : ¬p head = true
⊢ (!p head) = true

Tactic:
· exact hi

Goal state after:
case false
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x ↦ !p x) tail).head?
phh : false = p head
phh' : ¬p head = true
⊢ (!p head) = true
Module: Mathlib.Data.List.DropRight

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

Tactic:
simp_rw [rdropWhile]
  rw [getLast_reverse, head_dropWhile_not p]
  simp

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

Goal state before:
pp: n m l a : ℕ
⊢ n ≤ a → a < m → m ≤ a → l ≤ a

Tactic:
intro _

Goal state after:
n m l a : ℕ
a✝ : n ≤ a
⊢ a < m → m ≤ a → l ≤ a
Module: Mathlib.Data.List.ModifyLast

Goal state before:
pp: case cons
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ [] ++ [head✝] ++ modifyLast.go f (tl ++ [a]) #[] = head✝ :: (tl ++ [f a])

Tactic:
nil_append,

Goal state after:
case cons
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ [head✝] ++ modifyLast.go f (tl ++ [a]) #[] = head✝ :: (tl ++ [f a])
Module: Mathlib.Data.List.ModifyLast

Goal state before:
pp: case cons
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ head✝ :: ([] ++ modifyLast.go f (tl ++ [a]) #[]) = head✝ :: (tl ++ [f a])

Tactic:
nil_append,

Goal state after:
case cons
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ head✝ :: modifyLast.go f (tl ++ [a]) #[] = head✝ :: (tl ++ [f a])
Module: Mathlib.Data.List.ModifyLast

Goal state before:
pp: case cons.cons
α : Type u_1
f : α → α
l₁ : List α
hd hd' : α
tl' : List α
x✝ : hd :: hd' :: tl' ≠ []
⊢ modifyLast f (l₁ ++ [hd] ++ hd' :: tl') = l₁ ++ modifyLast f ([] ++ [hd] ++ hd' :: tl')

Tactic:
nil_append,

Goal state after:
case cons.cons
α : Type u_1
f : α → α
l₁ : List α
hd hd' : α
tl' : List α
x✝ : hd :: hd' :: tl' ≠ []
⊢ modifyLast f (l₁ ++ [hd] ++ hd' :: tl') = l₁ ++ modifyLast f ([hd] ++ hd' :: tl')
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m : ℕ
hnm : n < m
⊢ filter (fun x ↦ decide (x ≤ n)) (Ico n m) = [n]

Tactic:
rw [← filter_lt_of_succ_bot hnm]
  exact filter_congr fun _ _ => by
    simpa using Nat.lt_succ_iff.symm

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

Goal state before:
pp: case h_2.inl
α : Type u_1
r : α → α → Bool
b : α
l : List α
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
x✝ : Bool
heq✝ : r a b = false
IH :
  ∀ {a_1 : α} {g_1 : List α},
    (∀ (b : α), b ∈ g_1.head? → r b a_1 = true) →
      IsChain (fun y x ↦ r x y = true) g_1 →
        g.reverse ++ [a] ∈ splitBy.loop r l a_1 g_1 [] → IsChain (fun x y ↦ r x y = true) (g.reverse ++ [a])
⊢ IsChain (fun b a ↦ r a b = true) ([] ++ [a] ++ g.reverse.reverse)

Tactic:
nil_append,

Goal state after:
case h_2.inl
α : Type u_1
r : α → α → Bool
b : α
l : List α
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
x✝ : Bool
heq✝ : r a b = false
IH :
  ∀ {a_1 : α} {g_1 : List α},
    (∀ (b : α), b ∈ g_1.head? → r b a_1 = true) →
      IsChain (fun y x ↦ r x y = true) g_1 →
        g.reverse ++ [a] ∈ splitBy.loop r l a_1 g_1 [] → IsChain (fun x y ↦ r x y = true) (g.reverse ++ [a])
⊢ IsChain (fun b a ↦ r a b = true) ([a] ++ g.reverse.reverse)
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: case right
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ↑x ≤ ↑↑⌈x⌉₊

Tactic:
rw [Int.cast_natCast, NNRat.cast_le_natCast]
    exact Nat.le_ceil _

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case inr
a b n : ℕ
hn : n ≠ 0
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b

Tactic:
obtain rfl | hb := eq_or_ne b 0

Goal state after:
case inr.inl
a n : ℕ
hn : n ≠ 0
⊢ a ^ n ∣ 0 ↔ a ∣ n.floorRoot 0

case inr.inr
a b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: n : ℕ
hn : n ≠ 0
a : ℕ
⊢ n.ceilRoot (a ^ n) = a

Tactic:
simp [ceilRoot_def, pos_iff_ne_zero.2, hn]; split_ifs <;> simp [*]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case inr
a b n : ℕ
hn : n ≠ 0
ha : a ≠ 0
⊢ a ∣ b ^ n ↔ n.ceilRoot a ∣ b

Tactic:
obtain rfl | hb := eq_or_ne b 0

Goal state after:
case inr.inl
a n : ℕ
hn : n ≠ 0
ha : a ≠ 0
⊢ a ∣ 0 ^ n ↔ n.ceilRoot a ∣ 0

case inr.inr
a b n : ℕ
hn : n ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ a ∣ b ^ n ↔ n.ceilRoot a ∣ b
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n p : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
h : ∀ i ∈ Icc 1 (n - 1), ↑(n.choose i) ≡ 0 [ZMOD ↑p]
⊢ n = p ^ multiplicity p n

Tactic:
by_contra! hn₀

Goal state after:
n p : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
h : ∀ i ∈ Icc 1 (n - 1), ↑(n.choose i) ≡ 0 [ZMOD ↑p]
hn₀ : n ≠ p ^ multiplicity p n
⊢ False
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n : ℕ
hn : 1 < n
hpn : (Icc 1 (n - 1)).gcd n.choose ≠ 1
q : ℕ
hq : Nat.Prime q
h : q ∣ (Icc 1 (n - 1)).gcd n.choose
⊢ IsPrimePow n

Tactic:
simp_rw [Finset.dvd_gcd_iff, ← modEq_zero_iff_dvd] at h

Goal state after:
n : ℕ
hn : 1 < n
hpn : (Icc 1 (n - 1)).gcd n.choose ≠ 1
q : ℕ
hq : Nat.Prime q
h : ∀ b ∈ Icc 1 (n - 1), n.choose b ≡ 0 [MOD q]
⊢ IsPrimePow n
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.intro
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (x.approx 1)
ch : F.B (head' (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch
a : F.B (head' (x.approx 1))
⊢ ∀ (a'' : F.B (head' (CofixA.intro (head' (x.approx 1)) ch))),
    a ≍ a'' → children' (CofixA.intro (head' (x.approx 1)) ch) a'' = ch a

Tactic:
intro _

Goal state after:
case succ.intro
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (x.approx 1)
ch : F.B (head' (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch
a : F.B (head' (x.approx 1))
a''✝ : F.B (head' (CofixA.intro (head' (x.approx 1)) ch))
⊢ a ≍ a''✝ → children' (CofixA.intro (head' (x.approx 1)) ch) a''✝ = ch a
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.hy
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ Agree' i x y

Tactic:
rw [← agree_iff_agree', i_ih]
      apply y.consistent

Goal state after: