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

Goal state before:
pp: I : Type u
inst✝² : Category.{u, u} I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
⊢ IsColimit ((locallyConstantPresheaf X).mapCocone c.op)

Tactic:
refine Types.FilteredColimit.isColimitOf _ _ ?_ ?_

Goal state after:
case refine_1
I : Type u
inst✝² : Category.{u, u} I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
⊢ ∀ (x : ((locallyConstantPresheaf X).mapCocone c.op).pt),
    ∃ i xi, x = (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app i)) xi

case refine_2
I : Type u
inst✝² : Category.{u, u} I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
⊢ ∀ (i j : Iᵒᵖ) (xi : (fun X ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj i))
    (xj : (fun X ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj j)),
    (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app i)) xi =
        (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app j)) xj →
      ∃ k f g,
        (ConcreteCategory.hom (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).map f)) xi =
          (ConcreteCategory.hom (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).map g)) xj
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
⊢ IsColimit ((locallyConstantPresheaf X).mapCocone c.op)

Tactic:
refine Types.FilteredColimit.isColimitOf _ _ ?_ ?_

Goal state after:
case refine_1
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
⊢ ∀ (x : ((locallyConstantPresheaf X).mapCocone c.op).pt),
    ∃ i xi, x = (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app i)) xi

case refine_2
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
⊢ ∀ (i j : ℕᵒᵖᵒᵖ) (xi : (fun X ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj i))
    (xj : (fun X ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj j)),
    (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app i)) xi =
        (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app j)) xj →
      ∃ k f g,
        (ConcreteCategory.hom (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map f)) xi =
          (ConcreteCategory.hom (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map g)) xj
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: S : LightProfinite
inst✝ : Nonempty ↑S.toTop
X Y : Profinite
g : X ⟶ lightToProfinite.obj S
f : X ⟶ Y
h : Mono f
this✝¹ : ∀ (n : ℕ), Finite ↑(lightToProfinite.obj (S.component n)).toTop
this✝ : Nonempty ↑(lightToProfinite.obj (S.component 0)).toTop
this : ∀ (n : ℕ), Epi (S.transitionMap n)
k0 : Y ⟶ lightToProfinite.obj (S.diagram.obj (Opposite.op 0))
h_down0 : f ≫ k0 = g ≫ lightToProfinite.map (S.proj 0)
h_comm :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      f ≫ k = g ≫ lightToProfinite.map (S.proj (n + 1)) ≫ lightToProfinite.map (S.transitionMap n)
h_step :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      ∃ k', k' ≫ lightToProfinite.map (S.transitionMap n) = k ∧ f ≫ k' = g ≫ lightToProfinite.map (S.proj (n + 1))
lifts : ℕ → Type (max 0 u) := fun n ↦ { k // f ≫ k = g ≫ lightToProfinite.map (S.proj n) }
next : (n : ℕ) → lifts n → lifts (n + 1) := fun n k ↦ ⟨⋯.choose, ⋯⟩
k_seq : (n : ℕ) → lifts n := fun n ↦ Nat.rec ⟨k0, h_down0⟩ next n
h_down : ∀ (n : ℕ), f ≫ ↑(k_seq n) = g ≫ lightToProfinite.map (S.proj n)
h_up : ∀ (n : ℕ), ↑(k_seq (n + 1)) ≫ lightToProfinite.map (S.transitionMap n) = ↑(k_seq n)
k_cone : Cone (S.diagram ⋙ lightToProfinite) := { pt := Y, π := NatTrans.ofOpSequence (fun n ↦ ↑(k_seq n)) ⋯ }
hg : g = (isLimitOfPreserves lightToProfinite S.asLimit).lift (k_cone.extend f)
n : ℕᵒᵖ
⊢ (f ≫ (isLimitOfPreserves lightToProfinite S.asLimit).lift k_cone) ≫ (lightToProfinite.mapCone S.asLimitCone).π.app n =
    (k_cone.extend f).π.app n

Tactic:
simp [-Functor.mapCone_pt, -Functor.mapCone_π_app]

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

Goal state before:
pp: case id_bitraverse
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ β✝ : Type u
x✝ : _root_.flip t α✝ β✝
toLawfulBifunctor✝ : LawfulBifunctor t
id_bitraverse✝ : ∀ {α β : Type u} (x : t α β), bitraverse pure pure x = pure x
comp_bitraverse✝ :
  ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
    {α α' β β' γ γ' : Type u} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β') (x : t α α'),
    bitraverse (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x = Comp.mk (bitraverse f f' <$> bitraverse g g' x)
bitraverse_eq_bimap_id✝ :
  ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : t α α'),
    bitraverse (pure ∘ f) (pure ∘ f') x = pure (bimap f f' x)
binaturality✝ :
  ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
    (η : ApplicativeTransformation F G) {α α' β β' : Type u} (f : α → F β) (f' : α' → F β') (x : t α α'),
    (fun {α} ↦ η.app α) (bitraverse f f' x) = bitraverse ((fun {α} ↦ η.app α) ∘ f) ((fun {α} ↦ η.app α) ∘ f') x
⊢ bitraverse pure pure x✝ = pure x✝

Tactic:
apply_assumption only [*]

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

Goal state before:
pp: case comp_bitraverse
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type u
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
g✝ : α✝ → G✝ β✝
g'✝ : α'✝ → G✝ β'✝
x✝ : _root_.flip t α✝ α'✝
toLawfulBifunctor✝ : LawfulBifunctor t
id_bitraverse✝ : ∀ {α β : Type u} (x : t α β), bitraverse pure pure x = pure x
comp_bitraverse✝ :
  ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
    {α α' β β' γ γ' : Type u} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β') (x : t α α'),
    bitraverse (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x = Comp.mk (bitraverse f f' <$> bitraverse g g' x)
bitraverse_eq_bimap_id✝ :
  ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : t α α'),
    bitraverse (pure ∘ f) (pure ∘ f') x = pure (bimap f f' x)
binaturality✝ :
  ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
    (η : ApplicativeTransformation F G) {α α' β β' : Type u} (f : α → F β) (f' : α' → F β') (x : t α α'),
    (fun {α} ↦ η.app α) (bitraverse f f' x) = bitraverse ((fun {α} ↦ η.app α) ∘ f) ((fun {α} ↦ η.app α) ∘ f') x
⊢ bitraverse (Comp.mk ∘ map f✝ ∘ g✝) (Comp.mk ∘ map f'✝ ∘ g'✝) x✝ = Comp.mk (bitraverse f✝ f'✝ <$> bitraverse g✝ g'✝ x✝)

Tactic:
apply_assumption only [*]

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

Goal state before:
pp: case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : _root_.flip t α✝ α'✝
toLawfulBifunctor✝ : LawfulBifunctor t
id_bitraverse✝ : ∀ {α β : Type u} (x : t α β), bitraverse pure pure x = pure x
comp_bitraverse✝ :
  ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
    {α α' β β' γ γ' : Type u} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β') (x : t α α'),
    bitraverse (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x = Comp.mk (bitraverse f f' <$> bitraverse g g' x)
bitraverse_eq_bimap_id✝ :
  ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : t α α'),
    bitraverse (pure ∘ f) (pure ∘ f') x = pure (bimap f f' x)
binaturality✝ :
  ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
    (η : ApplicativeTransformation F G) {α α' β β' : Type u} (f : α → F β) (f' : α' → F β') (x : t α α'),
    (fun {α} ↦ η.app α) (bitraverse f f' x) = bitraverse ((fun {α} ↦ η.app α) ∘ f) ((fun {α} ↦ η.app α) ∘ f') x
⊢ bitraverse (pure ∘ f✝) (pure ∘ f'✝) x✝ = pure (bimap f✝ f'✝ x✝)

Tactic:
apply_assumption only [*]

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

Goal state before:
pp: case binaturality
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : _root_.flip t α✝ α'✝
toLawfulBifunctor✝ : LawfulBifunctor t
id_bitraverse✝ : ∀ {α β : Type u} (x : t α β), bitraverse pure pure x = pure x
comp_bitraverse✝ :
  ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
    {α α' β β' γ γ' : Type u} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β') (x : t α α'),
    bitraverse (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x = Comp.mk (bitraverse f f' <$> bitraverse g g' x)
bitraverse_eq_bimap_id✝ :
  ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : t α α'),
    bitraverse (pure ∘ f) (pure ∘ f') x = pure (bimap f f' x)
binaturality✝ :
  ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
    (η : ApplicativeTransformation F G) {α α' β β' : Type u} (f : α → F β) (f' : α' → F β') (x : t α α'),
    (fun {α} ↦ η.app α) (bitraverse f f' x) = bitraverse ((fun {α} ↦ η.app α) ∘ f) ((fun {α} ↦ η.app α) ∘ f') x
⊢ (fun {α} ↦ η✝.app α) (bitraverse f✝ f'✝ x✝) = bitraverse ((fun {α} ↦ η✝.app α) ∘ f✝) ((fun {α} ↦ η✝.app α) ∘ f'✝) x✝

Tactic:
apply_assumption only [*]

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

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
t : T
⊢ t ∈ fibres π σ ↔ (π t).2 = none ∨ ∃ x s, σ (Option.some x) s = t

Tactic:
simp [fibres]

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

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × OnePoint X
hπ : Function.Surjective π
⊢ Function.Surjective (y π)

Tactic:
by
  intro s
  let p (s : S) (n : OnePoint X) : T := (hπ (s, n)).choose
  have hp (s : S) (n : OnePoint X) : π (p s n) = (s, n) := (hπ (s, n)).choose_spec
  exact ⟨⟨fun n ↦ ⟨p s n, by grind⟩, by grind⟩, by grind⟩

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
c : Sigma β
l : List (Sigma β)
hl : l.NodupKeys
h : ¬c.fst ∈ { entries := l, nodupKeys := hl }
⊢ ⋯.mpr (IH c.fst c.snd { entries := l, nodupKeys := ⋯ } ⋯ (insertRec H0 IH { entries := l, nodupKeys := ⋯ })) ≍
    IH c.fst c.snd { entries := l, nodupKeys := hl } h (insertRec H0 IH { entries := l, nodupKeys := hl })

Tactic:
apply cast_heq

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✝
⊢ x✝ ∈ s₁.keys

Tactic:
keys,

Goal state after:
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✝
⊢ x✝ ∈ s₁.entries.keys
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
⊢ x✝ ∈ s₂.keys

Tactic:
keys,

Goal state after:
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
⊢ x✝ ∈ s₂.entries.keys
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: case h
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
a✝ : List α
⊢ Functor.map h <$> traverse g ⟦a✝⟧ = traverse (Functor.map h ∘ g) ⟦a✝⟧

Tactic:
simp only [traverse, quot_mk_to_coe, lift_coe, Function.comp_apply, Functor.map_map]

Goal state after:
case h
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
a✝ : List α
⊢ (fun a ↦ h <$> ↑a) <$> Traversable.traverse g a✝ = ofList <$> Traversable.traverse (Functor.map h ∘ g) a✝
Module: Mathlib.Data.List.Sigma

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

Tactic:
keys,

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ map Sigma.fst (kerase a l) = (map Sigma.fst l).erase a
Module: Mathlib.Data.Finset.NatDivisors

Goal state before:
pp: m n k : ℕ
⊢ k ∈ (m * n).divisors ↔ k ∈ m.divisors * n.divisors

Tactic:
simp_rw [mem_mul, mem_divisors, Nat.dvd_mul, mul_ne_zero_iff, ← exists_and_left,
    ← exists_and_right]

Goal state after:
m n k : ℕ
⊢ (∃ x x_1, (x ∣ m ∧ x_1 ∣ n ∧ x * x_1 = k) ∧ m ≠ 0 ∧ n ≠ 0) ↔ ∃ y x, (y ∣ m ∧ m ≠ 0) ∧ (x ∣ n ∧ n ≠ 0) ∧ y * x = k
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
h : a ∈ l₁.keys
⊢ dlookup a (l₁.kunion l₂) = dlookup a l₁

Tactic:
by
  induction l₁ generalizing l₂ with
  | nil => simp at h
  | cons s _ ih =>
    simp only [keys_cons, mem_cons] at h
    rcases h with rfl | h <;> obtain ⟨a'⟩ := s
    · simp
    · rw [kunion_cons]
      by_cases h' : a = a'
      · subst h'
        simp
      · simp [h', ih h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : DecidableEq β
f : α →. β
inst✝¹ : (x : α) → Decidable (f x).Dom
s t : Finset α
inst✝ : DecidableEq α
⊢ pimage f (s ∩ t) ⊆ pimage f s ∩ pimage f t

Tactic:
simp only [← coe_subset, coe_pimage, coe_inter, PFun.image_inter]

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

Goal state before:
pp: case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
⊢ _root_.Disjoint hd.support (foldr (fun x y ↦ x.support ⊔ y) ∅ tl)

Tactic:
← List.foldr_map,

Goal state after:
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
⊢ _root_.Disjoint hd.support (foldr max ∅ (map Finsupp.support tl))
Module: Mathlib.Data.Finsupp.Sigma

Goal state before:
pp: κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : Zero M
k : κ
⊢ Injective embSigma

Tactic:
intro f g h

Goal state after:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : Zero M
k : κ
f g : ι k →₀ M
h : f.embSigma = g.embSigma
⊢ f = g
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: b : Bool
n : ℕ
⊢ bit b ↑n = ↑(Nat.bit b n)

Tactic:
rw [bit_val, Nat.bit_val]

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

Goal state before:
pp: b : Bool
n : ℕ
⊢ bit b -[n+1] = -[Nat.bit (!b) n+1]

Tactic:
rw [bit_val, Nat.bit_val]

Goal state after:
b : Bool
n : ℕ
⊢ (2 * -[n+1] + bif b then 1 else 0) = -[2 * n + (!b).toNat+1]
Module: Mathlib.Data.LawfulXor.Basic

Goal state before:
pp: α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a : α
⊢ 0 ^^^ a = a

Tactic:
by rw [LawfulXor.xor_comm, xor_zero]

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

Goal state before:
pp: a b r : ℤ
hr : 0 < r
⊢ ↑(#({x ∈ Ico a b | r ∣ x})) = max (⌈↑b / ↑r⌉ - ⌈↑a / ↑r⌉) 0

Tactic:
by
  rw [Ico_filter_dvd_eq _ _ hr, card_map, card_Ico, toNat_eq_max]

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

Goal state before:
pp: case mpr
a b r v : ℕ
x : ℤ
h : (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r]
⊢ ∃ a_1, ((a < a_1 ∧ a_1 ≤ b) ∧ a_1 ≡ v [MOD r]) ∧ ↑a_1 = x

Tactic:
lift x to ℕ using (by lia)

Goal state after:
case mpr
a b r v x : ℕ
h : (↑a < ↑x ∧ ↑x ≤ ↑b) ∧ ↑x ≡ ↑v [ZMOD ↑r]
⊢ ∃ a_1, ((a < a_1 ∧ a_1 ≤ b) ∧ a_1 ≡ v [MOD r]) ∧ ↑a_1 = ↑x
Module: Mathlib.Data.List.Indexes

Goal state before:
pp: α : Type u
β : Type v
l : List α
f : ℕ → α → β
⊢ mapIdx f l = ofFn fun i ↦ f (↑i) (l.get i)

Tactic:
by
  induction l generalizing f with
  | nil => simp
  | cons _ _ IH => simp [IH]

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ find? p l = (dropWhile (fun x ↦ !p x) l).head?

Tactic:
induction l
  case nil => simp
  case cons head tail hi =>
    set ph := p head with phh
    rcases ph with rfl | rfl
    · have phh' : ¬(p head = true) := by simp [phh.symm]
      rw [find?_cons_of_neg phh', dropWhile_cons_of_pos]
      · exact hi
      · simpa using phh
    · rw [find?_cons_of_pos phh.symm, dropWhile_cons_of_neg]
      · simp
      · simpa using phh

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

Goal state before:
pp: n m k : ℕ
h₁ : k ≤ n
⊢ map (fun x ↦ x - k) (range' n (m - n)) = range' (n - k) (m - k - (n - k))

Tactic:
Nat.sub_sub_sub_cancel_right h₁,

Goal state after:
n m k : ℕ
h₁ : k ≤ n
⊢ map (fun x ↦ x - k) (range' n (m - n)) = range' (n - k) (m - n)
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
as : List α
b : β
bs : List β
⊢ zipWith (flip f) (b :: bs) (a :: as) = zipWith f (a :: as) (b :: bs)

Tactic:
simp! [zipWith_flip]
    rfl

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

Goal state before:
pp: case inl
n m l : ℕ
hlm : l ≤ m
hnl : n ≤ l
⊢ Ico n l ++ filter (fun x ↦ decide (x < l)) (Ico l m) = Ico n l

Tactic:
filter_lt_of_le_bot (le_refl l),

Goal state after:
case inl
n m l : ℕ
hlm : l ≤ m
hnl : n ≤ l
⊢ Ico n l ++ [] = Ico n l
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α},
        Acc (Shortlex r) b →
          (∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s) → Acc (Shortlex r) (y :: b)
b xb : List α
h✝ : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb → (∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s) → Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h : r x xa
h2len : xs.length = xb.length
⊢ xs.length < (xa :: xb).length

Tactic:
rw [h2len]

Goal state after:
α : Type u_1
r : α → α → Prop
a xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α},
        Acc (Shortlex r) b →
          (∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s) → Acc (Shortlex r) (y :: b)
b xb : List α
h✝ : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb → (∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s) → Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h : r x xa
h2len : xs.length = xb.length
⊢ xb.length < (xa :: xb).length
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

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

Goal state before:
pp: α : Type u_1
w : List α
⊢ w.HasPeriod 0

Tactic:
by
  simp [HasPeriod]

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

Goal state before:
pp: case neg
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_lt_n : ¬j < n
⊢ (take n w ++ w)[j]? = w[j % p]?

Tactic:
have j_minus : j - n < w.length := by lia

Goal state after:
case neg
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_lt_n : ¬j < n
j_minus : j - n < w.length
⊢ (take n w ++ w)[j]? = w[j % p]?
Module: Mathlib.Data.Multiset.Interval

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

Tactic:
bot_eq_zero,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ ∏ x ∈ toFinset 0 ∪ s.toFinset, (count x s + 1 - count x 0) = ∏ i ∈ s.toFinset, (count i s + 1)
Module: Mathlib.Data.Nat.Choose.Dvd

Goal state before:
pp: p a b : ℕ
hp : Prime p
hb : b < p
ha : a ≤ b
⊢ p.Coprime (b.choose a)

Tactic:
rw [Nat.choose_eq_descFactorial_div_factorial]

Goal state after:
p a b : ℕ
hp : Prime p
hb : b < p
ha : a ≤ b
⊢ p.Coprime (b.descFactorial a / a !)
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: case cons
ι : Type u_1
a s : ι → ℕ
z : ℕ
i : ι
l : List ι
ih :
  ∀ (co : List.Pairwise (Coprime on s) l),
    (∀ i ∈ l, z ≡ a i [MOD s i]) → z ≡ ↑(chineseRemainderOfList a s l co) [MOD (List.map s l).prod]
co : List.Pairwise (Coprime on s) (i :: l)
hz : ∀ i_1 ∈ i :: l, z ≡ a i_1 [MOD s i_1]
⊢ z ≡ ↑(chineseRemainderOfList a s (i :: l) co) [MOD (List.map s (i :: l)).prod]

Tactic:
simp only [List.map_cons, List.prod_cons, chineseRemainderOfList]

Goal state after:
case cons
ι : Type u_1
a s : ι → ℕ
z : ℕ
i : ι
l : List ι
ih :
  ∀ (co : List.Pairwise (Coprime on s) l),
    (∀ i ∈ l, z ≡ a i [MOD s i]) → z ≡ ↑(chineseRemainderOfList a s l co) [MOD (List.map s l).prod]
co : List.Pairwise (Coprime on s) (i :: l)
hz : ∀ i_1 ∈ i :: l, z ≡ a i_1 [MOD s i_1]
⊢ z ≡ ↑(chineseRemainder ⋯ (a i) ↑(chineseRemainderOfList a s l ⋯)) [MOD s i * (List.map s l).prod]
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n m : ℕ
h : n = m
⊢ n.dist m = 0

Tactic:
unfold Nat.dist; lia

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

Goal state before:
pp: n m : ℕ
h : n ≤ m
⊢ n.dist m = m - n

Tactic:
unfold Nat.dist; lia

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

Goal state before:
pp: n m : ℕ
h : m ≤ n
⊢ n.dist m = n - m

Tactic:
unfold Nat.dist; lia

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

Goal state before:
pp: n m : ℕ
⊢ m ≤ n.dist m + n

Tactic:
unfold Nat.dist; lia

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

Goal state before:
pp: n m : ℕ
⊢ m ≤ n + n.dist m

Tactic:
unfold Nat.dist; lia

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

Goal state before:
pp: n m : ℕ
⊢ n ≤ n.dist m + m

Tactic:
unfold Nat.dist; lia

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

Goal state before:
pp: n m : ℕ
⊢ n ≤ m + n.dist m

Tactic:
unfold Nat.dist; lia

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

Goal state before:
pp: n : ℕ
⊢ n.dist 0 = n

Tactic:
unfold Nat.dist; lia

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

Goal state before:
pp: n : ℕ
⊢ dist 0 n = n

Tactic:
unfold Nat.dist; lia

Goal state after: