mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: case refine_2.rel
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
x✝ y✝ : P.M α
a✝ : R x✝ y✝
⊢ (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x✝ =
    (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P y✝

Tactic:
rw [← Quot.factor_mk_eq R (Relation.EqvGen R) this]

Goal state after:
case refine_2.rel
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
x✝ y✝ : P.M α
a✝ : R x✝ y✝
⊢ (TypeVec.id ::: Quot.factor R (Relation.EqvGen R) this ∘ Quot.mk R) <$$> dest P x✝ =
    (TypeVec.id ::: Quot.factor R (Relation.EqvGen R) this ∘ Quot.mk R) <$$> dest P y✝
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

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

case nil.node.node
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx rr).Balanced
sr : (node rs (node rls rll rlx rlr) rx rr).Sized
⊢ nil.balance x ((node rls rll rlx rlr).node' rx rr) = nil.balance' x ((node rls rll rlx rlr).node' rx rr)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case tail.refl
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
this : Inhabited P.A
a : P.A
f f' : P.B a → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : P.B a
g' : P.B a → P.M
h₁ : ⟨a, f'⟩ = ⟨a, g'⟩
h₂ : ∀ (i : P.B a), R (f i) (g' i)
⊢ R (f i) (f' i)

Tactic:
cases h₁

Goal state after:
case tail.refl.refl
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
this : Inhabited P.A
a : P.A
f f' : P.B a → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : P.B a
h₂ : ∀ (i : P.B a), R (f i) (f' i)
⊢ R (f i) (f' i)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case pos
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun x ↦ All (fun y ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h✝ : ls > rs
v : Valid' o₁ (ll.node' lx lr).eraseMax ↑(findMax' lx lr)
e : (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1
⊢ BalancedSz (ll.node' lx lr).size (Ordnode.node rs rl rx rr).size

Tactic:
hl.2.eq_node'

Goal state after:
case pos
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun x ↦ All (fun y ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (ll.node' lx lr).size (Ordnode.node rs rl rx rr).size
h✝ : ls > rs
v : Valid' o₁ (ll.node' lx lr).eraseMax ↑(findMax' lx lr)
e : (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1
⊢ BalancedSz (ll.node' lx lr).size (Ordnode.node rs rl rx rr).size
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a b : Σₗ' (i : ι), α i
⊢ a ≤ b ∧ ¬b ≤ a → a < b

Tactic:
rintro ⟨⟨j, b, hij⟩ | ⟨i, hab⟩, hba⟩
        · exact Lex.left _ _ hij
        · exact Lex.right _ (hab.lt_of_not_ge fun h => hba <| Lex.right _ h)

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

Goal state before:
pp: case pos
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : delta * ls < rs
rd : delta ≤ rl.size + rr.size
⊢ (node ls ll lx lr).rotateL x (node rs rl rx rr) =
    rec nil
      (fun size l x_1 r l_ih r_ih ↦
        rec nil
          (fun size_1 l_1 x_2 r_1 l_ih r_ih ↦
            if size < ratio * size_1 then node (ls + rs + 1) (node (ls + size + 1) (node ls ll lx lr) x rl) rx rr
            else
              node (ls + rs + 1) (node (ls + l.size + 1) (node ls ll lx lr) x l) x_1
                (node (r.size + size_1 + 1) r rx rr))
          rr)
      rl

Tactic:
obtain - | ⟨rls, rll, rlx, rlr⟩ := rl

Goal state after:
case pos.nil
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rx : α
rr : Ordnode α
h : delta * ls < rs
hr : (node rs nil rx rr).Balanced
sr : (node rs nil rx rr).Sized
rd : delta ≤ nil.size + rr.size
⊢ (node ls ll lx lr).rotateL x (node rs nil rx rr) =
    rec nil
      (fun size l x_1 r l_ih r_ih ↦
        rec nil
          (fun size_1 l_1 x_2 r_1 l_ih r_ih ↦
            if size < ratio * size_1 then node (ls + rs + 1) (node (ls + size + 1) (node ls ll lx lr) x nil) rx rr
            else
              node (ls + rs + 1) (node (ls + l.size + 1) (node ls ll lx lr) x l) x_1
                (node (r.size + size_1 + 1) r rx rr))
          rr)
      nil

case pos.node
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rx : α
rr : Ordnode α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : (node rs (node rls rll rlx rlr) rx rr).Balanced
sr : (node rs (node rls rll rlx rlr) rx rr).Sized
rd : delta ≤ (node rls rll rlx rlr).size + rr.size
⊢ (node ls ll lx lr).rotateL x (node rs (node rls rll rlx rlr) rx rr) =
    rec nil
      (fun size l x_1 r l_ih r_ih ↦
        rec nil
          (fun size_1 l_1 x_2 r_1 l_ih r_ih ↦
            if size < ratio * size_1 then
              node (ls + rs + 1) (node (ls + size + 1) (node ls ll lx lr) x (node rls rll rlx rlr)) rx rr
            else
              node (ls + rs + 1) (node (ls + l.size + 1) (node ls ll lx lr) x l) x_1
                (node (r.size + size_1 + 1) r rx rr))
          rr)
      (node rls rll rlx rlr)
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: a b : ℕ+
⊢ (1 * (↑a - 1 + 1) + 0 * (↑b - 1 + 1), 0 * (↑a - 1 + 1) + 1 * (↑b - 1 + 1)) = (↑a, ↑b)

Tactic:
have := a.pos

Goal state after:
a b : ℕ+
this : 0 < ↑a
⊢ (1 * (↑a - 1 + 1) + 0 * (↑b - 1 + 1), 0 * (↑a - 1 + 1) + 1 * (↑b - 1 + 1)) = (↑a, ↑b)
Module: Mathlib.Data.Ordmap.Invariants

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

Tactic:
simp only [balance, id_eq, balance', size_node, gt_iff_lt]
      symm; rw [if_neg]
      · split_ifs with h h_1
        · have rd : delta ≤ size rl + size rr := by
            have := lt_of_le_of_lt (Nat.mul_le_mul_left _ sl.pos) h
            rwa [sr.1, Nat.lt_succ_iff] at this
          obtain - | ⟨rls, rll, rlx, rlr⟩ := rl
          · rw [size, zero_add] at rd
            exact absurd (le_trans rd (balancedSz_zero.1 hr.1.symm)) (by decide)
          obtain - | ⟨rrs, rrl, rrx, rrr⟩ := rr
          · exact absurd (le_trans rd (balancedSz_zero.1 hr.1)) (by decide)
          dsimp [rotateL]; split_ifs
          · simp [node3L, node', sr.1]; abel
          · simp [node4L, node', sr.1, sr.2.1.1]; abel
        · have ld : delta ≤ size ll + size lr := by
            have := lt_of_le_of_lt (Nat.mul_le_mul_left _ sr.pos) h_1
            rwa [sl.1, Nat.lt_succ_iff] at this
          obtain - | ⟨lls, lll, llx, llr⟩ := ll
          · rw [size, zero_add] at ld
            exact absurd (le_trans ld (balancedSz_zero.1 hl.1.symm)) (by decide)
          obtain - | ⟨lrs, lrl, lrx, lrr⟩ := lr
          · exact absurd (le_trans ld (balancedSz_zero.1 hl.1)) (by decide)
          dsimp [rotateR]; split_ifs
          · simp [node3R, node', sl.1]; abel
          · simp [node4R, node', sl.1, sl.2.2.1]; abel
        · simp [node']
      · exact not_le_of_gt (add_le_add (Nat.succ_le_of_lt sl.pos) (Nat.succ_le_of_lt sr.pos))

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

Goal state before:
pp: case right.right.right.left
a b : ℕ+
d : ℕ+ := ⋯
w : ℕ+ := ⋯
x : ℕ := ⋯
y : ℕ := ⋯
z : ℕ+ := ⋯
a' : ℕ+ := ⋯
b' : ℕ+ := ⋯
u : XgcdType := ⋯
ur : XgcdType := ⋯
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').succPNat

Tactic:
apply eq

Goal state after:
case right.right.right.left
a b : ℕ+
d : ℕ+ := ⋯
w : ℕ+ := ⋯
x : ℕ := ⋯
y : ℕ := ⋯
z : ℕ+ := ⋯
a' : ℕ+ := ⋯
b' : ℕ+ := ⋯
u : XgcdType := ⋯
ur : XgcdType := ⋯
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').succPNat
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case right.right.right.right.left
a b : ℕ+
d : ℕ+ := ⋯
w : ℕ+ := ⋯
x : ℕ := ⋯
y : ℕ := ⋯
z : ℕ+ := ⋯
a' : ℕ+ := ⋯
b' : ℕ+ := ⋯
u : XgcdType := ⋯
ur : XgcdType := ⋯
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').succPNat

Tactic:
apply eq

Goal state after:
case right.right.right.right.left
a b : ℕ+
d : ℕ+ := ⋯
w : ℕ+ := ⋯
x : ℕ := ⋯
y : ℕ := ⋯
z : ℕ+ := ⋯
a' : ℕ+ := ⋯
b' : ℕ+ := ⋯
u : XgcdType := ⋯
ur : XgcdType := ⋯
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').succPNat
Module: Mathlib.Data.QPF.Multivariate.Constructions.Sigma

Goal state before:
pp: n : ℕ
A : Type u
F : A → TypeVec.{u} n → Type u
inst✝ : (α : A) → MvQPF (F α)
⊢ ∀ {α : TypeVec.{u} n} (x : Pi F α), Pi.abs F (Pi.repr F x) = x

Tactic:
rintro α f

Goal state after:
n : ℕ
A : Type u
F : A → TypeVec.{u} n → Type u
inst✝ : (α : A) → MvQPF (F α)
α : TypeVec.{u} n
f : Pi F α
⊢ Pi.abs F (Pi.repr F f) = f
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), WEquiv (wrepr (f i)) (f i)
⊢ abs ((P F).wDest' (wrepr ((P F).wMk a f' f))) =
    abs ((P F).wDest' ((P F).wMk' ((TypeVec.id ::: wrepr) <$$> ⟨a, (P F).appendContents f' f⟩)))

Tactic:
rw [wrepr_wMk, q.P.wDest'_wMk', q.P.wDest'_wMk', abs_repr]

Goal state after:
Module: Mathlib.Data.Rat.Star

Goal state before:
pp: ⊢ closure (range fun x ↦ x * x) = ⊤

Tactic:
simpa only [sq] using addSubmonoid_closure_range_pow two_ne_zero

Goal state after:
Module: Mathlib.Data.Rat.Star

Goal state before:
pp: case e'_2
n : ℕ
hn₀ : n ≠ 0
hn : Even n
⊢ (range fun x ↦ x ^ n) = ⇑NNRat.coeHom '' range fun x ↦ x ^ n

Tactic:
have (x : ℚ) : ∃ y : ℚ≥0, y ^ n = x ^ n := ⟨x.nnabs, by simp [hn.pow_abs]⟩

Goal state after:
case e'_2
n : ℕ
hn₀ : n ≠ 0
hn : Even n
this : ∀ (x : ℚ), ∃ y, ↑y ^ n = x ^ n
⊢ (range fun x ↦ x ^ n) = ⇑NNRat.coeHom '' range fun x ↦ x ^ n
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : WSeq α
n : ℕ
⊢ s.think.drop n = (s.drop n).think

Tactic:
by
  induction n <;> simp [*, drop]

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

Goal state before:
pp: α : Type u
s : WSeq α
a : α
n : ℕ
h : some a ∈ s.get? n
⊢ ∃ a', some a' ∈ s.head

Tactic:
by
  induction n generalizing a with
  | zero => exact ⟨_, h⟩
  | succ n IH =>
      let ⟨a', h'⟩ := head_some_of_head_tail_some h
      exact IH h'

Goal state after:
Module: Mathlib.Data.Set.FiniteExhaustion

Goal state before:
pp: case neg
α : Type u_1
s✝ : Set α
K : s✝.FiniteExhaustion
s : Set α
hs : s.Countable
h : ¬Nonempty ↑s
⊢ Nonempty s.FiniteExhaustion

Tactic:
refine ⟨fun _ ↦ ∅, by simp [Finite.to_subtype], fun n ↦ by simp, ?_⟩

Goal state after:
case neg
α : Type u_1
s✝ : Set α
K : s✝.FiniteExhaustion
s : Set α
hs : s.Countable
h : ¬Nonempty ↑s
⊢ ⋃ n, ∅ = s
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some.some
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
a : α × WSeq α
dsm : some a ∈ s.destruct
dse : Prod.fst <$> some a = o
b : α × WSeq α
dtm : some b ∈ t.destruct
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some a) (some b)
⊢ Prod.fst <$> some a ∈ t.head

Tactic:
obtain ⟨a, s'⟩ := a
    obtain ⟨b, t'⟩ := b
    rw [dst.left]
    exact @Computation.mem_map _ _ (@Functor.map _ _ (α × WSeq α) _ Prod.fst)
      (some (b, t')) (destruct t) dtm

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

Goal state before:
pp: case inr.inr
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? 0
H : S.destruct = some (some c, S.tail)
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
· have C : corec parallel.aux1 (l, S) = _ := destruct_eq_think (by
        simp only [corec_eq, rmap, parallel.aux1.eq_1]
        rw [h, H])
      rw [C]
      refine @Computation.think_terminates _ _ ?_
      apply terminates_parallel.aux _ T
      simp

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

Goal state before:
pp: case none.none
α : Type u
β : Type v
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t ↦ LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
h : LiftRelO R (LiftRel R) none none
⊢ Computation.LiftRel
    (LiftRelO R fun s t ↦ LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x)
    (destruct_append.aux s2 none) (destruct_append.aux t2 none)

Tactic:
simp only [destruct_append.aux]

Goal state after:
case none.none
α : Type u
β : Type v
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t ↦ LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
h : LiftRelO R (LiftRel R) none none
⊢ Computation.LiftRel
    (LiftRelO R fun s t ↦ LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x) s2.destruct
    t2.destruct
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:
by 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:
by 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:
by 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:
by simpa using h₁

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : WSeq α
f : α → WSeq β
g : β → WSeq γ
⊢ (s.bind f).bind g ~ʷ s.bind ((fun y ↦ y.bind g) ∘ f)

Tactic:
simp only [bind, map_join]

Goal state after:
α : Type u
β : Type v
γ : Type w
s : WSeq α
f : α → WSeq β
g : β → WSeq γ
⊢ (map (map g) (map f s)).join.join ~ʷ (map ((fun y ↦ (map g y).join) ∘ f) s).join
Module: Mathlib.Data.Vector3

Goal state before:
pp: α : Type u_1
m n : ℕ
C : Vector3 α 0 → Sort u
H : C []
v : Vector3 α 0
⊢ C v

Tactic:
eq_nil v

Goal state after:
α : Type u_1
m n : ℕ
C : Vector3 α 0 → Sort u
H : C []
v : Vector3 α 0
⊢ C []
Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage

Goal state before:
pp: α : 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)
s : Set Y
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
this✝ : ν.InnerRegularCompactLTTop
ε : ℝ≥0∞
hε : ε > 0
this :
  ∀ {s : Set Y},
    NullMeasurableSet s ν → ν s ≠ ∞ → ∀ ε > 0, IsOpen[inst✝⁵] s → ∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε
hso : ¬IsOpen[inst✝⁵] s
H : 0 < ε / 3
U : Set Y
hUo : IsOpen[inst✝⁵] U
hU : ν U < ∞
hmU : NullMeasurableSet U ν
hUs : ν (U ∆ s) ≤ ε / 3
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : μ ((⇑(f a) ⁻¹' U) ∆ (⇑g ⁻¹' U)) ≤ ε / 3
⊢ μ ((⇑(f a) ⁻¹' s) ∆ (⇑(f a) ⁻¹' U)) + μ ((⇑(f a) ⁻¹' U) ∆ (⇑g ⁻¹' U)) + μ ((⇑g ⁻¹' U) ∆ (⇑g ⁻¹' s)) ≤
    ε / 3 + ε / 3 + ε / 3

Tactic:
by
        gcongr
        · rwa [← preimage_symmDiff, hfa.measure_preimage (hs.symmDiff hmU), symmDiff_comm]
        · rwa [← preimage_symmDiff, hg.measure_preimage (hmU.symmDiff hs)]

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

Goal state before:
pp: f : CircleDeg1Lift
hf : Continuous ⇑f
n : ℕ
⊢ Continuous (⇑f)^[n]

Tactic:
exact hf.iterate n

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
this : ⇑e ∘ f ∘ ⇑e.symm = fun y ↦ n • y
⊢ Ergodic (fun y ↦ n • y) volume

Tactic:
exact ergodic_zsmul h

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

Goal state before:
pp: case map_eq
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hs : MeasurableSet s
⊢ (map f (ν.withDensity (μ.rnDeriv ν))) s = (ν.withDensity (μ.rnDeriv ν)) s

Tactic:
rw [← ENNReal.add_left_inj (measure_ne_top (μ.singularPart ν) s), map_apply hfμ.measurable hs,
    ← add_apply, rnDeriv_add_singularPart,
    ← (hfμ.singularPart hfν).measure_preimage hs.nullMeasurableSet, ← add_apply,
    rnDeriv_add_singularPart, hfμ.measure_preimage hs.nullMeasurableSet]

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

Goal state before:
pp: case h
X : Type u_1
m : MeasurableSpace X
μ✝ ν : Measure X
inst✝¹ : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst✝ : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := ⋯
hsm : MeasurableSet s
hν_sdiff : ν (f ⁻¹' s \ s) = ν (s \ f ⁻¹' s)
h₀ : ν (f ⁻¹' s \ s) ≠ 0
⊢ ∀ᵐ (x : X) ∂ν, x ∈ s \ f ⁻¹' s → μ.rnDeriv ν x < c

Tactic:
exact .of_forall fun x hx ↦ hx.1

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

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

Tactic:
have : SigmaFinite (ν.withDensity f) := SigmaFinite.withDensity_of_ne_top hf_ne_top
  refine (withDensity_absolutelyContinuous' hf hf_ne_zero).ae_eq ?_
  refine (Measure.eq_rnDeriv₀ (ν := ν.withDensity f) ?_ Measure.MutuallySingular.zero_left ?_).symm
  · exact (hf.inv.mono_ac (withDensity_absolutelyContinuous _ _)).mul
      (Measure.measurable_rnDeriv _ _).aemeasurable
  · ext1 s hs
    conv_lhs => rw [← Measure.withDensity_rnDeriv_eq _ _ hμν]
    rw [zero_add, withDensity_apply _ hs, withDensity_apply _ hs]
    rw [setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀ _ _ _ hs]
    · simp only [Pi.mul_apply]
      have : (fun a ↦ f a * ((f a)⁻¹ * μ.rnDeriv ν a)) =ᵐ[ν] μ.rnDeriv ν := by
        filter_upwards [hf_ne_zero, hf_ne_top] with x hx1 hx2
        simp [← mul_assoc, ENNReal.mul_inv_cancel, hx1, hx2]
      rw [lintegral_congr_ae (ae_restrict_of_ae this)]
    · refine ae_restrict_of_ae ?_
      filter_upwards [hf_ne_top] with x hx using hx.lt_top
    · exact hf.restrict

Goal state after:
Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage

Goal state before:
pp: case succ
X : Type u_1
T : X → X
U : SetRel X X
inst✝ : UniformSpace X
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
ih : ⋂ i, ⋂ (_ : i < n), (map T T)^[i] ⁻¹' U ∈ 𝓤 X
⊢ (map T T)^[n] ⁻¹' U ∈ 𝓤 X

Tactic:
map_iterate T T n

Goal state after:
case succ
X : Type u_1
T : X → X
U : SetRel X X
inst✝ : UniformSpace X
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
ih : ⋂ i, ⋂ (_ : i < n), (map T T)^[i] ⁻¹' U ∈ 𝓤 X
⊢ map T^[n] T^[n] ⁻¹' U ∈ 𝓤 X
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
⊢ y ∈ ω f ϕ s ↔ ∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, (ϕ t '' s ∩ n).Nonempty

Tactic:
simp_rw [mem_omegaLimit_iff_frequently, image_inter_nonempty_iff]

Goal state after:
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: case neg
A : Type u_3
G : Type u_4
inst✝¹ : Finite A
inst✝ : Inhabited A
val✝ : Fintype A
cfg : G → A
dom : Finset G
cond : ∀ g ∉ dom, cfg g = default
g : G
hg : g ∉ dom
⊢ (if h : g ∈ dom then cfg g else default) = cfg g

Tactic:
· simp [hg, cond g hg]

Goal state after:
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: case intro
A : Type u_3
G : Type u_4
inst✝¹ : Finite A
inst✝ : Inhabited A
U : Finset G
val✝ : Fintype A
e : { p // p.support = U } ≃ (↥U → A) :=
  { toFun := fun p i ↦ (↑p).config ↑i,
    invFun := fun f ↦ ⟨{ config := fun g ↦ if h : g ∈ U then f ⟨g, h⟩ else default, support := U, condition := ⋯ }, ⋯⟩,
    left_inv := ⋯, right_inv := ⋯ }
this : Fintype ↑{p | p.support = U} := Fintype.ofEquiv (↥U → A) e.symm
⊢ {p | p.support = U}.Finite

Tactic:
apply toFinite

Goal state after: