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

Goal state before:
pp: case comp.refine_1
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
IHg : ∀ {k : Cont'}, codeSupp g k ⊆ S → Supports (codeSupp' g k) S
k : Cont'
H : codeSupp (f.comp g) k ⊆ S
H'✝ : trStmts₁ (trNormal (f.comp g) k) ∪ codeSupp g (Cont'.comp f k) ⊆ S
H' : codeSupp g (Cont'.comp f k) ⊆ S
h : codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ codeSupp' f k) ⊆ S
⊢ codeSupp f k ⊆ S

Tactic:
simp only [codeSupp', codeSupp, Finset.union_subset_iff] at h H ⊢

Goal state after:
case comp.refine_1
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
IHg : ∀ {k : Cont'}, codeSupp g k ⊆ S → Supports (codeSupp' g k) S
k : Cont'
H'✝ : trStmts₁ (trNormal (f.comp g) k) ∪ codeSupp g (Cont'.comp f k) ⊆ S
H' : codeSupp g (Cont'.comp f k) ⊆ S
h : codeSupp' g (Cont'.comp f k) ⊆ S ∧ trStmts₁ (trNormal f k) ⊆ S ∧ codeSupp' f k ⊆ S
H :
  (trStmts₁ (trNormal (f.comp g) k) ⊆ S ∧
      codeSupp' g (Cont'.comp f k) ⊆ S ∧ trStmts₁ (trNormal f k) ⊆ S ∧ codeSupp' f k ⊆ S) ∧
    contSupp k ⊆ S
⊢ codeSupp' f k ⊆ S ∧ contSupp k ⊆ S
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: I : Type u
inst✝² : Category.{u, u} I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
s : Cocone ((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X)
i : I
f : LocallyConstant (↑(toProfinite.obj (F.obj i)).toTop) X
⊢ (ConcreteCategory.hom ((isColimitLocallyConstantPresheaf c X hc).desc s))
      (LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) f) =
    (ConcreteCategory.hom (s.ι.app (Opposite.op i))) f

Tactic:
by
  change ((((locallyConstantPresheaf X).mapCocone c.op).ι.app ⟨i⟩) ≫
    (isColimitLocallyConstantPresheaf c X hc).desc s) _ = _
  rw [(isColimitLocallyConstantPresheaf c X hc).fac]

Goal state after:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
X : Type u
⊢ Presheaf.IsSheaf (coherentTopology LightProfinite) (locallyConstantPresheaf X)

Tactic:
exact (CompHausLike.LocallyConstant.functor.{u, u}
      (hs := fun _ _ _ ↦ ((LightProfinite.effectiveEpi_iff_surjective _).mp)).obj X).property

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

Goal state before:
pp: t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α₀ α₁ α₂ β : Type u
f : α₀ → F α₁
f' : α₁ → G α₂
x : t α₀ β
⊢ Comp.mk (tfst f' <$> tfst f x) = tfst (Comp.mk ∘ map f' ∘ f) x

Tactic:
rw [← comp_bitraverse]
  simp only [Function.comp_def, tfst, map_pure, Pure.pure]

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

Goal state before:
pp: σ : Type u
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
x : σ ⊕ α
⊢ (fun x ↦ f <$> x) <$> Sum.traverse g x = Sum.traverse (fun x ↦ f <$> g x) x

Tactic:
by
  cases x <;> simp [Sum.traverse, functor_norm] <;> congr

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
y : ℕ
⊢ { toFun := approx ⇑f, monotone' := ⋯ } y ≤ Part.fix ⇑f

Tactic:
x

Goal state after:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
y : ℕ
x : α
⊢ { toFun := approx ⇑f, monotone' := ⋯ } y x ≤ Part.fix (⇑f) x
Module: Mathlib.Data.DFinsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ toMultiset f ≤ toMultiset g ↔ f ≤ g

Tactic:
simp_rw [← Multiset.toDFinsupp_le_toDFinsupp, toMultiset_toDFinsupp]

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α : Type u_1} (x : Erased α), id <$> x = x

Tactic:
by intros; ext; simp

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α β : Type u_1} (f : α → β) (x : Erased α),
    (do
        let a ← x
        pure (f a)) =
      f <$> x

Tactic:
by intros; ext; simp

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α β : Type u_1} (x : α) (f : α → Erased β), pure x >>= f = f x

Tactic:
by intros; ext; simp

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α β γ : Type u_1} (x : Erased α) (f : α → Erased β) (g : β → Erased γ), x >>= f >>= g = x >>= fun x ↦ f x >>= g

Tactic:
by intros; ext; simp

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α β : Type u_3
f : α → β
s : Semiquot α
⊢ ∀ (a : β),
    (a ∈ do
        let y ← s
        pure (f y)) ↔
      a ∈ f <$> s

Tactic:
by simp [eq_comm]

Goal state after:
Module: Mathlib.Data.Semiquot

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

Tactic:
unfold get

Goal state after:
α : Type u_1
q : Semiquot α
p : q.IsPure
a : α
h : a ∈ q
⊢ q.liftOn id p ∈ q
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
p : s₁.entries ~ s₂.entries
⊢ (insert a b s₁).entries ~ (insert a b s₂).entries

Tactic:
simp only [entries_insert]; exact p.kinsert s₁.nodupKeys

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

Goal state before:
pp: case mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
l : List (Sigma β)
hl : l.NodupKeys
fst✝ : α
snd✝ : β fst✝
h : ¬⟨fst✝, snd✝⟩.fst ∈ { entries := l, nodupKeys := hl }
this :
  insertRec H0 IH { entries := ⟨fst✝, snd✝⟩ :: l, nodupKeys := ⋯ } ≍
    IH ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl } h
      (insertRec H0 IH { entries := l, nodupKeys := hl })
⊢ insertRec H0 IH (insert ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl }) ≍
    IH ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl } h
      (insertRec H0 IH { entries := l, nodupKeys := hl })

Tactic:
convert! this

Goal state after:
case e'_1.e'_3
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
l : List (Sigma β)
hl : l.NodupKeys
fst✝ : α
snd✝ : β fst✝
h : ¬⟨fst✝, snd✝⟩.fst ∈ { entries := l, nodupKeys := hl }
this :
  insertRec H0 IH { entries := ⟨fst✝, snd✝⟩ :: l, nodupKeys := ⋯ } ≍
    IH ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl } h
      (insertRec H0 IH { entries := l, nodupKeys := hl })
⊢ (insert ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl }).entries = ⟨fst✝, snd✝⟩ :: l

case e'_2.e'_3
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
l : List (Sigma β)
hl : l.NodupKeys
fst✝ : α
snd✝ : β fst✝
h : ¬⟨fst✝, snd✝⟩.fst ∈ { entries := l, nodupKeys := hl }
this :
  insertRec H0 IH { entries := ⟨fst✝, snd✝⟩ :: l, nodupKeys := ⋯ } ≍
    IH ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl } h
      (insertRec H0 IH { entries := l, nodupKeys := hl })
e_1✝ :
  C (insert ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl }) =
    C { entries := ⟨fst✝, snd✝⟩ :: l, nodupKeys := ⋯ }
⊢ (insert ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl }).entries = ⟨fst✝, snd✝⟩ :: l
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
⊢ lookupAll a l = (dlookup a l).toList

Tactic:
rw [← head?_lookupAll]
  have h1 := lookupAll_length_le_one a h; revert h1
  rcases lookupAll a l with (_ | ⟨b, _ | ⟨c, l⟩⟩) <;> intro h1 <;> try rfl
  exact absurd h1 (by simp)

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

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

Tactic:
by
  rw [← bit_decomp n]
  apply h

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
β : Type u_1
n : ℕ
s : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
⊢ ∀ (a : β) (s : Finset β),
    a ∉ s →
      ((∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (s.card * n) (∑ x ∈ s, f x)) →
        (∀ x ∈ insert a s, CPRankMax n (f x)) → CPRankMax ((insert a s).card * n) (∑ x ∈ insert a s, f x)

Tactic:
intro x s (h_x_notin_s : x ∉ s) ih h_cprank

Goal state after:
α : Type
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
β : Type u_1
n : ℕ
s✝ : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
s : Finset β
h_x_notin_s : x ∉ s
ih : (∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (s.card * n) (∑ x ∈ s, f x)
h_cprank : ∀ x_1 ∈ insert x s, CPRankMax n (f x_1)
⊢ CPRankMax ((insert x s).card * n) (∑ x ∈ insert x s, f x)
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: b : Bool
n : ℤ
⊢ (bif b then 1 else 0) / 2 + n = n

pp: case H
b : Bool
n : ℤ
⊢ 2 ≠ 0

Tactic:
(_ : (_ / 2 : ℤ) = 0),

Goal state after:
b : Bool
n : ℤ
⊢ 0 + n = n

b : Bool
n : ℤ
⊢ (bif b then 1 else 0) / 2 = 0

case H
b : Bool
n : ℤ
⊢ 2 ≠ 0
Module: Mathlib.Data.Int.Bitwise

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

Tactic:
Nat.cast_one

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

Goal state before:
pp: case pos
α : Type u_1
p : α → Bool
hd : α
tl : List α
IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p ((dropWhile p tl).get ⟨0, hl⟩) = true
hl : 0 < (dropWhile p (hd :: tl)).length
hp : p hd = true
⊢ ¬p
        ((match p hd with
            | true => dropWhile p tl
            | false => hd :: tl).get
          ⟨0, hl⟩) =
      true

pp: case neg
α : Type u_1
p : α → Bool
hd : α
tl : List α
IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p ((dropWhile p tl).get ⟨0, hl⟩) = true
hl : 0 < (dropWhile p (hd :: tl)).length
hp : ¬p hd = true
⊢ ¬p
        ((match p hd with
            | true => dropWhile p tl
            | false => hd :: tl).get
          ⟨0, hl⟩) =
      true

Tactic:
· simp_all only [get_eq_getElem]
      apply IH
      simp_all only [dropWhile_cons_of_pos]

Goal state after:
case neg
α : Type u_1
p : α → Bool
hd : α
tl : List α
IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p ((dropWhile p tl).get ⟨0, hl⟩) = true
hl : 0 < (dropWhile p (hd :: tl)).length
hp : ¬p hd = true
⊢ ¬p
        ((match p hd with
            | true => dropWhile p tl
            | false => hd :: tl).get
          ⟨0, hl⟩) =
      true
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m : ℕ
⊢ (Ico n m).length = m - n

Tactic:
dsimp [Ico]

Goal state after:
n m : ℕ
⊢ (range' n (m - n)).length = m - n
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m : ℕ
⊢ Pairwise (fun x1 x2 ↦ x1 < x2) (Ico n m)

Tactic:
dsimp [Ico]

Goal state after:
n m : ℕ
⊢ Pairwise (fun x1 x2 ↦ x1 < x2) (range' n (m - n))
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m : ℕ
⊢ (Ico n m).Nodup

Tactic:
dsimp [Ico]

Goal state after:
n m : ℕ
⊢ (range' n (m - n)).Nodup
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n : ℕ
⊢ Ico n (n + 1) = [n]

Tactic:
dsimp [Ico]

Goal state after:
n : ℕ
⊢ range' n (n + 1 - n) = [n]
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : List α
h : s.length = t.length
⊢ Shortlex r s t ↔ Lex r s t

Tactic:
simp [shortlex_def, h]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : Matrix m m A
k : ℕ
⊢ mulLeftLinearMap n R a ^ 0 = mulLeftLinearMap n R (a ^ 0)

Tactic:
by rw [pow_zero, pow_zero, mulLeftLinearMap_one, Module.End.one_eq_id]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ #(Finset.Icc ⊥ s) = ∏ i ∈ s.toFinset, (count i s + 1)

Tactic:
card_Icc,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ ∏ i ∈ ⊥.toFinset ∪ s.toFinset, (count i s + 1 - count i ⊥) = ∏ i ∈ s.toFinset, (count i s + 1)
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case intro.intro.inr
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep y
ihM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep (a ::ₘ y)
N : Multiset α
hN : ∀ (x : α), x ∈ N → x < a
hNM : (M + N).OneStep (a ::ₘ M)
⊢ Acc OneStep (M + N)

Tactic:
clear hNM

Goal state after:
case intro.intro.inr
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep y
ihM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep (a ::ₘ y)
N : Multiset α
hN : ∀ (x : α), x ∈ N → x < a
⊢ Acc OneStep (M + N)
Module: Mathlib.Data.Nat.Factorization.Divisors

Goal state before:
pp: n : ℕ
⊢ n.properDivisors =
    Finset.image (⇑{ toFun := fun x ↦ (↑x).prod fun x1 x2 ↦ x1 ^ x2, inj' := ⋯ }) (Finset.Iio n.factorization).attach

Tactic:
change _ = (Finset.Iio n.factorization).attach.image ((·.prod (· ^ ·)) ∘ Subtype.val)

Goal state after:
n : ℕ
⊢ n.properDivisors =
    Finset.image ((fun x ↦ x.prod fun x1 x2 ↦ x1 ^ x2) ∘ Subtype.val) (Finset.Iio n.factorization).attach
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: _a _b : ℕ
hab : _a ≤ _b
⊢ _a + 1 ≤ _b + 1

Tactic:
by gcongr

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

Goal state before:
pp: m n : ℕ
h : fib m ≤ n
⊢ fib m + 1 ≤ n + 1

Tactic:
by gcongr

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

Goal state before:
pp: case refine_1
n : PosNum
⊢ 2 ≤ ↑n + ↑n + 1

Tactic:
have := to_nat_pos n

Goal state after:
case refine_1
n : PosNum
this : 0 < ↑n
⊢ 2 ≤ ↑n + ↑n + 1
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
n : ℕ
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
h : ∀ (hfi : (Set.ofPred p).Finite), n < #hfi.toFinset
⊢ f (nth (fun i ↦ p (f i)) n) = nth p n

Tactic:
have hs {p' : ℕ → Prop} (h0p' : ∀ k, p' k → k ∈ Set.range f) :
      f '' {i | p' (f i)} = Set.ofPred p' := by
    ext i
    refine ⟨fun ⟨_, hi, h⟩ ↦ h ▸ hi, fun he ↦ ?_⟩
    rcases h0p' _ he with ⟨t, rfl⟩
    exact ⟨t, he, rfl⟩

Goal state after:
p : ℕ → Prop
n : ℕ
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
h : ∀ (hfi : (Set.ofPred p).Finite), n < #hfi.toFinset
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = Set.ofPred p'
⊢ f (nth (fun i ↦ p (f i)) n) = nth p n
Module: Mathlib.Data.PFunctor.Univariate.Basic

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

Tactic:
cases heq

Goal state after:
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)
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: case mk
n : ℕ
A : Type u
α : TypeVec.{u} n
fst✝ : (const n A).A
snd✝ : (const n A).B fst✝ ⟹ α
⊢ ⟨fst✝, fun x a ↦ PEmpty.elim a⟩ = ⟨fst✝, snd✝⟩

Tactic:
congr with (_⟨⟩)

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

Goal state before:
pp: m n : ZNum
x✝ : ↑m ∣ ↑n
k : ℤ
e : ↑n = ↑m * k
⊢ ↑↑n = m * ↑k

Tactic:
e

Goal state after:
m n : ZNum
x✝ : ↑m ∣ ↑n
k : ℤ
e : ↑n = ↑m * k
⊢ ↑(↑m * k) = m * ↑k
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → ↑P (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
⊢ splitFun (dropFun f)
      ((corec' P (fun b ↦ (g b).fst) (fun b ↦ dropFun (g b).snd) fun b ↦ lastFun (g b).snd) ∘ lastFun f) =
    (TypeVec.id ::: corec P g) ⊚ f

Tactic:
conv_rhs => rw [← split_dropFun_lastFun f, appendFun_comp_splitFun]

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → ↑P (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
⊢ splitFun (dropFun f)
      ((corec' P (fun b ↦ (g b).fst) (fun b ↦ dropFun (g b).snd) fun b ↦ lastFun (g b).snd) ∘ lastFun f) =
    splitFun (TypeVec.id ⊚ dropFun f) (corec P g ∘ lastFun f)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil.node
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (rl.node' rx rr).Balanced
sr : (node rs rl rx rr).Sized
⊢ nil.balance x (rl.node' rx rr) = nil.balance' x (rl.node' rx rr)

Tactic:
obtain - | ⟨rls, rll, rlx, rlr⟩ := rl <;> obtain - | ⟨rrs, rrl, rrx, rrr⟩ := rr <;>
        dsimp +instances [balance, balance']

Goal state after:
case nil.node.nil.nil
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
hr : (nil.node' rx nil).Balanced
sr : (node rs nil rx nil).Sized
⊢ node 2 nil x (nil.node' rx nil) = nil.node' x (nil.node' rx nil)

case nil.node.nil.node
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (nil.node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs nil rx (node rrs rrl rrx rrr)).Sized
⊢ node 3 (Ordnode.singleton x) rx (node rrs rrl rrx rrr) =
    if 0 + (0 + rrs + 1) ≤ 1 then nil.node' x (nil.node' rx (node rrs rrl rrx rrr))
    else nil.rotateL x (nil.node' rx (node rrs rrl rrx rrr))

case nil.node.node.nil
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx nil).Balanced
sr : (node rs (node rls rll rlx rlr) rx nil).Sized
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    if 0 + (rls + 1) ≤ 1 then nil.node' x ((node rls rll rlx rlr).node' rx nil)
    else nil.rotateL x ((node rls rll rlx rlr).node' rx nil)

case nil.node.node.node
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
⊢ (if rls < ratio * rrs then
      node (rls + rrs + 1 + 1) (node (rls + 1) nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
    else
      node (rls + rrs + 1 + 1) (node (rll.size + 1) nil x rll) rlx
        (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))) =
    if 0 + (rls + rrs + 1) ≤ 1 then nil.node' x ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr))
    else nil.rotateL x ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr))
Module: Mathlib.Data.PFunctor.Multivariate.W

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{?u.9} n
a : P.A
f : P.last.B a → P.last.W
g' : P.drop.B a ⟹ α
g : (j : P.last.B a) → P.WPath (f j) ⟹ α
i : Fin2 n
⊢ P.WPath (WType.mk a f) i → α i

Tactic:
x

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{?u.9} n
a : P.A
f : P.last.B a → P.last.W
g' : P.drop.B a ⟹ α
g : (j : P.last.B a) → P.WPath (f j) ⟹ α
i : Fin2 n
x : P.WPath (WType.mk a f) i
⊢ α i
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node
α : Type u_1
inst✝ : Preorder α
s : ℕ
o₂ : WithTop α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
l_ih✝ :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α},
    Valid' o₁ (l.node' x rl) o₂ →
      Valid' o₁ (l.node' x rl).eraseMax ↑(findMax' x rl) ∧ (l.node' x rl).size = (l.node' x rl).eraseMax.size + 1
IHrr :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α},
    Valid' o₁ (l.node' x rr) o₂ →
      Valid' o₁ (l.node' x rr).eraseMax ↑(findMax' x rr) ∧ (l.node' x rr).size = (l.node' x rr).eraseMax.size + 1
l : Ordnode α
x : α
o₁ : WithBot α
H : Valid' o₁ (l.node' x (rl.node' rx rr)) o₂
this : Ordnode.node rs rl rx rr = rl.node' rx rr
h : Valid' (↑x) (rl.node' rx rr).eraseMax ↑(findMax' rx rr)
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMax.size + 1
⊢ l.size + (rl.node' rx rr).size + 1 = l.size + (rl.node' rx rr).eraseMax.size + 1 + 1

Tactic:
e

Goal state after:
case node
α : Type u_1
inst✝ : Preorder α
s : ℕ
o₂ : WithTop α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
l_ih✝ :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α},
    Valid' o₁ (l.node' x rl) o₂ →
      Valid' o₁ (l.node' x rl).eraseMax ↑(findMax' x rl) ∧ (l.node' x rl).size = (l.node' x rl).eraseMax.size + 1
IHrr :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α},
    Valid' o₁ (l.node' x rr) o₂ →
      Valid' o₁ (l.node' x rr).eraseMax ↑(findMax' x rr) ∧ (l.node' x rr).size = (l.node' x rr).eraseMax.size + 1
l : Ordnode α
x : α
o₁ : WithBot α
H : Valid' o₁ (l.node' x (rl.node' rx rr)) o₂
this : Ordnode.node rs rl rx rr = rl.node' rx rr
h : Valid' (↑x) (rl.node' rx rr).eraseMax ↑(findMax' rx rr)
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMax.size + 1
⊢ l.size + ((rl.node' rx rr).eraseMax.size + 1) + 1 = l.size + (rl.node' rx rr).eraseMax.size + 1 + 1
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ (l.node' x r) o₂
⊢ Valid' o₁ (l.node' x r).eraseMax ↑(findMax' x r) ∧ (l.node' x r).size = (l.node' x r).eraseMax.size + 1

Tactic:
induction r generalizing l x o₁ with

Goal state after:
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: m : ℕ+
p : Nat.Primes
k : ℕ
⊢ ↑p ^ k ∣ m ↔ k ≤ Multiset.count p m.factorMultiset

Tactic:
rw [Multiset.le_count_iff_replicate_le, ← factorMultiset_le_iff, factorMultiset_pow,
    factorMultiset_ofPrime]

Goal state after:
m : ℕ+
p : Nat.Primes
k : ℕ
⊢ k • PrimeMultiset.ofPrime p ≤ m.factorMultiset ↔ Multiset.replicate k p ≤ m.factorMultiset
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t ↑rx
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
H₂ : 1 ≤ t.size → 1 ≤ rr.size → rr.size ≤ delta * t.size
H₁ : t.size = 0 → rr.size ≤ 1
⊢ 2 * t.size ≤ 9 * rr.size + 5 ∨ t.size ≤ 3

Tactic:
e

Goal state after:
case refine_1
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t ↑rx
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
H₂ : 1 ≤ t.size → 1 ≤ rr.size → rr.size ≤ delta * t.size
H₁ : t.size = 0 → rr.size ≤ 1
⊢ 2 * (ll.size + lr.size + 1 + rl.size) ≤ 9 * rr.size + 5 ∨ ll.size + lr.size + 1 + rl.size ≤ 3
Module: Mathlib.Data.PSigma.Order

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

Tactic:
exact hab.not_ge hba

Goal state after: