mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.SplitLengths

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

Tactic:
cases sz

Goal state after:
case nil
α : Type u_1
i : ℕ
hi : ∀ (l : List α) (sz : List ℕ), take i (sz.splitLengths l) = (take i sz).splitLengths l
l : List α
⊢ take (i + 1) ([].splitLengths l) = (take (i + 1) []).splitLengths l

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
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: case mp
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 : mulLeftLinearMap n R a = 0
inhabited_h : Inhabited n
⊢ a = 0

Tactic:
ext i j

Goal state after:
case mp
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 : mulLeftLinearMap n R a = 0
inhabited_h : Inhabited n
i : l
j : m
⊢ a i j = 0 i j
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: case mp
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✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
h : mulRightLinearMap l R a = 0
inhabited_h : Inhabited l
⊢ a = 0

Tactic:
ext i j

Goal state after:
case mp
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✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
h : mulRightLinearMap l R a = 0
inhabited_h : Inhabited l
i : m
j : n
⊢ a i j = 0 i j
Module: Mathlib.Data.List.SplitBy

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

Tactic:
by
  obtain rfl | hl := eq_or_ne l []
  · simp
  obtain rfl | hm := eq_or_ne m []
  · simp
  rw [splitBy_eq_iff]
  refine ⟨by simp, by simp, ?_, ?_⟩; · aesop (add apply unsafe isChain_of_mem_splitBy)
  rw [isChain_append]
  refine ⟨isChain_getLast_head_splitBy _ _, isChain_getLast_head_splitBy _ _, fun x hx y hy ↦ ?_⟩
  use ne_nil_of_mem_splitBy (mem_of_mem_getLast? hx), ne_nil_of_mem_splitBy (mem_of_mem_head? hy)
  apply ha
  · simp_rw [← getLast_of_mem_getLast? hx, getLast_getLast_splitBy _ hl]
    exact getLast_mem_getLast? _
  · simp_rw [← head_of_mem_head? hy, head_head_splitBy _ hm]
    exact head_mem_head? _

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

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

Tactic:
Finset.card_Ico_eq_card_Icc_sub_one,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ #(Finset.Icc s t) - 1 = ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s) - 1
Module: Mathlib.Data.Nat.Choose.Dvd

Goal state before:
pp: p a b : ℕ
hp : Prime p
hap : a < p
hbp : b < p
h : p ≤ a + b
h₁ : (p ∣ (a + b).choose a ∨ p ≤ a) ∨ p ≤ b
⊢ p ∣ (a + b).choose a

Tactic:
exact (h₁.resolve_right hbp.not_ge).resolve_right hap.not_ge

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case inr.inr.inr
a b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b

Tactic:
← factorization_le_iff_dvd (pow_ne_zero _ ha) hb,

Goal state after:
case inr.inr.inr
a b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ (a ^ n).factorization ≤ b.factorization ↔ a ∣ n.floorRoot b
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: n : ℕ
⊢ (n + 1).zeckendorf.IsZeckendorfRep

Tactic:
rw [zeckendorf_succ, IsZeckendorfRep, List.cons_append]

Goal state after:
n : ℕ
⊢ IsChain (fun a b ↦ b + 2 ≤ a) ((n + 1).greatestFib :: ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]))
Module: Mathlib.Data.Nat.Fib.Zeckendorf

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

Tactic:
exact le_greatestFib.2 le_add_self

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

Goal state before:
pp: n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha₁ : n < p ^ a
ha₂ : k < p ^ a
⊢ ↑(n.choose k) ≡ ∏ i ∈ range a, ↑((n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]

Tactic:
by
  apply (choose_modEq_choose_mul_prod_range_choose a).trans
  simp_rw [Nat.div_eq_of_lt ha₁, Nat.div_eq_of_lt ha₂, choose, cast_one, one_mul, cast_prod,
    Int.ModEq.refl]

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

Goal state before:
pp: p✝ p : ℕ → Prop
n : ℕ
⊢ ℕ

Tactic:
exact
    if h : Set.Finite (Set.ofPred p) then h.toFinset.sort.getD n 0
    else @Nat.Subtype.orderIsoOfNat (Set.ofPred p) (Set.Infinite.to_subtype h) n

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

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

Tactic:
simp_rw [nth_zero]

Goal state after:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = Set.ofPred p'
h : ∀ (hfi : (Set.ofPred p).Finite), 0 < #hfi.toFinset
⊢ f (sInf {i | p (f i)}) = sInf (Set.ofPred p)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.inr.inl
α : 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 ≤ (Ordnode.node s ml z mr).size
lr₁ : delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size
lr₂ : 3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9
mr₂ : (Ordnode.node s ml z mr).size ≤ 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:
rw [r0] at mr₂; cases not_le_of_gt Hm mr₂

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

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
⊢ Liftp p ⟨a, f⟩ ↔ ∀ (i : P.B a), p (f i)

Tactic:
by
  simp only [liftp_iff]; constructor <;> intro h
  · rcases h with ⟨a', f', heq, h'⟩
    cases heq
    assumption
  repeat' first | constructor | assumption

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

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

Tactic:
by
    rw [sub', ZNum.cast_bit0, cast_sub' a b]
    have : ((-b + (a + -b) : ℤ) : α) = a + (-b + -b) := by simp [add_left_comm]
    simpa [sub_eq_add_neg] using this

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

Goal state before:
pp: case h.right
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
a : P.A
f₀ f₁ : P.B a → α
xeq : x = ⟨a, f₀⟩
yeq : y = ⟨a, f₁⟩
h : ∀ (i : P.B a), r (f₀ i) (f₁ i)
⊢ (fun t ↦ (↑t).2) <$> ⟨a, fun i ↦ ⟨(f₀ i, f₁ i), ⋯⟩⟩ = y

Tactic:
rw [yeq]

Goal state after:
case h.right
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
a : P.A
f₀ f₁ : P.B a → α
xeq : x = ⟨a, f₀⟩
yeq : y = ⟨a, f₁⟩
h : ∀ (i : P.B a), r (f₀ i) (f₁ i)
⊢ (fun t ↦ (↑t).2) <$> ⟨a, fun i ↦ ⟨(f₀ i, f₁ i), ⋯⟩⟩ = ⟨a, f₁⟩
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ℕ
⊢ (↑n).toZNumNeg = -↑n

Tactic:
rw [← of_nat_toZNum, Num.zneg_toZNum]

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

Goal state before:
pp: case mpr.succ.step.f.f
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
x_a : F.A
x_f : F.B x_a → F.M
a✝¹ : M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩
y_a : F.A
y_f : F.B y_a → F.M
a✝ : M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩
⊢ Agree ((M.mk ⟨x_a, x_f⟩).approx (n✝ + 1)) ((M.mk ⟨y_a, y_f⟩).approx (n✝ + 1 + 1))

Tactic:
| _ y_a y_f
       => 

Goal state after:
case mpr.succ.step.f.f
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
x_a : F.A
x_f : F.B x_a → F.M
a✝¹ : M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩
y_a : F.A
y_f : F.B y_a → F.M
a✝ : M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩
⊢ Agree ((M.mk ⟨x_a, x_f⟩).approx (n✝ + 1)) ((M.mk ⟨y_a, y_f⟩).approx (n✝ + 1 + 1))
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
a : F.A
x : F.B a → F.M
i : F.B (M.mk ⟨a, x⟩).head
⊢ (M.mk ⟨a, x⟩).children i = x (cast ⋯ i)

Tactic:
apply ext'; intro n; rfl

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

Goal state before:
pp: α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
⊢ All P (l.rotateR x r) ↔ All P l ∧ P x ∧ All P r

Tactic:
by
  rw [← all_dual, dual_rotateR, all_rotateL]; simp [all_dual, and_comm, and_left_comm, and_assoc]

Goal state after:
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 (Ordnode.node rs rl rx rr)) o₂
⊢ Valid' o₁ (l.node' x (Ordnode.node rs rl rx rr)).eraseMax ↑(findMax' x (Ordnode.node rs rl rx rr)) ∧
    (l.node' x (Ordnode.node rs rl rx rr)).size = (l.node' x (Ordnode.node rs rl rx rr)).eraseMax.size + 1

Tactic:
| node rs rl rx rr _ IHrr =>

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

Goal state before:
pp: case node.nil.node.node
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
⊢ ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).rotateR x nil =
    if lrs < ratio * lls then
      node (lls + lrs + 1 + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)
    else
      node (lls + lrs + 1 + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
        (node (lrr.size + 1) lrr x nil)

pp: case node.nil.node.node.hnc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
⊢ ¬lls + lrs + 1 ≤ 1

Tactic:
rotateR

Goal state after:
case node.nil.node.node
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
⊢ (if (node lrs lrl lrx lrr).size < ratio * (node lls lll llx llr).size then
      (node lls lll llx llr).node3R lx (node lrs lrl lrx lrr) x nil
    else (node lls lll llx llr).node4R lx (node lrs lrl lrx lrr) x nil) =
    if lrs < ratio * lls then
      node (lls + lrs + 1 + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)
    else
      node (lls + lrs + 1 + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
        (node (lrr.size + 1) lrr x nil)

case node.nil.node.node.hnc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
⊢ ¬lls + lrs + 1 ≤ 1
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'
⊢ (l.balanceL x r).size = l.size + r.size + 1

Tactic:
rw [balanceL_eq_balance' hl hr sl sr H, size_balance' sl sr]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
h : nil.Bounded o₁ o₂
⊢ nil.Bounded o₁ ⊤

Tactic:
cases o₁ <;> trivial

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 : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : (P F).M α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
⊢ ∀ (a b : Cofix F α), r a b → Quot.lift (Quot.mk r') h₁ a = Quot.lift (Quot.mk r') h₁ b

Tactic:
intro c
          apply Quot.inductionOn
            (motive := fun c =>
              ∀ b, r c b → Quot.lift (Quot.mk r') h₁ c = Quot.lift (Quot.mk r') h₁ b) c
          clear c
          intro c d
          apply Quot.inductionOn
            (motive := fun d => r (Quot.mk Mcongr c) d →
              Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr c) = Quot.lift (Quot.mk r') h₁ d) d
          clear d
          intro d rcd; apply Quot.sound; apply rcd

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

Goal state before:
pp: case node.lt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → (erase x t_l).size = t_l.size - 1
t_ih_r' : x ∈ t_r → (erase x t_r).size = t_r.size - 1
h_mem : mem x t_l = true
t_ih_l : (erase x t_l).size = t_l.size - 1
⊢ ((erase x t_l).balanceR t_x t_r).size = (node size✝ t_l t_x t_r).size - 1

Tactic:
clear t_ih_l' t_ih_r'

Goal state after:
case node.lt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_l = true
t_ih_l : (erase x t_l).size = t_l.size - 1
⊢ ((erase x t_l).balanceR t_x t_r).size = (node size✝ t_l t_x t_r).size - 1
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.gt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → (erase x t_l).size = t_l.size - 1
t_ih_r' : x ∈ t_r → (erase x t_r).size = t_r.size - 1
h_mem : mem x t_r = true
t_ih_r : (erase x t_r).size = t_r.size - 1
⊢ (t_l.balanceL t_x (erase x t_r)).size = (node size✝ t_l t_x t_r).size - 1

Tactic:
clear t_ih_l' t_ih_r'

Goal state after:
case node.gt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : (erase x t_r).size = t_r.size - 1
⊢ (t_l.balanceL t_x (erase x t_r)).size = (node size✝ t_l t_x t_r).size - 1
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
x : F (α ::: Fix F α)
⊢ (mk x).dest = x

Tactic:
unfold Fix.dest
  rw [Fix.rec_eq, ← Fix.dest, ← comp_map]
  conv =>
    rhs
    rw [← MvFunctor.id_map x]
  rw [← appendFun_comp, id_comp]
  have : Fix.mk ∘ Fix.dest (F := F) (α := α) = _root_.id := by
    ext (x : Fix F α)
    apply Fix.mk_dest
  rw [this, appendFun_id_id]

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
⊢ ∀ {α β : TypeVec.{u} n} (f : α ⟹ β) (p : ↑(P F).wp α), Quot.mk WEquiv (f <$$> p) = f <$$> Quot.mk WEquiv p

Tactic:
by
    intro α β g x
    conv =>
      rhs
      dsimp [MvFunctor.map]
    rfl

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

Goal state before:
pp: case h.inr
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := fun x y ↦ x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
⊢ (Quot.factor r (fun x y ↦ x = y ∨ r x y) this ∘ Quot.mk r) <$> x.dest =
    (Quot.factor r (fun x y ↦ x = y ∨ r x y) this ∘ Quot.mk r) <$> y.dest

Tactic:
@comp_map _ q _ _ _ (Quot.mk r),

Goal state after:
case h.inr
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := fun x y ↦ x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
⊢ Quot.factor r (fun x y ↦ x = y ∨ r x y) this <$> Quot.mk r <$> x.dest =
    (Quot.factor r (fun x y ↦ x = y ∨ r x y) this ∘ Quot.mk r) <$> y.dest
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
⊢ Function.swap (LiftRelO R C) = LiftRelO (Function.swap R) (Function.swap C)

Tactic:
by
  funext x y
  rcases x with ⟨⟩ | ⟨hx, jx⟩ <;> rcases y with ⟨⟩ | ⟨hy, jy⟩ <;> rfl

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

Goal state before:
pp: α : Type u
c✝ : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct
c : Computation (WSeq α)
⊢ BisimO (fun c1 c2 ↦ c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct) (flatten c).destruct.destruct
    (c.bind destruct).destruct

Tactic:
by
      induction c using Computation.recOn with
      | pure a => simp; cases (destruct a).destruct <;> simp
      | think c' => simpa using Or.inr ⟨c', rfl, rfl⟩

Goal state after:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some.some
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
a b : α × WSeq α
h : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some a) (some b)
⊢ Option.rec nil Prod.snd (some a) ~ʷ Option.rec nil Prod.snd (some b)

Tactic:
· obtain ⟨a, s'⟩ := a
    obtain ⟨b, t'⟩ := b
    exact h.right

Goal state after:
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
β : Type v
f : α → β
S : WSeq (Computation α)
⊢ map f (parallel S) = parallel (WSeq.map (map f) S)

Tactic:
refine
    eq_of_bisim
      (fun c1 c2 =>
        ∃ l S,
          c1 = map f (corec parallel.aux1 (l, S)) ∧
            c2 = corec parallel.aux1 (l.map (map f), S.map (map f)))
      ?_ ⟨[], S, rfl, rfl⟩

Goal state after:
α : Type u
β : Type v
f : α → β
S : WSeq (Computation α)
⊢ IsBisimulation fun c1 c2 ↦
    ∃ l S, c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
Module: Mathlib.Data.Tree.Traversable

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

Tactic:
rw [traverse, traverse, η.preserves_pure]

Goal state after:
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:

Tactic:
f₂ g⁻¹ (f₁ g x) ≤ f₂ g⁻¹ (x + τ (f₁ g) + 1) :=
        mono _ (map_lt_add_translationNumber_add_one _ _).le
      _ = f₂ g⁻¹ (x + τ (f₂ g)) + 1 := by rw [h, map_add_one]
      _ ≤ x + τ (f₂ g) + τ (f₂ g⁻¹) + 1 + 1 := by grw [map_lt_add_translationNumber_add_one]
      _ = x + 2 := by simp [this, add_assoc, one_add_one_eq_two]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage

Goal state before:
pp: case h₁
α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
this : ν.InnerRegularCompactLTTop
s : Set Y
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
ε : ℝ≥0∞
hε : ε > 0
hso : IsOpen[inst✝⁵] s
hνs' : μ (⇑g ⁻¹' s) ≠ ∞
K : Set X
hKg : MapsTo (⇑g) K s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁹] K
hKμ : μ (⇑g ⁻¹' s \ K) < ε / 2
hKm : NullMeasurableSet K μ
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : MapsTo (⇑(f a)) K s
hK' : μ K ≠ ∞
⊢ μ (⇑g ⁻¹' s \ K) ≤ ε / 2

Tactic:
exact hKμ.le

Goal state after:
Module: Mathlib.Dynamics.Ergodic.Function

Goal state before:
pp: α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace X
inst✝¹ : MetrizableSpace X
inst✝ : Nonempty X
f : α → α
g : α → X
h : QuasiErgodic f μ
hgm : AEStronglyMeasurable g μ
hg_eq : g ∘ f =ᵐ[μ] g
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
⊢ ∃ c, g =ᵐ[μ] const α c

Tactic:
rcases hgm.isSeparable_ae_range with ⟨t, ht, hgt⟩

Goal state after:
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace X
inst✝¹ : MetrizableSpace X
inst✝ : Nonempty X
f : α → α
g : α → X
h : QuasiErgodic f μ
hgm : AEStronglyMeasurable g μ
hg_eq : g ∘ f =ᵐ[μ] g
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
t : Set X
ht : IsSeparable t
hgt : ∀ᵐ (x : α) ∂μ, g x ∈ t
⊢ ∃ c, g =ᵐ[μ] const α c
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst✝] n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst✝] (image2 ϕ v s)
⊢ ∃ u ∈ f, closure[inst✝] (image2 ϕ u s) ⊆ n

Tactic:
have hk : IsCompact (k \ n) :=
    (hc₁.of_isClosed_subset isClosed_closure hv₂).diff hn₁

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst✝] n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst✝] (image2 ϕ v s)
hk : IsCompact (k \ n)
⊢ ∃ u ∈ f, closure[inst✝] (image2 ϕ u s) ⊆ n