mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered

Goal state before:
pp: case empty
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
U0 : Set ↑C.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 : U0 = ⋂ i ∈ G, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he ↦ ⋯.some
Vs : J → Set ↑(F.obj j) := fun e ↦ if h : e ∈ G then ⇑(ConcreteCategory.hom (F.map (g e h))) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ e ∈ G, Vs e
S : Set (Set ↑(F.obj j))
P : J → Set ↑(F.obj j)
he : Set.univ ∈ S
_hh : ∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S
⊢ (∀ e ∈ ∅, P e ∈ S) → ⋂ e ∈ ∅, P e ∈ S

Tactic:
simpa

Goal state after:
Module: Mathlib.Topology.ClopenBox

Goal state before:
pp: case refine_2
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : Countable (Clopens X)
⊢ inst✝³ = generateFrom {s | IsClopen s}

pp: case refine_3
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : SecondCountableTopology X
⊢ Countable (Clopens X)

Tactic:
· apply IsTopologicalBasis.eq_generateFrom
    exact loc_compact_Haus_tot_disc_of_zero_dim

Goal state after:
case refine_3
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : SecondCountableTopology X
⊢ Countable (Clopens X)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case fix
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
⊢ ∃ b₂,
    TrCfg (if v.headI = 0 then stepRet k v.tail else stepNormal f (Cont.fix f k) v.tail) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (Λ'.ret (trCont (Cont.fix f k))), var := s,
          stk := elim (trList v) [] [] (trContStack (Cont.fix f k)) }
        b₂

Tactic:
have :
      if v.headI = 0 then natEnd ((trList v).head?.getD default) = true ∧
          (trList v).tail = trList v.tail
      else
        natEnd ((trList v).head?.getD default) = false ∧
          (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail := by
      obtain - | n := v
      · exact ⟨rfl, rfl⟩
      rcases n with - | n
      · simp
      rw [trList, List.headI, trNat, Nat.cast_succ, Num.add_one, Num.succ, List.tail]
      cases (n : Num).succ' <;> exact ⟨rfl, rfl⟩

Goal state after:
case fix
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
this :
  if v.headI = 0 then natEnd ((trList v).head?.getD default) = true ∧ (trList v).tail = trList v.tail
  else
    natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
⊢ ∃ b₂,
    TrCfg (if v.headI = 0 then stepRet k v.tail else stepNormal f (Cont.fix f k) v.tail) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (Λ'.ret (trCont (Cont.fix f k))), var := s,
          stk := elim (trList v) [] [] (trContStack (Cont.fix f k)) }
        b₂
Module: Mathlib.Logic.Function.FiberPartition

Goal state before:
pp: Y : Type u_2
Z : Type u_3
f : Y → Z
a : Fiber f
x : ↑↑a
⊢ f ↑x = image f a

Tactic:
have := a.2.choose_spec

Goal state after:
Y : Type u_2
Z : Type u_3
f : Y → Z
a : Fiber f
x : ↑↑a
this : (fun x ↦ f ⁻¹' {↑x}) (Exists.choose ⋯) = ↑a
⊢ f ↑x = image f a
Module: Mathlib.Logic.Function.FiberPartition

Goal state before:
pp: Y : Type u_2
Z : Type u_3
f : Y → Z
y : Y
a : Fiber f
h : f y = image f a
⊢ y ∈ ↑a

Tactic:
rw [a.eq_fiber_image]; exact h

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

Goal state before:
pp: X Y : LightCondSet
f : X ⟶ Y
⊢ IsLocallySurjective f ↔
    ∀ (S : LightProfinite) (y : Y.obj.obj (Opposite.op S)),
      ∃ S' φ,
        ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
          ∃ x,
            (ConcreteCategory.hom (f.hom.app (Opposite.op S'))) x = (ConcreteCategory.hom (Y.obj.map (Opposite.op φ))) y

Tactic:
exact LightCondensed.isLocallySurjective_iff_locallySurjective_on_lightProfinite _ f

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X Y : LightCondMod R
f : X ⟶ Y
⊢ IsLocallySurjective f ↔
    ∀ (S : LightProfinite) (y : ↑(Y.obj.obj (Opposite.op S))),
      ∃ S' φ,
        ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
          ∃ x,
            (ConcreteCategory.hom (f.hom.app (Opposite.op S'))) x = (ConcreteCategory.hom (Y.obj.map (Opposite.op φ))) y

Tactic:
exact LightCondensed.isLocallySurjective_iff_locallySurjective_on_lightProfinite _ f

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

Goal state before:
pp: t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β : Type u
η : ApplicativeTransformation F G
f : α → F β
x✝ : t α
⊢ traverse ((fun {α} ↦ η.app α) ∘ f) x✝ = ((fun {α} ↦ η.app α) ∘ traverse f) x✝

Tactic:
rw [comp_apply, naturality]

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α β : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β → β
xs : t α
x : β
⊢ (ConcreteCategory.hom (foldMap (Foldr.mk ∘ f) xs)) x =
    (TypeCat.Hom.hom ((Foldr.ofFreeMonoid f) (FreeMonoid.ofList (FreeMonoid.toList (foldMap FreeMonoid.of xs))))) x

Tactic:
FreeMonoid.ofList_toList,

Goal state after:
α β : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β → β
xs : t α
x : β
⊢ (ConcreteCategory.hom (foldMap (Foldr.mk ∘ f) xs)) x =
    (TypeCat.Hom.hom ((Foldr.ofFreeMonoid f) (foldMap FreeMonoid.of xs))) x
Module: Mathlib.Data.TypeVec

Goal state before:
pp: α : TypeVec.{u_1} 0
β : TypeVec.{u_2} 0
f : α ⟹ β
⊢ f = nilFun

Tactic:
by
  ext x; cases x

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: α : TypeVec.{u_1} 0
⊢ id = nilFun

Tactic:
by
  ext x; cases x

Goal state after:
Module: Mathlib.Data.FP.Basic

Goal state before:
pp: C : FloatCfg
n d : ℕ+
⊢ Float × Bool

Tactic:
let e₁ : ℤ := n.1.size - d.1.size - prec

Goal state after:
C : FloatCfg
n d : ℕ+
e₁ : ℤ := ↑(↑n).size - ↑(↑d).size - ↑prec
⊢ Float × Bool
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
⊢ take m h (update v i x) = take m h v

Tactic:
ext j
  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)
  simp only [take, update_of_ne this]

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝¹ : FinEnum α
p : α → Prop
inst✝ : DecidablePred p
x : α
h : p x
⊢ ⟨x, h⟩ ∈ List.filterMap (fun x ↦ if h : p x then some ⟨x, h⟩ else none) (toList α)

Tactic:
simpa

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

Goal state before:
pp: α : Type u
β : α → Type v
a : α
l : List (Sigma β)
h : a ∈ l.keys
⊢ ∃ b, ⟨a, b⟩ ∈ l

Tactic:
have := exists_of_mem_map h
  grind

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:
rw [keys, ← List.dlookup_isSome, h']

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✝
⊢ (some y✝).isSome = true
Module: Mathlib.Data.Finmap

Goal state before:
pp: case refine_2
α : Type u
β : α → Type v
γ : Type ?u.32
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
⊢ (Quotient.liftOn s.entries (fun l ↦ { Dom := l.NodupKeys, get := fun nd ↦ f { entries := l, nodupKeys := nd } })
      ⋯).Dom

Tactic:
have := s.nodupKeys
    revert this
    rcases s.entries with ⟨l⟩
    exact id

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

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

Tactic:
rw [keys, ← List.dlookup_isSome, h']

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
⊢ (some y✝).isSome = true
Module: Mathlib.Data.Finset.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : DenselyOrdered α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

Tactic:
by
  convert! _root_.exists_between (a₁ := s.max' hs) (a₂ := t.min' ht) (by simp_all) <;> simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : DenselyOrdered α
s t : Set α
hsf : s.Finite
hs : s.Nonempty
htf : t.Finite
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ hsf.toFinset.Nonempty

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : DenselyOrdered α
s t : Set α
hsf : s.Finite
hs : s.Nonempty
htf : t.Finite
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ htf.toFinset.Nonempty

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : DenselyOrdered α
s t : Set α
hsf : s.Finite
hs : s.Nonempty
htf : t.Finite
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ ∀ x ∈ hsf.toFinset, ∀ y ∈ htf.toFinset, x < y

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
s t : Set α
hs : s.Finite
ht : t.Finite
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ ∀ x ∈ hs.toFinset, ∀ y ∈ ht.toFinset, x < y

Tactic:
simpa

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : a ∈ xs.toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ xs
⊢ a ∈ (x :: xs).toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ x :: xs

Tactic:
| cons x xs =>

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:
| cons x xs =>

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Pi

Goal state before:
pp: case insert.refine_1.inl
α : Type u_1
ι : Type u_2
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
s : Finset ι
ih : (s.inf fun i ↦ (t i).sup (f i)) = (s.pi t).sup fun g ↦ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)
c : α
g : (a : ι) → a ∈ s → κ a
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
j : ι
hi : j ∉ s
h :
  ∀ (b : (a : ι) → a ∈ insert j s → κ a),
    (∀ (a : ι) (h : a ∈ insert j s), b a h ∈ t a) →
      f j (b j ⋯) ⊓ s.attach.inf ((fun i ↦ f (↑i) (b ↑i ⋯)) ∘ fun x ↦ ⟨↑x, ⋯⟩) ≤ c
a : κ j
ha : a ∈ t j
aux : ∀ (j_1 : ↥s), ↑j_1 ≠ j
hj : j ∈ insert j s
⊢ (if hji : j = j then cast ⋯ a else g j ⋯) ∈ t j

Tactic:
simpa

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

Goal state before:
pp: case true
n : ℕ
⊢ 2 * -[n.div2+1] = -[1 + 2 * n.div2+1]

Tactic:
add_comm

Goal state after:
case true
n : ℕ
⊢ 2 * -[n.div2+1] = -[2 * n.div2 + 1+1]
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : y₁.CPRankMax1
hy₂ : CPRankMax n y₂
⊢ CPRankMax (1 + n) (x ⊗ y₁ + x ⊗ y₂)

Tactic:
apply cprankMax_add

Goal state after:
case a
α : Type
d : ℕ
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : y₁.CPRankMax1
hy₂ : CPRankMax n y₂
⊢ CPRankMax 1 (x ⊗ y₁)

case a
α : Type
d : ℕ
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : y₁.CPRankMax1
hy₂ : CPRankMax n y₂
⊢ CPRankMax n (x ⊗ y₂)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: n k : ℕ
⊢ (↑n).lnot.testBit k = !(↑n).testBit k

Tactic:
simp [lnot, testBit]

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

Goal state before:
pp: n k : ℕ
⊢ -[n+1].lnot.testBit k = !-[n+1].testBit k

Tactic:
simp [lnot, testBit]

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

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
| ⌈(↑b - (↑r * ↑(v / r) + ↑(v % r))) / ↑r⌉ - ⌈(↑0 - (↑r * ↑(v / r) + ↑(v % r))) / ↑r⌉

Tactic:
add_comm

Goal state after:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
| ⌈(↑b - (↑(v % r) + ↑r * ↑(v / r))) / ↑r⌉ - ⌈(↑0 - (↑(v % r) + ↑r * ↑(v / r))) / ↑r⌉
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
| ⌈(↑b - ↑(v % r)) / ↑r⌉ - ↑(v / r) - (⌈(↑0 - ↑(v % r)) / ↑r⌉ - ↑(v / r))

Tactic:
rw [sub_sub_sub_cancel_right, cast_zero, zero_sub]

Goal state after:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
| ⌈(↑b - ↑(v % r)) / ↑r⌉ - ⌈-↑(v % r) / ↑r⌉
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
| ⌈(↑(b % r) - ↑(v % r)) / ↑r⌉ + ↑(b / r)

Tactic:
add_comm

Goal state after:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
| ↑(b / r) + ⌈(↑(b % r) - ↑(v % r)) / ↑r⌉
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n : ℕ
⊢ Ico 0 n = range n

Tactic:
rw [Ico, Nat.sub_zero, range_eq_range']

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

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

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
⊢ Set.range (foldr f a) ⊆ Set.range (foldr g a)

Tactic:
rintro _ ⟨l, rfl⟩
  induction l with
  | nil => exact ⟨[], rfl⟩
  | cons b l H =>
    obtain ⟨c, hgf⟩ := hfg (Set.mem_range_self b)
    obtain ⟨m, hgf'⟩ := H
    rw [foldr_cons, ← hgf, ← hgf']
    exact ⟨c :: m, rfl⟩

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

Goal state before:
pp: α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
⊢ i < (sz.splitLengths l).length

Tactic:
simpa

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

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

Tactic:
intro i hi

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.SplitBy

Goal state before:
pp: case h_2.hga
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs →
        (∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false) →
          IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs
hga : ∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x✝ : Bool
heq✝ : r a b = false
⊢ ∀ (m : List α), m ∈ ((a :: g).reverse :: gs).head? → ∃ ha hb, r (m.getLast ha) (([].reverse ++ [b]).head hb) = false

Tactic:
simpa

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

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Bool
⊢ IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy r [])

Tactic:
exact isChain_nil

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

Goal state before:
pp: α : Type u_1
m : List α
r : α → α → Bool
l : List (List α)
⊢ splitBy r m = l ↔
    m = l.flatten ∧
      ¬[] ∈ l ∧
        (∀ (m : List α), m ∈ l → IsChain (fun x y ↦ r x y = true) m) ∧
          IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) l

Tactic:
constructor
  · rintro rfl
    exact ⟨(flatten_splitBy r m).symm, nil_notMem_splitBy r m, fun _ ↦ isChain_of_mem_splitBy,
      isChain_getLast_head_splitBy r m⟩
  · rintro ⟨rfl, hn, hc, hc'⟩
    exact splitBy_flatten hn hc hc'

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

Goal state before:
pp: α : Type u_1
r : α → α → Bool
l : List α
a : α
m : List α
ha : ∀ (x : α), x ∈ l.getLast? → r x a = false
⊢ ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ (a :: m).head? → r x y = false

Tactic:
simpa

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B : Matrix n m R
⊢ A₁.fromRows A₂ * B = (A₁ * B).fromRows (A₂ * B)

Tactic:
ext (_ | _) _ <;> simp [mul_apply]

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n₁
inst✝ : Fintype n₂
A₁ : Matrix n₁ n R
A₂ : Matrix n₂ n R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
⊢ fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂ = (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂)

Tactic:
ext (_ | _) _ <;> simp [mul_apply]

Goal state after:
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case right
α : Type u_1
inst✝ : Preorder α
M N X Y : Multiset α
a : α
M_def : M = X + Y
N_def : N = X + {a}
ys_lt_a : ∀ (y : α), y ∈ Y → y < a
⊢ ∀ (y : α), y ∈ Y → ∃ z, z ∈ {a} ∧ y < z

Tactic:
simpa

Goal state after:
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case inr.refine_1
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : {a} + M = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ X + Y = a ::ₘ (Y + (M - {b}))

Tactic:
add_comm

Goal state after:
case inr.refine_1
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : M + {a} = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ X + Y = a ::ₘ (Y + (M - {b}))
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
M N : Multiset α
hMN : TransGen OneStep M N
X Y : Multiset α
a : α
hYa : ∀ (y : α), y ∈ Y → y < a
⊢ {a} ≠ ∅ ∧ X + Y = X + Y ∧ X + {a} = X + {a} ∧ ∀ (y : α), y ∈ Y → ∃ z, z ∈ {a} ∧ y < z

Tactic:
simpa

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

Goal state before:
pp: a : ℚ≥0
b : ℕ
⊢ (fun q ↦ ⌈↑q⌉₊) a ≤ b ↔ a ≤ ↑b

Tactic:
rw [← NNRat.coe_le_coe, Nat.ceil_le]

Goal state after:
a : ℚ≥0
b : ℕ
⊢ ↑a ≤ ↑b ↔ ↑a ≤ ↑↑b
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: case inr.refine_1
K : Type u_1
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
x : ℚ≥0
hx : x ≠ 0
⊢ ⌈x⌉₊ ≠ 0

Tactic:
simpa

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

Goal state before:
pp: case inr.refine_2
K : Type u_1
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
x : ℚ≥0
hx : x ≠ 0
⊢ ⌈x⌉₊ ≠ 0

Tactic:
simpa

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ⌊↑x⌋ = ⌊↑x⌋

Tactic:
rw [Int.floor_eq_iff, ← coe_floor]
  norm_cast
  norm_cast
  rw [Nat.cast_add_one, ← Nat.floor_eq_iff zero_le]

Goal state after:
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: A : Type u_1
inst✝ : Semiring A
m k : ℕ
hn_fac : IsUnit ↑(m + k)!
⊢ IsUnit ↑m !

Tactic:
induction k generalizing m with
  | zero => simpa using hn_fac
  | succ k ih =>
    rw [← add_assoc, add_right_comm] at hn_fac
    have := ih hn_fac
    rw [Nat.factorial_succ, Nat.cast_mul, Nat.cast_commute _ _ |>.isUnit_mul_iff] at this
    exact this.2

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n.greatestFib ≠ 0

Tactic:
simpa

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

Goal state before:
pp: a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun a b ↦ b + 2 ≤ a) (l ++ [0])
ha : 0 < a
n : ℕ
hn : a < n
x✝ : n ≤ (map fib l).sum + (fib a + 1)
⊢ ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n

Tactic:
simpa

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

Goal state before:
pp: p : ℕ → Prop
hf : (Set.ofPred p).Finite
⊢ StrictMonoOn (nth p) (Set.Iio #hf.toFinset)

Tactic:
rintro m (hm : m < _) n (hn : n < _) h

Goal state after:
p : ℕ → Prop
hf : (Set.ofPred p).Finite
m : ℕ
hm : m < #hf.toFinset
n : ℕ
hn : n < #hf.toFinset
h : m < n
⊢ nth p m < nth p n
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt : ∀ (hf : (Set.ofPred p).Finite), k + 1 < #hf.toFinset
⊢ {n ∈ range (nth p (k + 1)) | p n} = insert (nth p k) ({n ∈ range (nth p k) | p n})

Tactic:
refine (filter_range_nth_subset_insert p k).antisymm fun a ha => ?_

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt : ∀ (hf : (Set.ofPred p).Finite), k + 1 < #hf.toFinset
a : ℕ
ha : a ∈ insert (nth p k) ({n ∈ range (nth p k) | p n})
⊢ a ∈ {n ∈ range (nth p (k + 1)) | p n}
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ℕ
⊢ ZNum.ofInt' (↑n + 1) = ZNum.ofInt' ↑n + 1

Tactic:
change ZNum.ofInt' (n + 1 : ℕ) = ZNum.ofInt' (n : ℕ) + 1
    dsimp only [ZNum.ofInt', ZNum.ofInt']
    rw [Num.ofNat'_succ, Num.add_one, toZNum_succ, ZNum.add_one]

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(↑a + ↑b) = ↑(↑b + ↑a)

Tactic:
add_comm

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(↑b + ↑a) = ↑(↑b + ↑a)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: l r : ℕ
⊢ l + r ≤ 1 → r + l ≤ 1

Tactic:
add_comm

Goal state after:
l r : ℕ
⊢ r + l ≤ 1 → r + l ≤ 1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case none
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
e : Num.ofZNum' (r.sub' (Num.pos d)) = none
h :
  ↑d ≤
    ↑(match none with
        | some r' => (q.bit1, r')
        | none => (q.bit0, r)).2
r₂ : ℕ
e' :
  ↑d + ↑↑r₂ =
    ↑(match none with
        | some r' => (q.bit1, r')
        | none => (q.bit0, r)).2
⊢ False

Tactic:
add_comm

Goal state after:
case none
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
e : Num.ofZNum' (r.sub' (Num.pos d)) = none
h :
  ↑d ≤
    ↑(match none with
        | some r' => (q.bit1, r')
        | none => (q.bit0, r)).2
r₂ : ℕ
e' :
  ↑↑r₂ + ↑d =
    ↑(match none with
        | some r' => (q.bit1, r')
        | none => (q.bit0, r)).2
⊢ False