mathlib-initiative/mathlib-tactics huggingface dataset:
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) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b ↦ if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) gg
ι : α → α → Fin 2 := fun a b ↦ if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f ↦ if h : ∃ a, ι a = f then h.choose else default
x : ↑C.pt.toTop
h1 : ι (f x) = gg ((ConcreteCategory.hom (C.π.app j)) x)
h2 : ∃ a, ι a = gg ((ConcreteCategory.hom (C.π.app j)) x)
⊢ f x = if h : ∃ a, ι a = gg ((TopCat.Hom.hom (C.π.app j).hom) x) then h.choose else default

Tactic:
dif_pos

Goal state after:
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) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b ↦ if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) gg
ι : α → α → Fin 2 := fun a b ↦ if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f ↦ if h : ∃ a, ι a = f then h.choose else default
x : ↑C.pt.toTop
h1 : ι (f x) = gg ((ConcreteCategory.hom (C.π.app j)) x)
h2 : ∃ a, ι a = gg ((ConcreteCategory.hom (C.π.app j)) x)
⊢ f x = Exists.choose ?hc

case hc
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) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b ↦ if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) gg
ι : α → α → Fin 2 := fun a b ↦ if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f ↦ if h : ∃ a, ι a = f then h.choose else default
x : ↑C.pt.toTop
h1 : ι (f x) = gg ((ConcreteCategory.hom (C.π.app j)) x)
h2 : ∃ a, ι a = gg ((ConcreteCategory.hom (C.π.app j)) x)
⊢ ∃ a, ι a = gg ((TopCat.Hom.hom (C.π.app j).hom) x)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: S : Finset Λ'
q : Λ'
K : Finset Λ'
H₁ : Λ'.Supports S q
H₃ : K ⊆ S → Supports K S
H₂ : trStmts₁ q ⊆ S ∧ K ⊆ S
⊢ Supports (trStmts₁ q ∪ K) S

Tactic:
exact supports_union.2 ⟨trStmts₁_supports H₁ H₂.1, H₃ H₂.2⟩

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

Goal state before:
pp: case left
I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
e : I ≌ ULiftHom (ULift.{w, u} I) := ⋯
⊢ ∀ (d : StructuredArrow c.pt toProfinite), ∃ c_1, Nonempty ((e.inverse ⋙ functor c).obj c_1 ⟶ d)

Tactic:
intro ⟨_, X, (f : c.pt ⟶ _)⟩
    obtain ⟨i, g, h⟩ := exists_hom c hc f
    exact ⟨⟨i⟩, ⟨StructuredArrow.homMk g h.symm⟩⟩

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case comp
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H H' : contSupp (Cont'.comp f k) ⊆ S
⊢ Supports (contSupp (Cont'.comp f k)) S

Tactic:
rw [contSupp_comp] at H'

Goal state after:
case comp
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.comp f k) ⊆ S
H' : codeSupp f k ⊆ S
⊢ Supports (contSupp (Cont'.comp f k)) S
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: case e_a
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
f :
  LocallyConstant (↑(toProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X) PUnit.{u + 1})))
x : Function.Fiber ⇑f
this : Finite ↑(fiber f x).toTop
y : ↑(fiber f x).toTop
⊢ (ConcreteCategory.hom (X.map (CompHausLike.const (Profinite.of PUnit.{u + 1}) y ≫ sigmaIncl f x).op))
      ((ConcreteCategory.hom (isoFinYonedaComponents X (Profinite.of (Opposite.unop Y).obj)).inv) ⇑f) =
    (ConcreteCategory.hom
        (X.map (CompHausLike.const (Profinite.of PUnit.{u + 1}) y ≫ CompHausLike.isTerminalPUnit.from (fiber f x)).op))
      (Function.Fiber.image (⇑f) x)

Tactic:
show (Profinite.of PUnit.{u + 1}).const y ≫
    IsTerminal.from _ (fiber.{u, u + 1} f x) = 𝟙 _ from rfl

Goal state after:
case e_a
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
f :
  LocallyConstant (↑(toProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X) PUnit.{u + 1})))
x : Function.Fiber ⇑f
this : Finite ↑(fiber f x).toTop
y : ↑(fiber f x).toTop
⊢ (ConcreteCategory.hom (X.map (CompHausLike.const (Profinite.of PUnit.{u + 1}) y ≫ sigmaIncl f x).op))
      ((ConcreteCategory.hom (isoFinYonedaComponents X (Profinite.of (Opposite.unop Y).obj)).inv) ⇑f) =
    (ConcreteCategory.hom (X.map (𝟙 (Profinite.of PUnit.{u + 1})).op)) (Function.Fiber.image (⇑f) x)
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
P : LightCondMod R
x✝ : InternallyProjective P
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : P ⊗ (free R).obj S.toCondensed ⟶ B
h : isInternallyProjective P
hh :
  ∃ S' φ,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
      ∃ x,
        (ConcreteCategory.hom (((ihom P).map e).hom.app (Opposite.op S'))) x =
          (ConcreteCategory.hom ((P ⟹ B).obj.map (Opposite.op φ))) ((ihomPoints R P B S).symm g)
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ g = g' ≫ e

Tactic:
obtain ⟨S', π, hπ, g', hh⟩ := hh

Goal state after:
case refine_1
R : Type u
inst✝ : CommRing R
P : LightCondMod R
x✝ : InternallyProjective P
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : P ⊗ (free R).obj S.toCondensed ⟶ B
h : isInternallyProjective P
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : ↑((P ⟹ A).obj.obj (Opposite.op S'))
hh :
  (ConcreteCategory.hom (((ihom P).map e).hom.app (Opposite.op S'))) g' =
    (ConcreteCategory.hom ((P ⟹ B).obj.map (Opposite.op π))) ((ihomPoints R P B S).symm g)
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ g = g' ≫ e
Module: Mathlib.Data.Nat.Upto

Goal state before:
pp: p : ℕ → Prop
x : ℕ
h : p x
⊢ WellFounded (Upto.GT p)

Tactic:
suffices Upto.GT p = InvImage (· < ·) fun y : Nat.Upto p => x - y.val by
      rw [this]
      exact (measure _).wf

Goal state after:
p : ℕ → Prop
x : ℕ
h : p x
⊢ Upto.GT p = InvImage (fun x1 x2 ↦ x1 < x2) fun y ↦ x - ↑y
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: α : Type u_1
x : Option α
⊢ Option.traverse pure x = pure x

Tactic:
cases x <;> rfl

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: α β : Type u_1
f : α → β
x : Option α
⊢ Option.traverse (pure ∘ f) x = pure (f <$> x)

Tactic:
cases x <;> rfl

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: σ α : Type u_1
x : σ ⊕ α
⊢ Sum.traverse pure x = x

Tactic:
cases x <;> rfl

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
hij : i ≤ 0
⊢ approx (⇑f) i ≤ approx (⇑f) 0

Tactic:
cases hij; exact le_rfl

Goal state after:
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
x✝ : Set α
⊢ x✝ ∈
      { f := Subtype.val, pt := ⟨univ, ⋯⟩,
            inf := fun x x_1 ↦
              match x with
              | ⟨val, h₁⟩ =>
                match x_1 with
                | ⟨val_1, h₂⟩ => ⟨val ∩ val_1, ⋯⟩,
            inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ f.sets

Tactic:
by simp [exists_mem_subset_iff]

Goal state after:
Module: Mathlib.Data.Fin.Init

Goal state before:
pp: k : ℕ
inst✝ : NeZero k
a : Fin k
⊢ a ^^^ a = 0

Tactic:
by
  grind [Fin.xor_val, Nat.zero_mod]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
γ : Type ?u.51
s₁ s₂ : Finmap β
f : AList β → AList β → γ
H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries ~ a₂.entries → b₁.entries ~ b₂.entries → f a₁ b₁ = f a₂ b₂
a₁ a₂ : AList β
p : a₁.entries ~ a₂.entries
⊢ s₂.liftOn (f a₁) ⋯ = s₂.liftOn (f a₂) ⋯

Tactic:
have H' : f a₁ = f a₂ := funext fun _ => H _ _ _ _ p (Perm.refl _)
    simp only [H']

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
s t : Finset α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

Tactic:
by_cases hs : s.Nonempty

Goal state after:
case pos
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
s t : Finset α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : s.Nonempty
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

case neg
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
s t : Finset α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : ¬s.Nonempty
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case h_fst
R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : ¬Nonempty ↑S'.toTop
h : IsEmpty (↑S'.toTop ⊗ ↑ℕ∪{∞}.toTop)
x : ↑(S' ⊗ ℕ∪{∞}).toTop
⊢ (ConcreteCategory.hom
        ((ConcreteCategory.ofHom { toFun := fun x ↦ h.elim x, continuous_toFun := ⋯ } ≫ π') ≫ fst S' ℕ∪{∞}))
      x =
    (ConcreteCategory.hom (𝟙 (S' ⊗ ℕ∪{∞}) ≫ fst S' ℕ∪{∞})) x

Tactic:
exact h.elim x

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

Goal state before:
pp: case h_snd
R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : ¬Nonempty ↑S'.toTop
h : IsEmpty (↑S'.toTop ⊗ ↑ℕ∪{∞}.toTop)
x : ↑(S' ⊗ ℕ∪{∞}).toTop
⊢ (ConcreteCategory.hom
        ((ConcreteCategory.ofHom { toFun := fun x ↦ h.elim x, continuous_toFun := ⋯ } ≫ π') ≫ snd S' ℕ∪{∞}))
      x =
    (ConcreteCategory.hom (𝟙 (S' ⊗ ℕ∪{∞}) ≫ snd S' ℕ∪{∞})) x

Tactic:
exact h.elim x

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

Goal state before:
pp: case neg.cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : kerase a (kerase a' xs) = kerase a' (kerase a xs)
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))

Tactic:
by_cases a' = x.1

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : kerase a (kerase a' xs) = kerase a' (kerase a xs)
h✝ : a' = x.fst
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : kerase a (kerase a' xs) = kerase a' (kerase a xs)
h✝ : ¬a' = x.fst
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))
Module: Mathlib.Data.List.Sigma

Goal state before:
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)

Tactic:
subst h₁ h₂
      cases Ne.irrefl h

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

Goal state before:
pp: S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
abv : AbsoluteValue ℤ S
x : ℤˣ
⊢ abv ↑x = 1

Tactic:
rcases Int.units_eq_one_or x with (rfl | rfl) <;> simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : Ring R
inst✝³ : CommRing S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Nontrivial R
abv : AbsoluteValue R S
x : ℤˣ
⊢ abv ↑↑x = 1

Tactic:
rcases Int.units_eq_one_or x with (rfl | rfl) <;> simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
abv : AbsoluteValue R S
x : ℤˣ
y : R
⊢ abv (x • y) = abv y

Tactic:
rcases Int.units_eq_one_or x with (rfl | rfl) <;> simp

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
β : Type u_1
n : ℕ
s : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
⊢ ∀ (s : Finset β),
    x ∉ s →
      ((∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (s.card * n) (∑ x ∈ s, f x)) →
        (∀ x_1 ∈ insert x s, CPRankMax n (f x_1)) → CPRankMax ((insert x s).card * n) (∑ x ∈ insert x s, f x)

Tactic:
s

Goal state after:
α : Type
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
β : Type u_1
n : ℕ
s✝ : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
s : Finset β
⊢ x ∉ s →
    ((∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (s.card * n) (∑ x ∈ s, f x)) →
      (∀ x_1 ∈ insert x s, CPRankMax n (f x_1)) → CPRankMax ((insert x s).card * n) (∑ x ∈ insert x s, f x)
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: a b n : ℕ
a_lt_n : a < n
b_lt_n : b < n
⊢ (↑a - ↑b).natAbs < n

Tactic:
by
  rw [← Nat.cast_lt (α := ℤ), natCast_natAbs]
  exact abs_sub_lt_of_nonneg_of_lt (natCast_nonneg a) (ofNat_lt.mpr a_lt_n)
    (natCast_nonneg b) (ofNat_lt.mpr b_lt_n)

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

Goal state before:
pp: p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : ↑(p ^ k) ∣ m
hpn : ↑(p ^ l) ∣ n
hpmn : ↑(p ^ (k + l + 1)) ∣ m * n
hpm' : p ^ k ∣ m.natAbs
hpn' : p ^ l ∣ n.natAbs
hpmn' : p ^ (k + l + 1) ∣ m.natAbs * n.natAbs
hsd : p ^ (k + 1) ∣ m.natAbs ∨ p ^ (l + 1) ∣ n.natAbs :=
  Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul p_prime hpm' hpn' hpmn'
hsd2 : p ^ (l + 1) ∣ n.natAbs
⊢ ↑(p ^ (l + 1)) ∣ n

Tactic:
apply Int.dvd_natAbs.1; apply Int.natCast_dvd_natCast.2 hsd2

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

Goal state before:
pp: 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

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

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

Tactic:
· by_cases h : f false true <;> simp [h]

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)

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.List.Indexes

Goal state before:
pp: m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
as : List α
arr : Array PUnit
⊢ mapIdxMAux' f arr.size as = mapIdxM.go f as arr *> pure PUnit.unit

Tactic:
by
  induction as generalizing arr with
  | nil => simp only [mapIdxMAux', mapIdxM.go, seqRight_eq, map_pure, seq_pure]
  | cons head tail ih =>
    simp only [mapIdxMAux', seqRight_eq, map_eq_pure_bind, seq_eq_bind_map, bind_pure_unit,
      LawfulMonad.bind_assoc, pure_bind, mapIdxM.go]
    generalize (f (Array.size arr) head) = head
    have : (arr.push ⟨⟩).size = arr.size + 1 := Array.size_push _
    rw [← this, ih]
    simp only [seqRight_eq, map_eq_pure_bind, seq_pure, LawfulMonad.bind_assoc, pure_bind]

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

Goal state before:
pp: case cons
α : Type u_1
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) tl
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) (hd :: tl)

Tactic:
by_cases hp : p hd <;> by_cases hq : q hd <;> simp [takeWhile, hp, hq, IH]

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
hx : x ∈ (takeWhile p l.reverse).reverse
⊢ p x = true

Tactic:
mem_reverse

Goal state after:
α : Type u_1
p : α → Bool
l : List α
x : α
hx : x ∈ takeWhile p l.reverse
⊢ p x = true
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_2
l : List α
sz : List ℕ
b : ℕ
h : ∀ (n : ℕ), n ∈ sz → n ≤ b
⊢ ∀ (l₂ : List α), l₂ ∈ sz.splitLengths l → l₂.length ≤ b

Tactic:
List.forall_mem_iff_forall_getElem

Goal state after:
α : Type u_2
l : List α
sz : List ℕ
b : ℕ
h : ∀ (n : ℕ), n ∈ sz → n ≤ b
⊢ ∀ (i : ℕ) (hi : i < (sz.splitLengths l).length), (sz.splitLengths l)[i].length ≤ b
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case mp
α : Type u_1
p : ℕ
w : List α
⊢ w <+: take p w ++ w → ∀ i < w.length - p, w[i]? = w[i + p]?

Tactic:
intro pref j len

Goal state after:
case mp
α : Type u_1
p : ℕ
w : List α
pref : w <+: take p w ++ w
j : ℕ
len : j < w.length - p
⊢ w[j]? = w[j + p]?
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case inr.inr.lt
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.lt
⊢ w.HasPeriod (p.gcd q)

Tactic:
have p_lt_q := Nat.compare_eq_lt.mp hyp

Goal state after:
case inr.inr.lt
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.lt
p_lt_q : p < q
⊢ w.HasPeriod (p.gcd q)
Module: Mathlib.Data.Nat.Digits.Div

Goal state before:
pp: n : ℕ
⊢ ↑n ≡ (List.map (fun n ↦ ↑n) (digits 10 n)).alternatingSum [ZMOD 11]

Tactic:
by
  have t := zmodeq_ofDigits_digits 11 10 (-1 : ℤ) (by unfold Int.ModEq; rfl) n
  rwa [ofDigits_neg_one] at t

Goal state after:
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]
hn₀ : n ≠ p ^ multiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m
⊢ False

Tactic:
specialize h (p ^ multiplicity p n) (by grind [le_of_dvd hn (pow_multiplicity_dvd p n)])

Goal state after:
n p : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
h : ↑(n.choose (p ^ multiplicity p n)) ≡ 0 [ZMOD ↑p]
hn₀ : n ≠ p ^ multiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m
⊢ False
Module: Mathlib.Data.Nat.Hyperoperation

Goal state before:
pp: case zero
k : ℕ
⊢ hyperoperation (0 + 3) 1 k = 1

Tactic:
grind [cases Nat]

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

Goal state before:
pp: case succ
n✝ : ℕ
a✝ : ∀ (k : ℕ), hyperoperation (n✝ + 3) 1 k = 1
k : ℕ
⊢ hyperoperation (n✝ + 1 + 3) 1 k = 1

Tactic:
grind [cases Nat]

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

Goal state before:
pp: case succ
n : PosNum
n✝ : ℕ
a✝ : ∀ {k : PosNum}, (↑n).sqrt < n✝ + ↑k.bit1 → ↑(n.minFacAux n✝ k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < n✝ + 1 + ↑k.bit1
⊢ ↑(if n < k.bit1 * k.bit1 then n else if k.bit1 ∣ n then k.bit1 else n.minFacAux n✝ k.succ) =
    if ↑n < ↑k.bit1 * ↑k.bit1 then ↑n else if ↑k.bit1 ∣ ↑n then ↑k.bit1 else (↑n).minFacAux (↑k.bit1 + 2)

Tactic:
case succ fuel ih =>
    simp_rw [← mul_to_nat]
    simp only [cast_lt, dvd_to_nat]
    split_ifs <;> try rfl
    rw [ih] <;> [congr; convert! Nat.lt_succ_of_lt h using 1] <;>
      simp only [cast_bit1, cast_succ, Nat.succ_eq_add_one, add_assoc,
        add_left_comm, ← one_add_one_eq_two]

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

Goal state before:
pp: case bit1.hnc
n : PosNum
⊢ ¬2 ∣ ↑n.bit1

Tactic:
simp [← two_mul]

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

Goal state before:
pp: case bit0.hc
a✝ : PosNum
⊢ 2 ∣ ↑a✝.bit0

Tactic:
simp [← two_mul]

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

Goal state before:
pp: ⊢ (ofNat' 0).toZNum = (ofNat' (0 + 1)).toZNumNeg + 1

Tactic:
ofNat'_succ,

Goal state after:
⊢ (ofNat' 0).toZNum = (ofNat' 0 + 1).toZNumNeg + 1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: m : Num
p : PosNum
h : ZNum.neg p = m.toZNum
⊢ m ∈ ofZNum' (ZNum.neg p)

Tactic:
by cases m <;> cases h

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

Goal state before:
pp: case pos.succ.zero
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + (1 + 1)
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
r1 : r.size = 1
l1 : l.size = 1
n✝ : ℕ
mm : n✝ + 1 + 0 ≤ 1
⊢ BalancedSz 1 (n✝ + 1) ∧ BalancedSz 0 1 ∧ BalancedSz (1 + (n✝ + 1) + 1) (0 + 1 + 1)

Tactic:
rcases mm with (_ | ⟨⟨⟩⟩); decide

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

Goal state before:
pp: case mp
F : PFunctor.{uA, uB}
n : ℕ
x y : F.M
h : Agree (x.approx n) (y.approx (n + 1))
⊢ Agree' n x y

Tactic:
induction n generalizing x y with
    | zero => constructor
    | succ _ n_ih =>
      induction x using PFunctor.M.casesOn'
      induction y using PFunctor.M.casesOn'
      simp only [approx_mk] at h
      obtain - | ⟨_, _, hagree⟩ := h
      constructor <;> try rfl
      intro i
      apply n_ih
      apply hagree

Goal state after: