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

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

Tactic:
⟨j⟩

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

Goal state before:
pp: p : ℕ → Prop
x : ℕ
h : p x
⊢ WellFounded (Upto.GT p)

Tactic:
by
    suffices Upto.GT p = InvImage (· < ·) fun y : Nat.Upto p => x - y.val by
      rw [this]
      exact (measure _).wf
    ext ⟨a, ha⟩ ⟨b, _⟩
    dsimp [InvImage, Upto.GT]
    rw [tsub_lt_tsub_iff_left_of_le (le_of_not_gt fun h' => ha _ h' h)]

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

Goal state before:
pp: case inr
p : ℕ → Prop
x : Upto p
h : ¬p ↑x
h' : ↑x < (↑x).succ
⊢ ¬p ↑x

Tactic:
exact h

Goal state after:
Module: Mathlib.Control.Fix

Goal state before:
pp: case succ
α : 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
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α) (hwf : WellFounded fun y x ↦ x < y), hwf.fix (fixAux f) z x' = Fix.approx f n.succ x'
z : Upto p
_this : p (n + 1 + ↑z)
hk : Nat.find h' = n + 1 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
⊢ (fun x ↦ assert (¬p ↑z) fun h ↦ hwf✝.fix (fixAux f) (z.succ h) x) = Fix.approx f (n + 1)

Tactic:
ext : 1

Goal state after:
case succ
α : 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
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α) (hwf : WellFounded fun y x ↦ x < y), hwf.fix (fixAux f) z x' = Fix.approx f n.succ x'
z : Upto p
_this : p (n + 1 + ↑z)
hk : Nat.find h' = n + 1 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
x✝ : α
⊢ (assert (¬p ↑z) fun h ↦ hwf✝.fix (fixAux f) (z.succ h) x✝) = Fix.approx f (n + 1) x✝
Module: Mathlib.Control.Fold

Goal state before:
pp: m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : β → α → m β
x✝¹ y✝ : FreeMonoid α
x✝ : KleisliCat.mk m β
⊢ unop (op (flip (List.foldlM f) (FreeMonoid.toList (x✝¹ * y✝)))) x✝ =
    unop (op (flip (List.foldlM f) (FreeMonoid.toList x✝¹)) * op (flip (List.foldlM f) (FreeMonoid.toList y✝))) x✝

Tactic:
apply List.foldlM_append

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ ⊥ ≤ f ⊥

Tactic:
apply @bot_le _ _ _ (f ⊥)

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u} n
β : TypeVec.{v} n
f g : α ⟹ β
h : ∀ (i : Fin2 n), f i = g i
i : Fin2 n
⊢ f i = g i

Tactic:
apply h

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: r : Type u
m : Type u → Type v
α : Type w
x y : ContT r m α
h : ∀ (f : α → m r), x.run f = y.run f
x✝ : α → m r
⊢ x x✝ = y x✝

Tactic:
apply h

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α : Type u} (β : Type u) (x : α) (dead : Label α (ExceptT ε m) β → β → ExceptT ε m α),
    (callCC fun f ↦ goto f x >>= dead f) = pure x

Tactic:
intros
    simp only [callCC, ExceptT.callCC, ExceptT.goto_mkLabel, map_eq_bind_pure_comp, Function.comp,
      ExceptT.run_bind, ExceptT.run_mk, bind_assoc, pure_bind, @callCC_bind_left m _]
    ext; rfl

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∀ (i : ℕ) (b : β x), b ∉ approx (⇑f) i x
b' : β x
h' : ∃ i, b' ∈ approx (⇑f) i x
⊢ b' ∈ approx (⇑f) 0 x

Tactic:
obtain ⟨i, h'⟩ := h'

Goal state after:
case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∀ (i : ℕ) (b : β x), b ∉ approx (⇑f) i x
b' : β x
i : ℕ
h' : b' ∈ approx (⇑f) i x
⊢ b' ∈ approx (⇑f) 0 x
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
q : Semiquot α
p : q.IsPure
a : α
h : a ∈ q
⊢ id a ∈ q

Tactic:
exact h

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
xs : List α
h : ∀ (x : α), x ∈ xs
h' : xs.Nodup
x : α
⊢ x ∈ xs

Tactic:
apply h

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

Goal state before:
pp: case h
α : Type u_1
f : α → Option α
h : ∀ (a b : α), b ∈ f a → a = b
l : List α
⊢ ∀ (a b : α), b ∈ f a → id a = id b

Tactic:
exact h

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

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

Tactic:
ext : 1

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b b' : β a
s : AList β
⊢ (insert a b' (insert a b s)).entries = (insert a b' s).entries
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
⊢ a ≠ ⟨a', b'⟩.fst

Tactic:
exact h

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₂.entries.keys

Tactic:
apply 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✝
⊢ x✝ ∈ s₁.keys
Module: Mathlib.Data.List.Sigma

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

Tactic:
exact h

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

Goal state before:
pp: α : Type u_1
inst✝ : SizeOf α
l r : List α
a : α
h : sizeOf l ≤ sizeOf r
⊢ 1 + sizeOf a + sizeOf l ≤ 1 + sizeOf a + sizeOf r

Tactic:
exact Nat.add_le_add_iff_left.mpr h

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

Goal state before:
pp: case h
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
a : List (ι →₀ M)
hs : Pairwise (Disjoint on Finsupp.support) (Quot.mk (⇑(List.isSetoid (ι →₀ M))) a)
⊢ (sum (Quot.mk (⇑(List.isSetoid (ι →₀ M))) a)).support =
    (map Finsupp.support (Quot.mk (⇑(List.isSetoid (ι →₀ M))) a)).sup

Tactic:
obtain ⟨l, hl, hd⟩ := hs

Goal state after:
case h
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
a l : List (ι →₀ M)
hl : Quot.mk (⇑(List.isSetoid (ι →₀ M))) a = ↑l
hd : List.Pairwise (Disjoint on Finsupp.support) l
⊢ (sum (Quot.mk (⇑(List.isSetoid (ι →₀ M))) a)).support =
    (map Finsupp.support (Quot.mk (⇑(List.isSetoid (ι →₀ M))) a)).sup
Module: Mathlib.Data.Finsupp.Sigma

Goal state before:
pp: case pos
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : AddMonoid M
k : κ
f g : ι k →₀ M
k' : κ
i : ι k'
hk : k' = k
⊢ (f + g).embSigma ⟨k', i⟩ = (f.embSigma + g.embSigma) ⟨k', i⟩

Tactic:
subst hk

Goal state after:
case pos
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : AddMonoid M
k' : κ
i : ι k'
f g : ι k' →₀ M
⊢ (f + g).embSigma ⟨k', i⟩ = (f.embSigma + g.embSigma) ⟨k', i⟩
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: C : ℤ → Sort u
n : ℤ
h : (b : Bool) → (n : ℤ) → C (bit b n)
⊢ C (bit n.bodd n.div2)

Tactic:
apply h

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

Goal state before:
pp: a b : ℤ
⊢ a.natAbs ≤ b.natAbs ↔ a * a ≤ b * b

Tactic:
exact natAbs_le_iff_mul_self_le

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
v : β → α → β
b : β
inst✝ : RightCommutative v
⊢ foldr (flip v) b l = foldl v b l

Tactic:
by
  induction l generalizing b <;> simp [*, flip, foldl_cons_eq_apply_foldl, -foldl_cons]

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

Goal state before:
pp: case neg
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : ¬v % r < b % r
⊢ v % r < r + b % r ∧ b % r ≤ v % r

Tactic:
exact ⟨(mod_lt _ hr).trans_le (by simp), not_lt.mp h⟩

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

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
⊢ l.rdrop n = (drop n l.reverse).reverse

Tactic:
rw [rdrop]

Goal state after:
α : Type u_1
l : List α
n : ℕ
⊢ take (l.length - n) l = (drop n l.reverse).reverse
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ (rtakeWhile p l).reverse <+: l.reverse

Tactic:
rtakeWhile,

Goal state after:
α : Type u_1
p : α → Bool
l : List α
⊢ (takeWhile p l.reverse).reverse.reverse <+: l.reverse
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
hx : x ∈ rtakeWhile p l
⊢ p x = true

Tactic:
rtakeWhile,

Goal state after:
α : Type u_1
p : α → Bool
l : List α
x : α
hx : x ∈ (takeWhile p l.reverse).reverse
⊢ p x = true
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ rtakeWhile p l.reverse = (takeWhile p l).reverse

Tactic:
rtakeWhile,

Goal state after:
α : Type u_1
p : α → Bool
l : List α
⊢ (takeWhile p l.reverse.reverse).reverse = (takeWhile p l).reverse
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case inr.nil
α : Type u_1
r : α → α → Prop
s₁ s₂ : List α
h : Shortlex r s₁ s₂
h2 : s₁.length = s₂.length ∧ Lex r s₁ s₂
⊢ Shortlex r s₁ s₂

Tactic:
exact h

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

Goal state before:
pp: case inr.nil
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
h2 : t₁.length = t₂.length ∧ Lex r t₁ t₂
⊢ Shortlex r t₁ t₂

Tactic:
exact h

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

Goal state before:
pp: case nil.inl
α : Type u_1
m : List α
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
hm : m ∈ []
⊢ IsChain (fun x y ↦ r x y = true) m

Tactic:
cases not_mem_nil hm

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: case mpr
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
h : a = 0
⊢ mulLeftLinearMap n R a = 0

Tactic:
rw [h]
    exact mulLeftLinearMap_zero_eq_zero _ _

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

Goal state before:
pp: α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
z : List α
hz : drop q w ++ z = w
⊢ take q w = take q (drop q w ++ z)

Tactic:
rw [hz]

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

Goal state before:
pp: case cons.inl
α : Type u_1
inst✝ : Preorder α
z : α
M N X Y : Multiset α
hM : M = X + Y
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    0 ≠ ∅ → M = X + Y → N = X + 0 → (∀ (y : α), y ∈ Y → ∃ z, z ∈ 0 ∧ y < z) → TransGen OneStep M N
hZ : z ::ₘ 0 ≠ ∅
hN : N = X + z ::ₘ 0
hYZ : ∀ (y : α), y ∈ Y → ∃ z_1, z_1 ∈ z ::ₘ 0 ∧ y < z_1
⊢ TransGen OneStep M N

Tactic:
exact .single ⟨X, Y, z, hM, hN, by simpa using hYZ⟩

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

Goal state before:
pp: q✝ : ℚ≥0
α : ℚ≥0 → Sort u_1
h : (m n : ℕ) → α (↑m / ↑n)
q : ℚ≥0
⊢ α (↑q.num / ↑q.den)

Tactic:
apply h

Goal state after:
Module: Mathlib.Data.Nat.Digits.Div

Goal state before:
pp: b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ b ∣ n ↔ b ∣ (b'.digits n).sum

Tactic:
by
  rw [← ofDigits_one]
  conv_lhs => rw [← ofDigits_digits b' n]
  rw [Nat.dvd_iff_mod_eq_zero, Nat.dvd_iff_mod_eq_zero, ofDigits_mod, h]

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
a b : A
h : ↑p ^ m * a + ↑n * b = 1
⊢ ↑n * b = 1

Tactic:
simpa [hm] using h

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ ↑(m.choose k.1) = ↑m ! * (↑k.1!)⁻¹ʳ * (↑k.2!)⁻¹ʳ

Tactic:
subst hk

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
k : ℕ × ℕ
hm : IsUnit ↑(k.1 + k.2)!
⊢ ↑((k.1 + k.2).choose k.1) = ↑(k.1 + k.2)! * (↑k.1!)⁻¹ʳ * (↑k.2!)⁻¹ʳ
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: case inr
n : ℕ
h : n + 1 - fib (n + 1).greatestFib > 0
⊢ (n + 1 - fib (n + 1).greatestFib).greatestFib + 2 ≤ (n + 1).greatestFib

Tactic:
exact add_le_of_le_tsub_right_of_le (le_greatestFib.2 le_add_self)
      (greatestFib_sub_fib_greatestFib_le_greatestFib n.succ_ne_zero)

Goal state after:
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n : ℕ
hn : 1 < n
hpn : (Icc 1 (n - 1)).gcd n.choose ≠ 1
q : ℕ
hq : Nat.Prime q
h : q ∣ n
this✝ : Fact (Nat.Prime q)
this : n = q ^ multiplicity q n
⊢ q ∣ n

Tactic:
exact h

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

Goal state before:
pp: case node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α

Tactic:
· rcases id r with _ | ⟨rs, rl, rx, rr⟩
    · rcases id ll with _ | lls
      · rcases lr with _ | ⟨_, _, lrx⟩
        · exact node 2 l x nil
        · exact node 3 (ι lx) lrx ι x
      · rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩
        · exact node 3 ll lx ι x
        · exact
            if lrs < ratio * lls then node (ls + 1) ll lx (node (lrs + 1) lr x nil)
            else
              node (ls + 1) (node (lls + size lrl + 1) ll lx lrl) lrx
                (node (size lrr + 1) lrr x nil)
    · refine
        if delta * ls < rs then ?_ else if delta * rs < ls then ?_ else node (ls + rs + 1) l x r
      · rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩
        · exact nil
        --should not happen
        rcases id rr with _ | rrs
        · exact nil
        --should not happen
        exact
          if rls < ratio * rrs then node (ls + rs + 1) (node (ls + rls + 1) l x rl) rx rr
          else
            node (ls + rs + 1) (node (ls + size rll + 1) l x rll) rlx
              (node (size rlr + rrs + 1) rlr rx rr)
      · rcases id ll with _ | lls
        · exact nil
        --should not happen
        rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩
        · exact nil
        --should not happen
        exact
          if lrs < ratio * lls then node (ls + rs + 1) ll lx (node (lrs + rs + 1) lr x r)
          else
            node (ls + rs + 1) (node (lls + size lrl + 1) ll lx lrl) lrx
              (node (size lrr + rs + 1) lrr x r)

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

Goal state before:
pp: case inr
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt✝ : ∀ (hf : (Set.ofPred p).Finite), k + 1 < #hf.toFinset
a : ℕ
this : nth p k < nth p (k + 1)
hlt : a < nth p k
hpa : p a
⊢ a < nth p (k + 1) ∧ p a

Tactic:
· exact ⟨hlt.trans this, hpa⟩

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

Goal state before:
pp: case node.inr.inr
α : 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₁ : ratio * r.size ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
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
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)

Tactic:
by_cases mm : size ml + size mr ≤ 1

Goal state after:
case pos
α : 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₁ : ratio * r.size ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
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
mm : ml.size + mr.size ≤ 1
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)

case neg
α : 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₁ : ratio * r.size ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
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
mm : ¬ml.size + mr.size ≤ 1
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case neg
α : 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₁ : ratio * r.size ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
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
mm : ¬ml.size + mr.size ≤ 1
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)

Tactic:
rcases hm.3.1.resolve_left mm with ⟨mm₁, mm₂⟩

Goal state after:
case neg
α : 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₁ : ratio * r.size ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
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
mm : ¬ml.size + mr.size ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size ≤ delta * ml.size
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node
α : 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 + 1) ≤ 9 * l.size + 5 ∨ rl.size + rr.size + 1 ≤ 3
⊢ Valid' o₁ (l.rotateL x (Ordnode.node rs rl rx rr)) o₂

Tactic:
replace H3 : 2 * (size rl + size rr) ≤ 9 * size l + 3 ∨ size rl + size rr ≤ 2 :=
    H3.imp (@Nat.le_of_add_le_add_right _ 2 _) Nat.le_of_succ_le_succ

Goal state after:
case node
α : 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
⊢ Valid' o₁ (l.rotateL x (Ordnode.node rs rl rx rr)) o₂
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x✝ : P.last.M
b : β
x : P.last.M
i : Fin2 n
a : P.A
f : P.last.B a → P.last.M
h' : (corecShape P g₀ g₂ b).dest = ⟨a, f⟩
c : P.drop.B a i
h : x = corecShape P g₀ g₂ b
⊢ a = g₀ b

Tactic:
M.corecShape,

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x✝ : P.last.M
b : β
x : P.last.M
i : Fin2 n
a : P.A
f : P.last.B a → P.last.M
h' : (PFunctor.M.corec (fun b ↦ ⟨g₀ b, g₂ b⟩) b).dest = ⟨a, f⟩
c : P.drop.B a i
h : x = corecShape P g₀ g₂ b
⊢ a = g₀ b
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x✝ : P.last.M
b : β
x : P.last.M
i : Fin2 n
a : P.A
f : P.last.B a → P.last.M
h' : (corecShape P g₀ g₂ b).dest = ⟨a, f⟩
j : P.last.B a
c : Path P (f j) i
h : x = corecShape P g₀ g₂ b
⊢ a = g₀ b

Tactic:
M.corecShape,

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x✝ : P.last.M
b : β
x : P.last.M
i : Fin2 n
a : P.A
f : P.last.B a → P.last.M
h' : (PFunctor.M.corec (fun b ↦ ⟨g₀ b, g₂ b⟩) b).dest = ⟨a, f⟩
j : P.last.B a
c : Path P (f j) i
h : x = corecShape P g₀ g₂ b
⊢ a = g₀ b
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x✝ : P.last.M
b : β
x : P.last.M
i : Fin2 n
a : P.A
f : P.last.B a → P.last.M
h' : (corecShape P g₀ g₂ b).dest = ⟨a, f⟩
j : P.last.B a
c : Path P (f j) i
h : x = corecShape P g₀ g₂ b
h₀ : a = g₀ b
⊢ f j = corecShape P g₀ g₂ (g₂ b (P.castLastB h₀ j))

Tactic:
M.corecShape,

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x✝ : P.last.M
b : β
x : P.last.M
i : Fin2 n
a : P.A
f : P.last.B a → P.last.M
h' : (PFunctor.M.corec (fun b ↦ ⟨g₀ b, g₂ b⟩) b).dest = ⟨a, f⟩
j : P.last.B a
c : Path P (f j) i
h : x = corecShape P g₀ g₂ b
h₀ : a = g₀ b
⊢ f j = corecShape P g₀ g₂ (g₂ b (P.castLastB h₀ j))
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case nil
F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
x : F.M
h : ¬IsPath [] x
⊢ False

Tactic:
apply h

Goal state after:
case nil
F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
x : F.M
h : ¬IsPath [] x
⊢ IsPath [] x