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

Goal state before:
pp: case tail.convert_5
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := ⋯
⊢ List Γ'

pp: case tail.convert_9
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn v none fun x x_1 ↦ some Γ'.cons
⊢ splitAtPred natEnd (elim (trList v) [] [] (trContStack k) main) = (?tail.convert_5, o, trList v.tail)

Tactic:
swap

Goal state after:
case tail.convert_9
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn v none fun x x_1 ↦ some Γ'.cons
⊢ splitAtPred natEnd (elim (trList v) [] [] (trContStack k) main) = (?tail.convert_5, o, trList v.tail)

case tail.convert_5
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := ⋯
⊢ List Γ'
Module: Mathlib.Topology.ClopenBox

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace Y
inst✝ : CompactSpace X
W : Clopens (X × Y)
⊢ ∃ I, W = I.sup fun i ↦ i.1 ×ˢ i.2

Tactic:
by
  choose! U hxU V hxV hUV using fun x ↦ W.exists_prod_subset (a := x)
  rcases W.2.1.isCompact.elim_nhds_subcover (fun x ↦ U x ×ˢ V x) (fun x hx ↦
    (U x ×ˢ V x).2.isOpen.mem_nhds ⟨hxU x hx, hxV x hx⟩) with ⟨I, hIW, hWI⟩
  classical
  use I.image fun x ↦ (U x, V x)
  rw [Finset.sup_image]
  refine le_antisymm (fun x hx ↦ ?_) (Finset.sup_le fun x hx ↦ ?_)
  · rcases Set.mem_iUnion₂.1 (hWI hx) with ⟨i, hi, hxi⟩
    exact SetLike.le_def.1 (Finset.le_sup hi) hxi
  · exact hUV _ <| hIW _ hx

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

Goal state before:
pp: X Y : LightProfinite
f : X ⟶ Y
⊢ EffectiveEpi f ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ ⟨⟨effectiveEpiStruct f h⟩⟩⟩
  rw [← epi_iff_surjective]
  infer_instance

Goal state after:
Module: Mathlib.Logic.Function.FiberPartition

Goal state before:
pp: Y : Type u_2
Z : Type u_3
W : Type u_4
f : Y → Z
g : Z → W
a : Fiber (g ∘ f)
⊢ g (f (preimage (g ∘ f) a)) = image (g ∘ f) a

Tactic:
by rw [← map_preimage_eq_image, comp_apply]

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

Goal state before:
pp: J : Type v
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
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

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

Tactic:
swap

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

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
Module: Mathlib.Condensed.Discrete.Module

Goal state before:
pp: P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
M : ModuleCat R
this✝ : (constantSheaf (coherentTopology CompHaus) (Type (u + 1))).Faithful
this : (constantSheaf (coherentTopology CompHaus) (Type (u + 1))).Full
⊢ CondensedSet.LocallyConstant.functor.essImage
    ((sheafCompose (coherentTopology CompHaus) (CategoryTheory.forget (ModuleCat R))).obj ((functor R).obj M))

Tactic:
exact obj_mem_essImage CondensedSet.LocallyConstant.functor M

Goal state after:
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 (𝟙 (Profinite.of PUnit.{u + 1})).op)) (Function.Fiber.image (⇑f) x)

Tactic:
simp only [op_comp, Functor.map_comp_apply, op_id, Functor.map_id_apply]

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).op))
      ((ConcreteCategory.hom (X.map (sigmaIncl f x).op))
        ((ConcreteCategory.hom (isoFinYonedaComponents X (Profinite.of (Opposite.unop Y).obj)).inv) ⇑f)) =
    Function.Fiber.image (⇑f) x
Module: Mathlib.Control.Fix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
k : ℕ
this : p (k + ↑Upto.zero)
⊢ Nat.find h' = k + ↑Upto.zero →
    (assert (∃ i, (Fix.approx f i x).Dom) fun h ↦ ⋯.fix (fixAux f) Upto.zero x) = Fix.approx f (k + 1) x

Tactic:
rw [assert_pos h']

Goal state after:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
k : ℕ
this : p (k + ↑Upto.zero)
⊢ Nat.find h' = k + ↑Upto.zero → ⋯.fix (fixAux f) Upto.zero x = Fix.approx f (k + 1) x
Module: Mathlib.Control.LawfulFix

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

Tactic:
induction j with
  | zero => cases hij; exact le_rfl
  | succ j ih =>
    cases hij; · exact le_rfl
    exact le_trans (ih ‹_›) (approx_mono' f)

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

Goal state before:
pp: case refine_1
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
x : T
x✝ : ¬(π x).2 = none ∧ ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x
h₁ : ¬(π x).2 = none
h₂ : ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x
⊢ ∃ i, (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = ↑i

Tactic:
obtain ⟨n, hn⟩ := Option.ne_none_iff_exists'.mp h₁

Goal state after:
case refine_1
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
x : T
x✝ : ¬(π x).2 = none ∧ ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x
h₁ : ¬(π x).2 = none
h₂ : ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x
n : X
hn : (π x).2 = Option.some n
⊢ ∃ i, (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = ↑i
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
F : f.Realizer
E : F.σ ≃ τ
x✝¹ : Set α
x✝ : x✝¹ ∈ F.F.toFilter.sets
t : F.σ
h : F.F.f t ⊆ x✝¹
⊢ (CFilter.ofEquiv E F.F).f (E t) ⊆ x✝¹

Tactic:
simp [h]

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

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

Tactic:
simp_rw [Finset.sum_cons, ihs]

Goal state after:
case cons
α : Type u_1
ι : Type u_2
f : α → ι → ℕ∞
hf : ∀ (i j : ι), ∃ k, ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a : α
s : Finset α
ha : a ∉ s
ihs : ∑ a ∈ s, ⨆ i, f a i = ⨆ i, ∑ a ∈ s, f a i
⊢ (⨆ i, f a i) + ⨆ i, ∑ a ∈ s, f a i = ⨆ i, f a i + ∑ a ∈ s, f a i
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n : ℕ
α : Type u_2
m : ℕ
h : m ≤ n
v : Fin n → α
⊢ (List.ofFn (take m h v)).length = (List.take m (List.ofFn v)).length

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_2
m : ℕ
l : List α
h : m ≤ l.length
⊢ (List.ofFn (take m h l.get)).length = (List.take m l).length

Tactic:
simp [h]

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

Goal state before:
pp: n : ℕ
α✝ : Fin n → Sort u_1
α : Type u_2
m : ℕ
v : Fin n → α
h : m ≤ n
⊢ (List.take m (List.ofFn v)).length = m

Tactic:
simp [h]

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

Goal state before:
pp: case cons
α : Type u
α' : Type u'
β : Type v
f : α → α'
hf : Function.Injective f
hd : (_ : α) × β
tl : List ((_ : α) × β)
ih : tl.NodupKeys → (map (Sigma.map f fun x ↦ id) tl).NodupKeys
nd : ¬hd.fst ∈ tl.keys ∧ tl.NodupKeys
⊢ ¬(Sigma.map f (fun x ↦ id) hd).fst ∈ (map (Sigma.map f fun x ↦ id) tl).keys ∧
    (map (Sigma.map f fun x ↦ id) tl).NodupKeys

Tactic:
exact ⟨mt (fun h => by
      simp only [keys, map_map] at h ⊢
      obtain ⟨x, hm, he⟩ := mem_map.mp h
      exact mem_map.mpr ⟨x, hm, hf he⟩) nd.1, ih nd.2⟩

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup x s₁.entries = dlookup x s₂.entries
⊢ s₁.entries ~ s₂.entries

Tactic:
apply lookup_ext s₁.nodupKeys s₂.nodupKeys

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup x s₁.entries = dlookup x s₂.entries
⊢ ∀ (x : α) (y : β x), y ∈ dlookup x s₁.entries ↔ y ∈ dlookup x s₂.entries
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
bh : β a'
h₁ : ¬a = a'
⊢ dlookup a (kerase a' (⟨a', bh⟩ :: tl)) = dlookup a (⟨a', bh⟩ :: tl)

Tactic:
simp [h]

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

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

Tactic:
· simp [h₁, h₂, ih]

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

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

Tactic:
simp [h]

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

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : a = a'
⊢ a ∈ (kinsert a' b' l).keys ↔ a = a' ∨ a ∈ l.keys

Tactic:
simp [h]

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

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ a ∈ (kinsert a' b' l).keys ↔ a = a' ∨ a ∈ l.keys

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : a ≠ a'
⊢ dlookup a (kinsert a' b' l) = dlookup a l

Tactic:
simp [h]

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

Goal state before:
pp: m n : ℕ
hmn : m.Coprime n
⊢ Set.InjOn (fun p ↦ p.1 * p.2) ↑(m.divisors ×ˢ n.divisors)

Tactic:
by
  rintro ⟨dm₁, dn₁⟩ h₁ ⟨dm₂, dn₂⟩ h₂ hd
  simp only [Finset.mem_coe, Finset.mem_product, mem_divisors] at *
  suffices dm₁ = dm₂ from Prod.ext this <| by
    rwa [this, Nat.mul_right_inj (by simp [·] at h₂)] at hd
  exact dvd_antisymm
    (hmn.coprime_dvd_left h₁.1.1 |>.coprime_dvd_right h₂.2.1
      |>.dvd_of_dvd_mul_right (hd ▸ dm₁.dvd_mul_right dn₁))
    (hmn.coprime_dvd_left h₂.1.1 |>.coprime_dvd_right h₁.2.1
      |>.dvd_of_dvd_mul_right (hd ▸ dm₂.dvd_mul_right dn₂))

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

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

Tactic:
simp [h]

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

Goal state before:
pp: case pos
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
m : M
b : α
h : b = a
⊢ (insert a m l).lookupFinsupp b = (l.lookupFinsupp.update a m) b

Tactic:
simp [h]

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

Goal state before:
pp: case neg
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
m : M
b : α
h : ¬b = a
⊢ (insert a m l).lookupFinsupp b = (l.lookupFinsupp.update a m) b

Tactic:
simp [h]

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

Goal state before:
pp: case neg
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬f a = 0
⊢ f.toAList.lookupFinsupp a = f a

Tactic:
suffices f.toAList.lookup a = some (f a) by simp [this]
      apply mem_lookup_iff.2
      simpa using h

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

Goal state before:
pp: m n : ℤ
⊢ (m * n).bodd = (m.bodd && n.bodd)

Tactic:
rcases m with m | m <;> rcases n with n | n <;>
  simp only [ofNat_eq_natCast, ofNat_mul_negSucc, negSucc_mul_ofNat, ofNat_mul_ofNat,
             negSucc_mul_negSucc]

Goal state after:
case ofNat.ofNat
m n : ℕ
⊢ (↑(m * n)).bodd = ((↑m).bodd && (↑n).bodd)

case ofNat.negSucc
m n : ℕ
⊢ (-↑(m * n.succ)).bodd = ((↑m).bodd && -[n+1].bodd)

case negSucc.ofNat
m n : ℕ
⊢ (-↑(m.succ * n)).bodd = (-[m+1].bodd && (↑n).bodd)

case negSucc.negSucc
m n : ℕ
⊢ (↑(m.succ * n.succ)).bodd = (-[m+1].bodd && -[n+1].bodd)
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: a b r q : ℤ
h : b ≠ 0
⊢ a / b = q ∧ a % b = r ↔ r + b * q = a ∧ 0 ≤ r ∧ r < |b|

Tactic:
constructor
  · intro ⟨rfl, rfl⟩
    exact ⟨emod_add_mul_ediv a b, emod_nonneg _ h, emod_lt_abs _ h⟩
  · intro ⟨rfl, hz, hb⟩
    constructor
    · rw [Int.add_mul_ediv_left r q h, ediv_eq_zero_of_lt_abs hz hb]
      simp
    · rw [add_mul_emod_self_left, ← emod_abs, emod_eq_of_lt hz hb]

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

Goal state before:
pp: case pos
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : f false false = true
⊢ (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)

Tactic:
simp [h]

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

Goal state before:
pp: case neg
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : ¬f false false = true
⊢ (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)

Tactic:
simp [h]

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

Goal state before:
pp: case pos
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : f false true = true
⊢ (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:
simp [h]

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

Goal state before:
pp: case neg
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : ¬f false true = true
⊢ (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:
simp [h]

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

Goal state before:
pp: case pos
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : f true false = true
⊢ (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:
simp [h]

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

Goal state before:
pp: case neg
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : ¬f true false = true
⊢ (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:
simp [h]

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

Goal state before:
pp: case pos
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : f true true = true
⊢ (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:
simp [h]

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

Goal state before:
pp: case neg
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : ¬f true true = true
⊢ (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:
simp [h]

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

Goal state before:
pp: m n✝ k i n : ℕ
⊢ ↑m >>> (↑i + 1) = ↑(m <<< n >>> (n + i + 1))

Tactic:
Nat.shiftRight_add,

Goal state after:
m n✝ k i n : ℕ
⊢ ↑m >>> (↑i + 1) = ↑(m <<< n >>> n >>> i >>> 1)
Module: Mathlib.Data.Int.Bitwise

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

Tactic:
Nat.shiftRight_add,

Goal state after:
m n✝ k i n : ℕ
⊢ m >>> i.succ = Nat.shiftLeft' true m n >>> n >>> (i + 1)
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: case pos
α : Type u_1
p : α → Bool
l : List α
x : α
h : p x = true
⊢ (match p x with
      | true => dropWhile p l.reverse
      | false => x :: l.reverse).reverse =
    (dropWhile p l.reverse).reverse

Tactic:
simp [h]

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

Goal state before:
pp: case neg
α : Type u_1
p : α → Bool
l : List α
x : α
h : ¬p x = true
⊢ (match p x with
      | true => dropWhile p l.reverse
      | false => x :: l.reverse).reverse =
    l ++ [x]

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
⊢ rdropWhile p (l ++ [x]) = if p x = true then rdropWhile p l else l ++ [x]

Tactic:
by
  simp only [rdropWhile, dropWhile, reverse_append, reverse_singleton, singleton_append]
  split_ifs with h <;> simp [h]

Goal state after:
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:
by
  simp_rw [rdropWhile]
  rw [getLast_reverse, head_dropWhile_not p]
  simp

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

Goal state before:
pp: case pos
α : Type u_1
p : α → Bool
l : List α
x : α
h : p x = true
⊢ (match p x with
      | true => x :: takeWhile p l.reverse
      | false => []).reverse =
    (takeWhile p l.reverse).reverse ++ [x]

Tactic:
simp [h]

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

Goal state before:
pp: case neg
α : Type u_1
p : α → Bool
l : List α
x : α
h : ¬p x = true
⊢ (match p x with
      | true => x :: takeWhile p l.reverse
      | false => []).reverse =
    []

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
l : List α
i j : ℕ
⊢ (l.rdrop i).rdrop j = l.rdrop (i + j)

Tactic:
simp_rw [rdrop_eq_reverse_drop_reverse, reverse_reverse, drop_drop]

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

Goal state before:
pp: case cons
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ go f (tl ++ [a]) (r.push hd) = r.toListAppend (go f (tl ++ [a]) (#[].push hd))

pp: case cons.x_3
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ tl ++ [a] = [] → False

pp: case cons.x_3
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ tl ++ [a] = [] → False

Tactic:
case x_3 | x_3 => exact append_ne_nil_of_right_ne_nil tl (cons_ne_nil a [])

Goal state after:
case cons
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ go f (tl ++ [a]) (r.push hd) = r.toListAppend (go f (tl ++ [a]) (#[].push hd))
Module: Mathlib.Data.List.ModifyLast

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

Tactic:
rw [modifyLast.go_concat, Array.toListAppend_eq, Array.toList_push, List.toList_toArray,
      nil_append, cons_append, nil_append, cons_inj_right]

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

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

Tactic:
| cons _ tl =>

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

Goal state before:
pp: α : Type u_1
l : List α
x : α
hx : ¬x ∈ l
⊢ Set.InjOn (fun k ↦ l.insertIdx k x) {n | n ≤ l.length}

Tactic:
by
  intro n hn m hm h
  induction l generalizing n m with
  | nil =>
    simp_all [Set.mem_singleton_iff, Set.ofPred_eq_eq_singleton, length]
  | cons hd tl IH =>
    simp only [length, Set.mem_ofPred_eq] at hn hm
    simp only [mem_cons, not_or] at hx
    cases n <;> cases m
    · rfl
    · simp [hx.left] at h
    · simp [Ne.symm hx.left] at h
    · simp only [insertIdx_succ_cons, cons.injEq, true_and] at h
      rw [Nat.succ_inj]
      refine IH hx.right ?_ ?_ h
      · simpa [Nat.succ_le_succ_iff] using hn
      · simpa [Nat.succ_le_succ_iff] using hm

Goal state after: