mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos.mpr.inr.inl.case
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
h₁ : y ∈ approx (⇑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (⇑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (⇑f) i a → ∀ (j : ℕ), y ∈ approx (⇑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : i ≤ j
⊢ i ≤ j

Tactic:
assumption

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos.mpr.inr.inr.h₀
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
h₁ : y ∈ approx (⇑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (⇑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (⇑f) i a → ∀ (j : ℕ), y ∈ approx (⇑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : j ≤ i
⊢ ∃ i, (approx (⇑?pos.mpr.inr.inr.f✝) i a).Dom

Tactic:
assumption

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos.mpr.inr.inr.hh
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
h₁ : y ∈ approx (⇑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (⇑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (⇑f) i a → ∀ (j : ℕ), y ∈ approx (⇑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : j ≤ i
⊢ y ∈ approx ⇑f ?pos.mpr.inr.inr.i✝ a

Tactic:
assumption

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos.mpr.inr.inr.h₁
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
h₁ : y ∈ approx (⇑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (⇑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (⇑f) i a → ∀ (j : ℕ), y ∈ approx (⇑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : j ≤ i
⊢ b ∈ approx ⇑f ?pos.mpr.inr.inr.j✝ a

Tactic:
assumption

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos.mpr.inr.inr.case
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
h₁ : y ∈ approx (⇑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (⇑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (⇑f) i a → ∀ (j : ℕ), y ∈ approx (⇑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : j ≤ i
⊢ j ≤ i

Tactic:
assumption

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case a
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ ωSup ((approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ }) ≤
    ωSup (approxChain { toFun := g, monotone' := ⋯ })

Tactic:
apply ωSup_le_ωSup_of_le _
    intro i
    exists i.succ

Goal state after:
Module: Mathlib.Data.BitVec

Goal state before:
pp: w : ℕ
z : ℤ
x : BitVec w
⊢ (↑z).toFin * x.toFin = z • x.toFin

Tactic:
open scoped Fin.CommRing in
    simp only [zsmul_eq_mul, toFin_intCast]

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 α
m : α → Filter β
F : f✝.Realizer
G : (i : α) → (m i).Realizer
x✝ : (s : F.σ) × ((i : α) → i ∈ F.F.f s → (G i).σ)
s : F.σ
f : (i : α) → i ∈ F.F.f s → (G i).σ
i : α
h✝ : i ∈ F.F.f s
⊢ i ∈ F.F.f s

Tactic:
assumption

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
a : Erased α
⊢ (map f a).out = f a.out

Tactic:
simp [map]

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

Goal state before:
pp: n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
i : Fin n
⊢ take n ⋯ v i = v i

Tactic:
simp [take]

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

Goal state before:
pp: case pos
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
⊢ ∃ g', (free R).map (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p

Tactic:
have : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd _ _)) := by
      rw [CompHausLike.mono_iff_injective]
      exact Subtype.val_injective

Goal state after:
case pos
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
this : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
⊢ ∃ g', (free R).map (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p
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₁.entries.keys

Tactic:
← List.dlookup_isSome,

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✝
⊢ (dlookup x✝ s₁.entries).isSome = true
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₂.entries.keys

Tactic:
← List.dlookup_isSome,

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
⊢ (dlookup x✝ s₂.entries).isSome = true
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case neg.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ a ≠ ⟨a', b⟩.fst

Tactic:
assumption

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
x y z : Finmap β
⊢ (y ∪ z).Disjoint x ↔ x.Disjoint y ∧ x.Disjoint z

Tactic:
disjoint_union_left,

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x y z : Finmap β
⊢ y.Disjoint x ∧ z.Disjoint x ↔ x.Disjoint y ∧ x.Disjoint z
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
s : Finset α
⊢ traverse pure s = pure s

Tactic:
traverse,

Goal state after:
α : Type u
inst✝ : DecidableEq α
s : Finset α
⊢ Multiset.toFinset <$> Multiset.traverse pure s.val = pure s
Module: Mathlib.Data.Int.Fib.Lemmas

Goal state before:
pp: n : ℕ
⊢ fib (↑n + 1) * fib (↑n - 1) - fib ↑n ^ 2 = (-1) ^ n

Tactic:
by
  induction n with
  | zero => simp
  | succ _ _ => grind [fib_add_two]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: case a
α : Type
ds : List ℕ
inst✝¹ : Mul α
inst✝ : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : x₁.CPRankMax1
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
⊢ x₁.CPRankMax1

Tactic:
assumption

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
x : Holor α [d]
⊢ CPRankMax 0 (x ⊗ 0)

Tactic:
by simp [mul_zero x, CPRankMax.zero]

Goal state after:
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:
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.true.inr
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hp : p hd = true
hx : x ∈ takeWhile p tl
⊢ p x = true

Tactic:
exact IH hx

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

Goal state before:
pp: case nil
α : Type u_1
l : List α
⊢ [].reverse = []

Tactic:
try (exact rfl)

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

Goal state before:
pp: case singleton
α : Type u_1
l : List α
x✝ : α
⊢ [x✝].reverse = [x✝]

Tactic:
try (exact rfl)

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:
try (exact rfl)

Goal state after:
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✝])
Module: Mathlib.Data.List.Lemmas

Goal state before:
pp: case cons.succ.succ.refine_2
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : tl.insertIdx n✝¹ x = tl.insertIdx n✝ x
⊢ n✝ ∈ {n | n ≤ tl.length}

Tactic:
simpa [Nat.succ_le_succ_iff] using hm

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

Goal state before:
pp: case refine_1
α : Type u_1
L : List (List α)
f : List α
h : f ∈ L.sections
⊢ Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f L

Tactic:
induction L generalizing f

Goal state after:
case refine_1.nil
α : Type u_1
f : List α
h : f ∈ [].sections
⊢ Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f []

case refine_1.cons
α : Type u_1
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ {f : List α}, f ∈ tail✝.sections → Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f tail✝
f : List α
h : f ∈ (head✝ :: tail✝).sections
⊢ Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f (head✝ :: tail✝)
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s₁ s₂ t : List α
h : Shortlex r s₁ s₂
⊢ Shortlex r s₁ (s₂ ++ t)

Tactic:
rcases shortlex_def.mp h with h1 | h2
  · apply of_length_lt
    rw [List.length_append]
    lia
  cases t with
  | nil =>
    rw [List.append_nil]
    exact h
  | cons head tail =>
    apply of_length_lt
    rw [List.length_append, List.length_cons]
    lia

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

Goal state before:
pp: case cons
α : Type u_1
i : ℕ
hi : ∀ (l : List α) (sz : List ℕ), take i (sz.splitLengths l) = (take i sz).splitLengths l
l : List α
head✝ : ℕ
tail✝ : List ℕ
⊢ take (i + 1) ((head✝ :: tail✝).splitLengths l) = (take (i + 1) (head✝ :: tail✝)).splitLengths l

Tactic:
· simp only [splitLengths_cons, take_succ_cons, hi]

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

Goal state before:
pp: case intro.intro.inr.rel
α : 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)
h2len : (x :: xs).length = (xa :: xb).length
h : r x xa
⊢ Acc (Shortlex r) (x :: xs)

Tactic:
simp only [List.length_cons, add_left_inj] at h2len
          refine iha _ h (ih xs (by rw [h2len]; simp)) fun l hl => ?_
          apply ih
          rw [List.length_cons, ← h2len]
          exact hl

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

Goal state before:
pp: case mp
α : Type u_1
p : ℕ
w : List α
per : w.HasPeriod p
i : ℕ
len : i < w.length
⊢ w[i]? = w[i % p]?

Tactic:
exact Eq.symm (per.getElem?_mod p i w len)

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

Goal state before:
pp: case inr.inr
α : 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
⊢ (take n w ++ w).HasPeriod p

Tactic:
rw [hasPeriod_iff_forall_getElem?_mod]

Goal state after:
case inr.inr
α : 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
⊢ ∀ i < (take n w ++ w).length, (take n w ++ w)[i]? = (take n w ++ w)[i % p]?
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: case succ
A : Type u_1
inst✝² : Ring A
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP A p
hp : Nat.Prime p
n : ℕ
ih : IsUnit ↑n ! ↔ n < p
⊢ IsUnit ↑(n + 1)! ↔ n + 1 < p

Tactic:
rw [factorial_succ, cast_mul, Nat.cast_commute _ _ |>.isUnit_mul_iff, ih.symm.symm,
      ← Nat.add_one_le_iff, CharP.isUnit_natCast_iff hp]
    exact ⟨fun ⟨h1, h2⟩ ↦ lt_of_le_of_ne h2 (mt (· ▸ dvd_rfl) h1),
      fun h ↦ ⟨not_dvd_of_pos_of_lt (Nat.succ_pos _) h, h.le⟩⟩

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

Goal state before:
pp: k n m : ℕ
⊢ (n * k).dist (m * k) = k * n.dist m

Tactic:
dist_mul_right,

Goal state after:
k n m : ℕ
⊢ n.dist m * k = k * n.dist m
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
⊢ (∑ i ∈ range (n % p + 1),
          ∑ j ∈ range (n / p + 1), X ^ i * ↑((n % p).choose i) * (X ^ (p * j) * ↑((n / p).choose j))).coeff
      k =
    (Int.castRingHom (ZMod p)) (↑((n % p).choose (k % p)) * ↑((n / p).choose (k / p)))

Tactic:
conv_lhs =>
    enter [1, 2, k, 2, k']
    rw [← mul_assoc, mul_right_comm _ _ (X ^ (p * k')), ← pow_add, mul_assoc, ← cast_mul]

Goal state after:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
⊢ (∑ k ∈ range (n % p + 1), ∑ k' ∈ range (n / p + 1), X ^ (k + p * k') * ↑((n % p).choose k * (n / p).choose k')).coeff
      k =
    (Int.castRingHom (ZMod p)) (↑((n % p).choose (k % p)) * ↑((n / p).choose (k / p)))
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: i j : ℕ
⊢ i.dist j = max i j - min i j

Tactic:
by
  cases le_total i j <;> simp [Nat.dist, *]

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

Goal state before:
pp: case neg
p : ℕ → Prop
n : ℕ
hf : (Set.ofPred p).Finite
hn : #⋯.toFinset ≤ n
⊢ nth p n = sInf {x | p x ∧ ∀ k < n, nth p k < x}

Tactic:
rw [nth_of_card_le _ hn]

Goal state after:
case neg
p : ℕ → Prop
n : ℕ
hf : (Set.ofPred p).Finite
hn : #⋯.toFinset ≤ n
⊢ 0 = sInf {x | p x ∧ ∀ k < n, nth p k < x}
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: case mp.refl
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h' : ∀ (i : P.B a), p (f i)
⊢ ∀ (i : P.B a), p (f i)

Tactic:
assumption

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
⊢ ↑n.bitm1 = ↑n + ↑n - 1

Tactic:
conv =>
    lhs
    rw [← zneg_zneg n]
  rw [← zneg_bit1, cast_zneg, cast_bit1]
  have : ((-1 + n + n : ℤ) : α) = (n + n + -1 : ℤ) := by simp [add_comm]
  simpa [sub_eq_add_neg] using this

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

Goal state before:
pp: p : PosNum
⊢ ↑p.bit1 = ZNum.pos p.bit1

Tactic:
have := congr_arg ZNum.bit1 (cast_to_znum p)
      rwa [← ZNum.bit1_of_bit1] at this

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

Goal state before:
pp: case mpr.h.h.right
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ∀ (i : P.B a), p (f i)

Tactic:
assumption

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

Goal state before:
pp: p : PosNum
⊢ (pos p).toZNum = ZNum.pos p

Tactic:
toZNum

Goal state after:
p : PosNum
⊢ ZNum.pos p = ZNum.pos p
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: case mp
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
right✝ : ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
⊢ ∀ (i : Fin2 n) (x : P.B a i), p (f i x)

Tactic:
assumption

Goal state after:
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: case mpr.h.h.right
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)

Tactic:
assumption

Goal state after:
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: case mpr
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
⊢ (∀ (i : Fin2 n) (x : P.B a i), p (f i x)) →
    ∃ a_2 f_1, ⟨a, f⟩ = ⟨a_2, f_1⟩ ∧ ∀ (i : Fin2 n) (j : P.B a_2 i), p (f_1 i j)

Tactic:
· intro
    repeat' first | constructor | assumption

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

Goal state before:
pp: case neg.inr
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : ¬rl.size < ratio * rr.size
rl0 : rl.size > 0
⊢ Valid' o₁ (l.node4L x rl rx rr) o₂

Tactic:
refine hl.node4L hr.left hr.right rl0 ?_

Goal state after:
case neg.inr
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : ¬rl.size < ratio * rr.size
rl0 : rl.size > 0
⊢ l.size = 0 ∧ rl.size = 1 ∧ rr.size ≤ 1 ∨
    0 < l.size ∧
      ratio * rr.size ≤ rl.size ∧
        delta * l.size ≤ rl.size + rr.size ∧ 3 * (rl.size + rr.size) ≤ 16 * l.size + 9 ∧ rl.size ≤ delta * rr.size
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a₃ : ι
b₃ : α a₃
a✝¹ : a₁ < a₂
a✝ : a₂ < a₃
⊢ a₁ < ?left.left.b

Tactic:
assumption

Goal state after:
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case left.left.a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a₃ : ι
b₃ : α a₃
a✝¹ : a₁ < a₂
a✝ : a₂ < a₃
⊢ a₂ < a₃

Tactic:
assumption

Goal state after:
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case left.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a✝¹ : a₁ < a₂
b₂✝ : α a₂
a✝ : b₂ ≤ b₂✝
⊢ a₁ < a₂

Tactic:
assumption

Goal state after:
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case right.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁ : ι
b₁ : α a₁
a₃ : ι
b₃ : α a₃
b₂✝ : α a₁
a✝¹ : b₁ ≤ b₂✝
a✝ : a₁ < a₃
⊢ a₁ < a₃

Tactic:
assumption

Goal state after:
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁ : ι
b₁ b₂✝¹ : α a₁
a✝¹ : b₁ ≤ b₂✝¹
b₂✝ : α a₁
a✝ : b₂✝¹ ≤ b₂✝
⊢ b₁ ≤ ?right.right.b

Tactic:
assumption

Goal state after:
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case right.right.a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁ : ι
b₁ b₂✝¹ : α a₁
a✝¹ : b₁ ≤ b₂✝¹
b₂✝ : α a₁
a✝ : b₂✝¹ ≤ b₂✝
⊢ b₂✝¹ ≤ b₂✝

Tactic:
assumption

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

Goal state before:
pp: case node.node
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
sl : (node ls ll lx lr).Sized
H1 : (node ls ll lx lr).size = 0 → (node rs rl rx rr).size ≤ 1
H2 :
  1 ≤ (node ls ll lx lr).size → 1 ≤ (node rs rl rx rr).size → (node rs rl rx rr).size ≤ delta * (node ls ll lx lr).size
⊢ (node ls ll lx lr).balanceL x (node rs rl rx rr) = (node ls ll lx lr).balance x (node rs rl rx rr)

Tactic:
replace H2 : ¬rs > delta * ls := not_lt_of_ge (H2 sl.pos sr.pos)

Goal state after:
case node.node
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
sl : (node ls ll lx lr).Sized
H1 : (node ls ll lx lr).size = 0 → (node rs rl rx rr).size ≤ 1
H2 : ¬rs > delta * ls
⊢ (node ls ll lx lr).balanceL x (node rs rl rx rr) = (node ls ll lx lr).balance x (node rs rl rx rr)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ recF g ((P F).wMk a f' f) = g (abs ⟨a, splitFun f' (recF g ∘ f)⟩)

Tactic:
recF,

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ (P F).wRec (fun a f' _f rec ↦ g (abs ⟨a, splitFun f' rec⟩)) ((P F).wMk a f' f) = g (abs ⟨a, splitFun f' (recF g ∘ f)⟩)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
⊢ rec g = h

Tactic:
ext x
  apply Fix.ind_rec
  intro x hyp'
  rw [hyp, ← hyp', Fix.rec_eq]

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)
⊢ rec g = h

Tactic:
ext x
  apply Fix.ind_rec
  intro x hyp'
  rw [hyp, ← hyp', Fix.rec_eq]

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR' (α.RelLast' r) x.dest y.dest
x✝ y✝ : Cofix F α
a✝ : r x✝ y✝
⊢ r x✝ y✝

Tactic:
assumption

Goal state after:
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inl
⊢ 0⁻¹.sign = sign 0

pp: case inr.inr
r : ℝ
hp : 0 < r
⊢ r⁻¹.sign = r.sign

Tactic:
· rw [sign_zero, inv_zero, sign_zero]

Goal state after:
case inr.inr
r : ℝ
hp : 0 < r
⊢ r⁻¹.sign = r.sign