mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
hr : nil.Sized
⊢ (l.rotateL x nil).Sized

pp: case node
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : (node size✝ l✝ x✝ r✝).Sized
⊢ (l.rotateL x (node size✝ l✝ x✝ r✝)).Sized

Tactic:
· exact hl.node' hr

Goal state after:
case node
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : (node size✝ l✝ x✝ r✝).Sized
⊢ (l.rotateL x (node size✝ l✝ x✝ r✝)).Sized
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝ : l.size + r.size ≤ 1
⊢ (l.node' x r).Sized

pp: case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝¹ : ¬l.size + r.size ≤ 1
h✝ : r.size > delta * l.size
⊢ (l.rotateL x r).Sized

pp: case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : l.size > delta * r.size
⊢ (l.rotateR x r).Sized

pp: case neg
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : ¬l.size > delta * r.size
⊢ (l.node' x r).Sized

Tactic:
· exact hl.node' hr

Goal state after:
case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝¹ : ¬l.size + r.size ≤ 1
h✝ : r.size > delta * l.size
⊢ (l.rotateL x r).Sized

case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : l.size > delta * r.size
⊢ (l.rotateR x r).Sized

case neg
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : ¬l.size > delta * r.size
⊢ (l.node' x r).Sized
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case neg
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : ¬l.size > delta * r.size
⊢ (l.node' x r).Sized

Tactic:
· exact hl.node' hr

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : r.size = 0 → l.size ≤ 1
H₂ : 1 ≤ r.size → 1 ≤ l.size → l.size ≤ delta * r.size
H₃ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
⊢ Valid' o₁ (l.balanceR x r) o₂

Tactic:
rw [Valid'.dual_iff, dual_balanceR]

Goal state after:
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : r.size = 0 → l.size ≤ 1
H₂ : 1 ≤ r.size → 1 ≤ l.size → l.size ≤ delta * r.size
H₃ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
⊢ Valid' o₂ (r.dual.balanceL x l.dual) o₁
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'
⊢ Valid' o₁ (l.balanceR x r) o₂

Tactic:
rw [Valid'.dual_iff, dual_balanceR]

Goal state after:
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'
⊢ Valid' o₂ (r.dual.balanceL x l.dual) o₁
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₁ (Ordnode.node s l x r) o₂
⊢ Valid' (↑(l.findMin' x)) (l.node' x r).eraseMin o₂ ∧ (l.node' x r).size = (l.node' x r).eraseMin.size + 1

Tactic:
by
  have := H.dual.eraseMax_aux
  rwa [← dual_node', size_dual, ← dual_eraseMin, size_dual, ← Valid'.dual_iff, findMax'_dual]
    at this

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

Goal state before:
pp: v : PrimeMultiset
⊢ v.prod.factorMultiset.toNatMultiset = v.toNatMultiset

Tactic:
v.prod.coeNat_factorMultiset,

Goal state after:
v : PrimeMultiset
⊢ ↑(↑v.prod).primeFactorsList = v.toNatMultiset
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case mk
v : PrimeMultiset
l : List Nat.Primes
l' : List ℕ := List.map Subtype.val l
⊢ ↑(List.map Subtype.val l).prod.primeFactorsList = ↑(List.map Subtype.val l)

Tactic:
have (p : ℕ) (hp : p ∈ l') : p.Prime := by
    simp only [List.map_subtype, List.map_id_fun', id_eq, List.mem_unattach, l'] at hp
    obtain ⟨hp', -⟩ := hp
    exact hp'

Goal state after:
case mk
v : PrimeMultiset
l : List Nat.Primes
l' : List ℕ := List.map Subtype.val l
this : ∀ (p : ℕ), p ∈ l' → Nat.Prime p
⊢ ↑(List.map Subtype.val l).prod.primeFactorsList = ↑(List.map Subtype.val l)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : 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
h✝ : lrs < ratio * lls
⊢ (node lls lll llx llr).node3R lx (node lrs lrl lrx lrr) x nil =
    node (lls + lrs + 1 + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)

Tactic:
simp [node3R, node']

Goal state after:
case pos
α : 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
h✝ : lrs < ratio * lls
⊢ lls + (lrs + 1) = lls + lrs + 1
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: x✝ : XgcdType
u : XgcdType := x✝
h : ¬u.r = 0
hs : x✝.IsSpecial
⊢ x✝.reduce.IsSpecial

Tactic:
by
      have : SizeOf.sizeOf u.step < SizeOf.sizeOf u := u.step_wf h
      rw [reduce_b h]
      exact (flip_isSpecial _).mpr (reduce_isSpecial _ (u.step_isSpecial hs))

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

Goal state before:
pp: case h.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
u : F fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : (P F).A
f : (P F).B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ x = abs ⟨a, fun i j ↦ (↑(f i j)).1⟩

Tactic:
← xeq,

Goal state after:
case h.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
u : F fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : (P F).A
f : (P F).B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ (fun i t ↦ (↑t).1) <$$> u = abs ⟨a, fun i j ↦ (↑(f i j)).1⟩
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case right.right.right.left
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑(z * a') = (x * ↑b').succ

Tactic:
Nat.succ_eq_add_one,

Goal state after:
case right.right.right.left
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑(z * a') = x * ↑b' + 1
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case right.right.right.right.left
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑(w * b') = (y * ↑a').succ

Tactic:
Nat.succ_eq_add_one,

Goal state after:
case right.right.right.right.left
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑(w * b') = y * ↑a' + 1
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h.left
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
u : F { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : (P F).A
f : (P F).B a → { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ x = abs ⟨a, fun i ↦ (↑(f i)).1⟩

Tactic:
← xeq,

Goal state after:
case h.left
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
u : F { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : (P F).A
f : (P F).B a → { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ (fun t ↦ (↑t).1) <$> u = abs ⟨a, fun i ↦ (↑(f i)).1⟩
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Ordset α
h : (↑s).empty = true
⊢ s = ∅

Tactic:
cases s with | mk s_val _ => cases s_val <;> [rfl; cases h]

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

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
x : F α
u : α
⊢ u ∈ supp x ↔ ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ

Tactic:
by
  rw [supp]; dsimp; constructor
  · intro h a f haf
    have : Liftp (fun u => u ∈ f '' univ) x := by
      rw [liftp_iff]
      exact ⟨a, f, haf.symm, fun i => mem_image_of_mem _ (mem_univ _)⟩
    exact h this
  intro h p; rw [liftp_iff]
  rintro ⟨a, f, xeq, h'⟩
  rcases h a f xeq.symm with ⟨i, _, hi⟩
  rw [← hi]; apply h'

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
b : β
h : b ∈ t
⊢ ∃ a ∈ s, R a b

Tactic:
rw [← LiftRel.swap] at H; exact exists_of_liftRel_left H h

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

Goal state before:
pp: case none
α : Type u
β : Type v
f : α → β
b : β
g : Stream' (Option (Option α))
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
om : none ∈ ⟨g, al⟩
oe : Option.map f none = some b
⊢ ∃ a ∈ ⟨g, al⟩, f a = b

pp: case some
α : Type u
β : Type v
f : α → β
b : β
g : Stream' (Option (Option α))
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
a : α
om : some a ∈ ⟨g, al⟩
oe : Option.map f (some a) = some b
⊢ ∃ a ∈ ⟨g, al⟩, f a = b

Tactic:
· injection oe

Goal state after:
case some
α : Type u
β : Type v
f : α → β
b : β
g : Stream' (Option (Option α))
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
a : α
om : some a ∈ ⟨g, al⟩
oe : Option.map f (some a) = some b
⊢ ∃ a ∈ ⟨g, al⟩, f a = b
Module: Mathlib.Data.String.Basic

Goal state before:
pp: c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c } =
    ltb s₁.next s₂.next
⊢ { s := ofList s₂.s.toList, i := s₂.i }.hasNext = true

Tactic:
simpa using h₁

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

Goal state before:
pp: c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : ¬s₁.curr = s₂.curr
⊢ { s := ofList s₂.s.toList, i := s₂.i }.hasNext = true

Tactic:
simpa using h₁

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

Goal state before:
pp: c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : ¬s₁.hasNext = true
⊢ { s := ofList s₂.s.toList, i := s₂.i }.hasNext = true

Tactic:
simpa using h₁

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

Goal state before:
pp: c : Char
s₁ s₂ : Legacy.Iterator
h₁ : ¬s₂.hasNext = true
⊢ ¬{ s := ofList s₂.s.toList, i := s₂.i }.hasNext = true

Tactic:
simpa using h₁

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

Goal state before:
pp: c : Char
s₁ s₂ : Legacy.Iterator
⊢ ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c } { s := ofList (c :: s₂.s.toList), i := s₂.i + c } = ltb s₁ s₂

Tactic:
fun_induction ltb s₁ s₂ with
  | case1 s₁ s₂ h₁ h₂ h ih =>
    rw [ltb, Legacy.Iterator.hasNext_cons_addChar, Legacy.Iterator.hasNext_cons_addChar,
      if_pos (by simpa using h₁), if_pos (by simpa using h₂), if_pos, ← ih]
    · simp only [Legacy.Iterator.next, Pos.Raw.next, get_cons_addChar, ofList_toList]
      congr 2 <;> apply Pos.Raw.add_char_right_comm
    · simpa only [Legacy.Iterator.curr, get_cons_addChar, ofList_toList] using h
  | case2 s₁ s₂ h₁ h₂ h =>
    rw [ltb, Legacy.Iterator.hasNext_cons_addChar, Legacy.Iterator.hasNext_cons_addChar,
      if_pos (by simpa using h₁), if_pos (by simpa using h₂), if_neg]
    · simp only [Legacy.Iterator.curr, get_cons_addChar, ofList_toList]
    · simpa only [Legacy.Iterator.curr, get_cons_addChar, ofList_toList] using h
  | case3 s₁ s₂ h₁ h₂ =>
    rw [ltb, Legacy.Iterator.hasNext_cons_addChar, Legacy.Iterator.hasNext_cons_addChar,
      if_pos (by simpa using h₁), if_neg (by simpa using h₂)]
  | case4 s₁ s₂ h₁ =>
    rw [ltb, Legacy.Iterator.hasNext_cons_addChar, if_neg (by simpa using h₁)]

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
n : ℕ
xs : Vector α n
ys : Vector β n
f₁ : γ → β → ζ
f₂ : α → γ
⊢ map₂ f₁ (map f₂ xs) ys = map₂ (fun x y ↦ f₁ (f₂ x) y) xs ys

Tactic:
induction xs, ys using Vector.revInductionOn₂ <;> simp_all

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
n : ℕ
xs : Vector α n
ys : Vector β n
f₁ : α → γ → ζ
f₂ : β → γ
⊢ map₂ f₁ xs (map f₂ ys) = map₂ (fun x y ↦ f₁ x (f₂ y)) xs ys

Tactic:
induction xs, ys using Vector.revInductionOn₂ <;> simp_all

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
n : ℕ
xs : Vector α n
ys : Vector β n
f₁ : γ → ζ
f₂ : α → β → γ
⊢ map f₁ (map₂ f₂ xs ys) = map₂ (fun x y ↦ f₁ (f₂ x y)) xs ys

Tactic:
induction xs, ys using Vector.revInductionOn₂ <;> simp_all

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → γ
⊢ map₂ f xs ys = (mapAccumr₂ (fun x y x_1 ↦ ((), f x y)) xs ys ()).2

Tactic:
induction xs, ys using Vector.revInductionOn₂ <;> simp_all

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

Goal state before:
pp: α : Type u
s : WSeq α
inst✝ : s.Productive
n m : ℕ
⊢ ((s.drop n).get? m).Terminates

Tactic:
← get?_add

Goal state after:
α : Type u
s : WSeq α
inst✝ : s.Productive
n m : ℕ
⊢ (s.get? (n + m)).Terminates
Module: Mathlib.Data.WSeq.Defs

Goal state before:
pp: case nil
α : Type u
s : WSeq α
s1 s2 : Computation ℕ
l : List α
h :
  s1 =
      Computation.corec
        (fun x ↦
          match x with
          | (n, s) =>
            match Seq.destruct s with
            | none => Sum.inl n
            | some (none, s') => Sum.inr (n, s')
            | some (some val, s') => Sum.inr (n + 1, s'))
        (l.length, nil) ∧
    s2 =
      Computation.map List.length
        (Computation.corec
          (fun x ↦
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l, nil))
⊢ Computation.BisimO
    (fun c1 c2 ↦
      ∃ l s,
        c1 =
            Computation.corec
              (fun x ↦
                match x with
                | (n, s) =>
                  match Seq.destruct s with
                  | none => Sum.inl n
                  | some (none, s') => Sum.inr (n, s')
                  | some (some val, s') => Sum.inr (n + 1, s'))
              (l.length, s) ∧
          c2 =
            Computation.map List.length
              (Computation.corec
                (fun x ↦
                  match x with
                  | (l, s) =>
                    match Seq.destruct s with
                    | none => Sum.inl l.reverse
                    | some (none, s') => Sum.inr (l, s')
                    | some (some a, s') => Sum.inr (a :: l, s'))
                (l, s)))
    (Computation.corec
        (fun x ↦
          match x with
          | (n, s) =>
            match Seq.destruct s with
            | none => Sum.inl n
            | some (none, s') => Sum.inr (n, s')
            | some (some val, s') => Sum.inr (n + 1, s'))
        (l.length, nil)).destruct
    (Computation.map List.length
        (Computation.corec
          (fun x ↦
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l, nil))).destruct

Tactic:
simp [nil]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
g : α → β
hg : MeasurePreserving g μ μ'
hf : PreErgodic f μ
f' : β → β
h_comm : Semiconj g f f'
s : Set β
hs₀ : MeasurableSet s
hs₁ : f' ⁻¹' s = s
⊢ g ⁻¹' f' ⁻¹' s = g ⁻¹' s

Tactic:
hs₁

Goal state after:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
g : α → β
hg : MeasurePreserving g μ μ'
hf : PreErgodic f μ
f' : β → β
h_comm : Semiconj g f f'
s : Set β
hs₀ : MeasurableSet s
hs₁ : f' ⁻¹' s = s
⊢ g ⁻¹' s = g ⁻¹' s
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ (⇑f)^[n] x ≤ x + ↑n * ↑m ↔ f x ≤ x + ↑m

Tactic:
by
  simpa only [nsmul_eq_mul, add_right_iterate] using
    (f.commute_add_int m).iterate_pos_le_iff_map_le f.monotone (strictMono_id.add_const (m : ℝ)) hn

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

Goal state before:
pp: f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C
n : ℕ
this : 0 < 2 ^ n
⊢ dist (f.transnumAuxSeq n) (x (2 ^ n) / 2 ^ n) ≤ C / 2 ^ n

Tactic:
convert! (div_le_div_iff_of_pos_right this).2 (H (2 ^ n)) using 1

Goal state after:
case e'_3
f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C
n : ℕ
this : 0 < 2 ^ n
⊢ dist (f.transnumAuxSeq n) (x (2 ^ n) / 2 ^ n) = dist ((f ^ 2 ^ n) 0) (x (2 ^ n)) / 2 ^ n
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
⊢ f x < x + ↑⌊τ f⌋ + 1

Tactic:
rw [add_assoc]
  norm_cast
  refine map_lt_of_translationNumber_lt_int _ ?_ _
  push_cast
  exact lt_floor_add_one _

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

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
⊢ x + ↑⌊τ f⌋ + 1 ≤ x + τ f + 1

Tactic:
by gcongr; apply floor_le

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g ↦ (f₂ g⁻¹) ((f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits
F₂ : G →* ℝ ≃o ℝ := toOrderIso.comp f₂.toHomUnits
hF₁ : ∀ (g : G), ⇑(F₁ g) = ⇑(f₁ g)
hF₂ : ∀ (g : G), ⇑(F₂ g) = ⇑(f₂ g)
⊢ ∃ F, ∀ (g : G), Semiconj ⇑F ⇑(f₁ g) ⇑(f₂ g)

Tactic:
refine ⟨⟨⟨fun x ↦ ⨆ g', (F₂ g')⁻¹ (F₁ g' x), fun x y hxy => ?_⟩, fun x => ?_⟩,
    csSup_div_semiconj F₂ F₁ fun x => ?_⟩

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g ↦ (f₂ g⁻¹) ((f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits
F₂ : G →* ℝ ≃o ℝ := toOrderIso.comp f₂.toHomUnits
hF₁ : ∀ (g : G), ⇑(F₁ g) = ⇑(f₁ g)
hF₂ : ∀ (g : G), ⇑(F₂ g) = ⇑(f₂ g)
x y : ℝ
hxy : x ≤ y
⊢ (fun x ↦ ⨆ g', (F₂ g')⁻¹ ((F₁ g') x)) x ≤ (fun x ↦ ⨆ g', (F₂ g')⁻¹ ((F₁ g') x)) y

case refine_2
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g ↦ (f₂ g⁻¹) ((f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits
F₂ : G →* ℝ ≃o ℝ := toOrderIso.comp f₂.toHomUnits
hF₁ : ∀ (g : G), ⇑(F₁ g) = ⇑(f₁ g)
hF₂ : ∀ (g : G), ⇑(F₂ g) = ⇑(f₂ g)
x : ℝ
⊢ { toFun := fun x ↦ ⨆ g', (F₂ g')⁻¹ ((F₁ g') x), monotone' := ⋯ }.toFun (x + 1) =
    { toFun := fun x ↦ ⨆ g', (F₂ g')⁻¹ ((F₁ g') x), monotone' := ⋯ }.toFun x + 1

case refine_3
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g ↦ (f₂ g⁻¹) ((f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits
F₂ : G →* ℝ ≃o ℝ := toOrderIso.comp f₂.toHomUnits
hF₁ : ∀ (g : G), ⇑(F₁ g) = ⇑(f₁ g)
hF₂ : ∀ (g : G), ⇑(F₂ g) = ⇑(f₂ g)
x : ℝ
⊢ BddAbove (range fun g ↦ (F₂ g)⁻¹ ((F₁ g) x))
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hsm : NullMeasurableSet s μ
hs₀ : μ s ≠ 0
t : Set α
hsub : t ⊆ s
htm : MeasurableSet t
hts : t =ᵐ[μ] s
⊢ μ t ≠ 0

Tactic:
by rwa [measure_congr hts]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hsm : NullMeasurableSet s μ
hs₀ : μ s ≠ 0
⊢ ∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[m] x ∈ s

Tactic:
rcases hsm.exists_measurable_subset_ae_eq with ⟨t, hsub, htm, hts⟩
  rcases hf.exists_mem_iterate_mem' htm (by rwa [measure_congr hts]) with ⟨x, hxt, m, hm₀, hmt⟩
  exact ⟨x, hsub hxt, m, hm₀, hsub hmt⟩

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᵐ[ν] μ.rnDeriv (ν.withDensity f)

Tactic:
by
  conv_rhs => rw [μ.haveLebesgueDecomposition_add ν, add_comm]
  have hν_ac : ν ≪ ν.withDensity f := withDensity_absolutelyContinuous' hf hf_ne_zero
  refine hν_ac.ae_eq ?_
  have : SigmaFinite (ν.withDensity f) := SigmaFinite.withDensity_of_ne_top hf_ne_top
  refine (rnDeriv_add_of_mutuallySingular _ _ _ ?_).symm
  exact ((mutuallySingular_singularPart μ ν).symm.withDensity).symm

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞

Tactic:
refine ae_restrict_of_ae ?_
      exact Measure.rnDeriv_lt_top _ _

Goal state after: