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

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

Tactic:
induction x

Goal state after:
case nil
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
⊢ (fun {α} ↦ η.app α) (List.traverse f []) = List.traverse ((fun {α} ↦ η.app α) ∘ f) []

case cons
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
head✝ : α
tail✝ : List α
tail_ih✝ : (fun {α} ↦ η.app α) (List.traverse f tail✝) = List.traverse ((fun {α} ↦ η.app α) ∘ f) tail✝
⊢ (fun {α} ↦ η.app α) (List.traverse f (head✝ :: tail✝)) = List.traverse ((fun {α} ↦ η.app α) ∘ f) (head✝ :: tail✝)
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: σ α β : Type u
f : α → β
x : σ ⊕ α
⊢ Sum.traverse (pure ∘ f) x = pure (f <$> x)

Tactic:
induction x

Goal state after:
case inl
σ α β : Type u
f : α → β
val✝ : σ
⊢ Sum.traverse (pure ∘ f) (inl val✝) = pure (f <$> inl val✝)

case inr
σ α β : Type u
f : α → β
val✝ : α
⊢ Sum.traverse (pure ∘ f) (inr val✝) = pure (f <$> inr val✝)
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
n✝ : ℕ
i_ih : approx (⇑f) n✝ ≤ approx (⇑f) n✝.succ
⊢ approx (⇑f) (n✝ + 1) ≤ approx (⇑f) (n✝ + 1).succ

Tactic:
| succ _ i_ih =>

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
X : (a : α) → Part (β a)
hX : f X ≤ X
n✝ : ℕ
i_ih : { toFun := approx ⇑f, monotone' := ⋯ } n✝ ≤ X
⊢ { toFun := approx ⇑f, monotone' := ⋯ } (n✝ + 1) ≤ X

Tactic:
| succ _ i_ih =>

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

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
α : Type u
x : t' α
⊢ Equiv.map eqv id x = x

Tactic:
simp [Equiv.map, id_map]

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

Goal state before:
pp: case neg
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)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property✝ : π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).1 = π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).2
h : ¬(π t).2 = none
⊢ ∃ a, coverToFun (fibreIncl π σ) (π_r π σ) a = ⟨(⟨t, ht⟩, ⟨t', ht'⟩), property✝⟩

Tactic:
· obtain ⟨n, hn⟩ := Option.ne_none_iff_exists'.mp h
    exact ⟨Sum.inl ⟨σ n (π t).1, by grind⟩, by grind⟩

Goal state after:
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
inst✝ : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : t.support ⊆ s
i : ι
h : f i ∈ 0
hi : i ∈ f.support
H : t i = 0
⊢ f i = 0

Tactic:
mem_zero

Goal state after:
case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
inst✝ : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : t.support ⊆ s
i : ι
h : f i = 0
hi : i ∈ f.support
H : t i = 0
⊢ f i = 0
Module: Mathlib.Data.Fin.Tuple.Take

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

Tactic:
ext i
  simp [take]

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

Goal state before:
pp: α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ s₁.keys
this✝ : DecidableEq α := Classical.decEq α
this : (lookup k s₁).get ⋯ ∈ lookup k s₂
⊢ k ∈ s₂.keys

Tactic:
Option.mem_def

Goal state after:
α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ s₁.keys
this✝ : DecidableEq α := Classical.decEq α
this : lookup k s₂ = some ((lookup k s₁).get ⋯)
⊢ k ∈ s₂.keys
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
l₁ l₂ : List (Sigma β)
⊢ (l₁ ++ l₂).keys = l₁.keys ++ l₂.keys

Tactic:
simp [keys]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
a : α
b : β a
s : Multiset (Sigma β)
⊢ (⟨a, b⟩ ::ₘ s).keys = a ::ₘ s.keys

Tactic:
simp [keys]

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 : α), lookup x ⟦s₁⟧ = lookup x ⟦s₂⟧
⊢ ⟦s₁⟧ = ⟦s₂⟧

Tactic:
simp only [AList.lookup, lookup_toFinmap] at h
    rw [AList.toFinmap_eq]
    apply lookup_ext s₁.nodupKeys s₂.nodupKeys
    intro x y
    rw [h]

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

Goal state before:
pp: α β : Type u_1
h : α → β
x✝ : List α
⊢ (Functor.map h ∘ ofList) x✝ = (ofList ∘ Functor.map h) x✝

Tactic:
simp only [Function.comp_apply, fmap_def, map_coe, List.map_eq_map]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b b' : β a
s✝ : Finmap β
s : AList β
⊢ insert a b' (insert a b ⟦s⟧) = insert a b' ⟦s⟧

Tactic:
simp only [insert_toFinmap, AList.insert_insert]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
⊢ ∀ (a : α), a ∈ (⟦s₁⟧ ∪ ⟦s₂⟧).keys ↔ a ∈ ⟦s₁⟧.keys ∪ ⟦s₂⟧.keys

Tactic:
simp [keys]

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₂
ha₁ : ¬a₁ ∈ l.keys
⊢ kerase a₂ (kerase a₁ l) = kerase a₁ (kerase a₂ l)

Tactic:
by simp [ha₁, mt mem_keys_of_mem_keys_kerase ha₁]

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

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

Tactic:
simpa [ne_of_mem_of_not_mem hj hi] using! hg _ _

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:
by
  simp only [coe_pimage, coe_union, ← PFun.image_union]

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

Goal state before:
pp: case intro.a.inr
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hne : (univ.sigma f).Nonempty
⊢ p f

Tactic:
rcases sigma_nonempty.1 hne with ⟨i, -, hi⟩
    rcases H_ex i (f i) hi with ⟨x, x_mem, hr⟩
    set g := update f i ((f i).erase x) with hg
    clear_value g
    have hx' : x ∉ g i := by
      rw [hg, update_self]
      apply notMem_erase
    rw [show f = update g i (insert x (g i)) by
      rw [hg, update_idem, update_self, insert_erase x_mem, update_eq_self]] at hr ihs ⊢
    clear hg
    rw [update_self, erase_insert hx'] at hr
    refine step _ _ _ hr (ihs (univ.sigma g) ?_ _ rfl)
    rw [ssubset_iff_of_subset (sigma_mono (Subset.refl _) _)]
    exacts [⟨⟨i, x⟩, mem_sigma.2 ⟨mem_univ _, by simp⟩, by simp [hx']⟩,
      (@le_update_iff _ _ _ _ g g i _).2 ⟨subset_insert _ _, fun _ _ ↦ le_rfl⟩]

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

Goal state before:
pp: a b r v x : ℤ
⊢ (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔ ∃ a_1, ((a - v ≤ a_1 ∧ a_1 < b - v) ∧ r ∣ a_1) ∧ a_1 + v = x

Tactic:
← eq_sub_iff_add_eq,

Goal state after:
a b r v x : ℤ
⊢ (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔ ∃ a_1, ((a - v ≤ a_1 ∧ a_1 < b - v) ∧ r ∣ a_1) ∧ a_1 = x - v
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r v x : ℤ
⊢ (a < x ∧ x ≤ b) ∧ x ≡ v [ZMOD r] ↔ ∃ a_1, ((a - v < a_1 ∧ a_1 ≤ b - v) ∧ r ∣ a_1) ∧ a_1 + v = x

Tactic:
← eq_sub_iff_add_eq,

Goal state after:
a b r v x : ℤ
⊢ (a < x ∧ x ≤ b) ∧ x ≡ v [ZMOD r] ↔ ∃ a_1, ((a - v < a_1 ∧ a_1 ≤ b - v) ∧ r ∣ a_1) ∧ a_1 = x - v
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
x : α
⊢ (l ++ [x]).rdrop (n + 1) = l.rdrop n

Tactic:
simp [rdrop_eq_reverse_drop_reverse]

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

Goal state before:
pp: n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ ¬decide (k < l) = true

Tactic:
simp only [decide_eq_true_eq, not_lt]

Goal state after:
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ l ≤ k
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
⊢ filter (fun x ↦ decide (x < l)) (Ico n m) = Ico n (min m l)

Tactic:
rcases le_total m l with hml | hlm

Goal state after:
case inl
n m l : ℕ
hml : m ≤ l
⊢ filter (fun x ↦ decide (x < l)) (Ico n m) = Ico n (min m l)

case inr
n m l : ℕ
hlm : l ≤ m
⊢ filter (fun x ↦ decide (x < l)) (Ico n m) = Ico n (min m l)
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: case inr
n m l : ℕ
hln : l ≤ n
⊢ filter (fun x ↦ decide (l ≤ x)) (Ico n m) = Ico (max n l) m

Tactic:
max_eq_left hln,

Goal state after:
case inr
n m l : ℕ
hln : l ≤ n
⊢ filter (fun x ↦ decide (l ≤ x)) (Ico n m) = Ico n m
Module: Mathlib.Data.List.Shortlex

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

Tactic:
refine ihb _ (of_lex h2len h) fun l hl => ?_

Goal state after:
case intro.intro.inr.cons
α : 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
xs : List α
lt : Shortlex r (xa :: xs) (xa :: xb)
h : Lex r xs xb
h2len : xs.length = xb.length
l : List α
hl : l.length < (xa :: xs).length
⊢ Acc (Shortlex r) l
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: α : Type u_1
r : α → α → Prop
h : WellFounded r
a : List α
⊢ Acc (Shortlex r) a

Tactic:
by
  induction len_a : a.length using Nat.caseStrongRecOn generalizing a with
  | zero =>
    rw [List.length_eq_zero_iff] at len_a
    rw [len_a]
    exact Acc.intro _ <| fun _ ylt => (not_shortlex_nil_right ylt).elim
  | ind n ih =>
    obtain ⟨head, tail, rfl⟩ := List.exists_of_length_succ a len_a
    rw [List.length_cons, add_left_inj] at len_a
    apply Acc.shortlex (WellFounded.apply h head) (ih n le_rfl tail len_a)
    intro l ll
    apply ih l.length _ _ rfl
    rw [← len_a]
    exact Nat.le_of_lt_succ ll

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

Goal state before:
pp: case cons
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α},
    (∀ (b : α), b ∈ g.head? → r b a = true) →
      IsChain (fun y x ↦ r x y = true) g → m ∈ splitBy.loop r l a g [] → IsChain (fun x y ↦ r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
h : m ∈ splitBy.loop r (b :: l) a g []
⊢ IsChain (fun x y ↦ r x y = true) m

Tactic:
simp only [splitBy.loop, reverse_cons] at h
    split at h
    · apply IH _ (isChain_cons.2 ⟨hga, hg⟩) h
      grind
    · rw [splitByLoop_eq_append, mem_append, reverse_singleton, mem_singleton] at h
      obtain rfl | hm := h
      · apply List.isChain_reverse.1
        rw [reverse_append, reverse_cons, reverse_nil, nil_append, reverse_reverse]
        exact isChain_cons.2 ⟨hga, hg⟩
      · grind

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

Goal state before:
pp: α : 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_minus : j - n < w.length
n_le_j : n ≤ j
⊢ (j - n) % p = j % p

Tactic:
calc
          (j - n) % p = (j - p * (n / p)) % p := by rw [Nat.mul_div_cancel' dvd]
          _ = j % p := sub_mul_mod ((Nat.mul_div_cancel' dvd).symm ▸ n_le_j)

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
l : List ι
co : List.Pairwise (Coprime on s) l
hs : ∀ i ∈ l, s i ≠ 0
⊢ ↑(chineseRemainderOfList a s l co) < (List.map s l).prod

Tactic:
by
  cases l with
  | nil => simp
  | cons i l =>
    simp only [chineseRemainderOfList, List.map_cons, List.prod_cons]
    have : Coprime (s i) (l.map s).prod := by
      simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]
      intro j hj
      exact (List.pairwise_cons.mp co).1 j hj
    refine chineseRemainder_lt_mul this (a i) (chineseRemainderOfList a s l co.of_cons)
      (hs i List.mem_cons_self) ?_
    simp only [ne_eq, List.prod_eq_zero_iff, List.mem_map, not_exists, not_and]
    intro j hj
    exact hs j (List.mem_cons_of_mem _ hj)

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

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

Tactic:
simp [hp.pos]

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

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
n p : ℕ
h : p.Coprime n
m : ℕ
hm : ↑p ^ m = 0
⊢ ↑(↑(p ^ m) * (p ^ m).gcdA n + ↑n * (p ^ m).gcdB n) = ↑↑1

Tactic:
← (h.pow_left m).gcd_eq_one,

Goal state after:
A : Type u_1
inst✝ : CommRing A
n p : ℕ
h : p.Coprime n
m : ℕ
hm : ↑p ^ m = 0
⊢ ↑(↑(p ^ m) * (p ^ m).gcdA n + ↑n * (p ^ m).gcdB n) = ↑↑((p ^ m).gcd n)
Module: Mathlib.Data.Nat.Factorization.Divisors

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n.divisors =
    Finset.map { toFun := fun x ↦ (↑x).prod fun x1 x2 ↦ x1 ^ x2, inj' := ⋯ } (Finset.Iic n.factorization).attach

Tactic:
by
  rw [Finset.map_eq_image]
  change _ = (Finset.Iic n.factorization).attach.image ((·.prod (· ^ ·)) ∘ Subtype.val)
  rw [← Finset.image_image, Finset.attach_image_val]
  exact divisors_eq_image_Iic_factorization_prod_pow hn

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

Goal state before:
pp: case succ
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : MonotoneOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) → f n ≤ nth p n
hn : ∀ (hf : (Set.ofPred p).Finite), n + 1 < #hf.toFinset
⊢ f (n + 1) ≤ nth p (n + 1)

Tactic:
rw [nth_eq_sInf]
    refine le_csInf ?_ ?_
    · use nth p (n + 1), nth_mem _ hn
      exact fun k hk => nth_lt_nth' hk hn
    rintro b ⟨hb, h⟩
    rcases hsurj hb with ⟨m, hm, rfl⟩
    apply hmono hn hm
    rw [Nat.succ_le_iff]
    apply hmono.reflect_lt <;> grind

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

Goal state before:
pp: case nil.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rrs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩
        · exact node 3 (ι x) rx rr
        · exact
            if rls < ratio * rrs then node (rs + 1) (node (rls + 1) nil x rl) rx rr
            else
              node (rs + 1) (node (size rll + 1) nil x rll) rlx
                (node (size rlr + rrs + 1) rlr rx rr)

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

Goal state before:
pp: p : ℕ → Prop
m n : ℕ
h0 : ∀ k < m, ¬p k
h : nth p n ≠ 0
k : ℕ
hk : p k
hn : k ∉ Set.range fun x ↦ id x + m
⊢ False

Tactic:
simp_rw [id_eq, Set.mem_range, eq_comm] at hn

Goal state after:
p : ℕ → Prop
m n : ℕ
h0 : ∀ k < m, ¬p k
h : nth p n ≠ 0
k : ℕ
hk : p k
hn : ¬∃ y, k = y + m
⊢ False
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
m n : ℕ
h0 : ∀ k < m, ¬p k
h : nth p n ≠ 0
⊢ nth (fun i ↦ p (i + m)) n = nth p n - m

Tactic:
rw [← nth_add h0 h, Nat.add_sub_cancel]

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(a.sub' b).bit1 = ↑a.bit1 - ↑b.bit0

Tactic:
ZNum.cast_bit1,

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(a.sub' b) + ↑(a.sub' b) + 1 = ↑a.bit1 - ↑b.bit0
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : PosNum
⊢ ↑n = ↑↑n.pred' + 1

Tactic:
← n.to_nat_to_int,

Goal state after:
n : PosNum
⊢ ↑↑n = ↑↑n.pred' + 1
Module: Mathlib.Data.Ordmap.Ordset

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

Tactic:
rw [Nat.succ_add] at mm; rcases mm with (_ | ⟨⟨⟩⟩)

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

Goal state before:
pp: case mp
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
h : ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 ⟨a, f⟩ → P_1 i x
⊢ ∃ y, f i y = x

pp: case mpr
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
h : ∃ y, f i y = x
⊢ ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 ⟨a, f⟩ → P_1 i x

Tactic:
· apply @h fun i x => ∃ y : P.B a i, f i y = x
    rw [liftP_iff']
    intros
    exact ⟨_, rfl⟩

Goal state after:
case mpr
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
h : ∃ y, f i y = x
⊢ ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 ⟨a, f⟩ → P_1 i x
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
⊢ (l.rotateR x r).dual.Sized

Tactic:
by rw [dual_rotateR]; exact hr.dual.rotateL hl.dual

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

Goal state before:
pp: case f.f.cons.f
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        (isubtree ps (M.mk ⟨a, f⟩)).head = (isubtree ps (M.mk ⟨a, f'⟩)).head ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : F.B a
hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)
h₁ : R (f i) (f' i)
a₀ : F.A
f₀ : F.B a₀ → F.M
h : f i = M.mk ⟨a₀, f₀⟩
x✝ : F.M
h' : f' i = x✝
⊢ (isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩)).head = (isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)).head ∧
    ∃ a_1 f_1 f'_1,
      isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
        isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)

Tactic:
induction h' : f' i using PFunctor.M.casesOn' with

Goal state after:
case f.f.cons.f.f
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        (isubtree ps (M.mk ⟨a, f⟩)).head = (isubtree ps (M.mk ⟨a, f'⟩)).head ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : F.B a
hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)
h₁ : R (f i) (f' i)
a₀ : F.A
f₀ : F.B a₀ → F.M
h : f i = M.mk ⟨a₀, f₀⟩
a₁ : F.A
f₁ : F.B a₁ → F.M
h' : f' i = M.mk ⟨a₁, f₁⟩
⊢ (isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩)).head = (isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)).head ∧
    ∃ a_1 f_1 f'_1,
      isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
        isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: l : List ℕ
h : ∀ (p : ℕ), p ∈ l → Nat.Prime p
⊢ ↑(ofNatList l h).prod = l.prod

Tactic:
have := prod_ofNatMultiset (l : Multiset ℕ) h
  rw [Multiset.prod_coe] at this
  exact this

Goal state after: