mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Vector.Snoc

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
n : ℕ
x : α
xs : Vector α n
ys : Vector β n
f : α → β → σ
y : β
⊢ map₂ f (xs.snoc x) (ys.snoc y) = (map₂ f xs ys).snoc (f x y)

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × φ
x : α
y : β
⊢ mapAccumr₂ f (xs.snoc x) (ys.snoc y) s =
    let q := f x y s;
    let r := mapAccumr₂ f xs ys q.1;
    (r.1, r.2.snoc q.2)

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n : ℕ
b : β
v : Vector α n
f : α → β
⊢ b ∈ (map f v).toList ↔ ∃ a, a ∈ v.toList ∧ f a = b

Tactic:
by
  rw [Vector.toList_map, List.mem_map]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
⊢ (List.zipWith f ↑x ↑y).length = n

Tactic:
by simp

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

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr f₁ nil s₁).1 (mapAccumr f₂ nil s₂).1 ∧ (mapAccumr f₁ nil s₁).2 = (mapAccumr f₂ nil s₂).2

pp: case snoc
α : Type u_1
β : Type u_2
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2
n✝ : ℕ
xs✝ : Vector α n✝
x✝ : α
a✝ :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ → R (mapAccumr f₁ xs✝ s₁).1 (mapAccumr f₂ xs✝ s₂).1 ∧ (mapAccumr f₁ xs✝ s₁).2 = (mapAccumr f₂ xs✝ s₂).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr f₁ (xs✝.snoc x✝) s₁).1 (mapAccumr f₂ (xs✝.snoc x✝) s₂).1 ∧
    (mapAccumr f₁ (xs✝.snoc x✝) s₁).2 = (mapAccumr f₂ (xs✝.snoc x✝) s₂).2

Tactic:
next => exact ⟨h₀, rfl⟩

Goal state after:
case snoc
α : Type u_1
β : Type u_2
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2
n✝ : ℕ
xs✝ : Vector α n✝
x✝ : α
a✝ :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ → R (mapAccumr f₁ xs✝ s₁).1 (mapAccumr f₂ xs✝ s₂).1 ∧ (mapAccumr f₁ xs✝ s₁).2 = (mapAccumr f₂ xs✝ s₂).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr f₁ (xs✝.snoc x✝) s₁).1 (mapAccumr f₂ (xs✝.snoc x✝) s₂).1 ∧
    (mapAccumr f₁ (xs✝.snoc x✝) s₁).2 = (mapAccumr f₂ (xs✝.snoc x✝) s₂).2
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr₂ f₁ nil nil s₁).1 (mapAccumr₂ f₂ nil nil s₂).1 ∧
    (mapAccumr₂ f₁ nil nil s₁).2 = (mapAccumr₂ f₂ nil nil s₂).2

pp: case snoc
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ →
      R (mapAccumr₂ f₁ xs✝ ys✝ s₁).1 (mapAccumr₂ f₂ xs✝ ys✝ s₂).1 ∧
        (mapAccumr₂ f₁ xs✝ ys✝ s₁).2 = (mapAccumr₂ f₂ xs✝ ys✝ s₂).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr₂ f₁ (xs✝.snoc x✝) (ys✝.snoc y✝) s₁).1 (mapAccumr₂ f₂ (xs✝.snoc x✝) (ys✝.snoc y✝) s₂).1 ∧
    (mapAccumr₂ f₁ (xs✝.snoc x✝) (ys✝.snoc y✝) s₁).2 = (mapAccumr₂ f₂ (xs✝.snoc x✝) (ys✝.snoc y✝) s₂).2

Tactic:
next => exact ⟨h₀, rfl⟩

Goal state after:
case snoc
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ →
      R (mapAccumr₂ f₁ xs✝ ys✝ s₁).1 (mapAccumr₂ f₂ xs✝ ys✝ s₂).1 ∧
        (mapAccumr₂ f₁ xs✝ ys✝ s₁).2 = (mapAccumr₂ f₂ xs✝ ys✝ s₂).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr₂ f₁ (xs✝.snoc x✝) (ys✝.snoc y✝) s₁).1 (mapAccumr₂ f₂ (xs✝.snoc x✝) (ys✝.snoc y✝) s₂).1 ∧
    (mapAccumr₂ f₁ (xs✝.snoc x✝) (ys✝.snoc y✝) s₁).2 = (mapAccumr₂ f₂ (xs✝.snoc x✝) (ys✝.snoc y✝) s₂).2
Module: Mathlib.Data.W.Constructions

Goal state before:
pp: γ : Type u
x : γ
f : Listβ γ (Listα.cons x) → WType (Listβ γ)
⊢ ofList γ (toList γ (mk (Listα.cons x) f)) = mk (Listα.cons x) f

Tactic:
by
    simp only [toList, ofList, leftInverse_list (f PUnit.unit), mk.injEq, heq_eq_eq, true_and]
    rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n : ℕ
xs ys : Vector α n
f : α → α → β
comm : ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁
⊢ map₂ f xs ys = map₂ f ys xs

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
⊢ ∀ (a b x : α ⊕ β), x ∈ sumLift₂ Icc Icc a b ↔ a ≤ x ∧ x ≤ b

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
⊢ ∀ (a b x : α ⊕ β), x ∈ sumLift₂ Ico Ico a b ↔ a ≤ x ∧ x < b

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
⊢ ∀ (a b x : α ⊕ β), x ∈ sumLift₂ Ioc Ioc a b ↔ a < x ∧ x ≤ b

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
⊢ ∀ (a b x : α ⊕ β), x ∈ sumLift₂ Ioo Ioo a b ↔ a < x ∧ x < b

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : LocallyFiniteOrderBot β
⊢ ∀ (a x : α ⊕ β), x ∈ Sum.elim (fun x ↦ map Embedding.inl (Iic x)) (fun x ↦ map Embedding.inr (Iic x)) a ↔ x ≤ a

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : LocallyFiniteOrderBot β
⊢ ∀ (a x : α ⊕ β), x ∈ Sum.elim (fun x ↦ map Embedding.inl (Iio x)) (fun x ↦ map Embedding.inr (Iio x)) a ↔ x < a

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderTop β
⊢ ∀ (a x : α ⊕ β), x ∈ Sum.elim (fun x ↦ map Embedding.inl (Ici x)) (fun x ↦ map Embedding.inr (Ici x)) a ↔ a ≤ x

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderTop β
⊢ ∀ (a x : α ⊕ β), x ∈ Sum.elim (fun x ↦ map Embedding.inl (Ioi x)) (fun x ↦ map Embedding.inr (Ioi x)) a ↔ a < x

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
⊢ ∀ (a b x : α ⊕ₗ β),
    x ∈ map toLex.toEmbedding (sumLexLift Icc Icc (fun a x ↦ Ici a) (fun x ↦ Iic) (ofLex a) (ofLex b)) ↔ a ≤ x ∧ x ≤ b

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
⊢ ∀ (a b x : α ⊕ₗ β),
    x ∈ map toLex.toEmbedding (sumLexLift Ico Ico (fun a x ↦ Ici a) (fun x ↦ Iio) (ofLex a) (ofLex b)) ↔ a ≤ x ∧ x < b

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
⊢ ∀ (a b x : α ⊕ₗ β),
    x ∈ map toLex.toEmbedding (sumLexLift Ioc Ioc (fun a x ↦ Ioi a) (fun x ↦ Iic) (ofLex a) (ofLex b)) ↔ a < x ∧ x ≤ b

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
⊢ ∀ (a b x : α ⊕ₗ β),
    x ∈ map toLex.toEmbedding (sumLexLift Ioo Ioo (fun a x ↦ Ioi a) (fun x ↦ Iio) (ofLex a) (ofLex b)) ↔ a < x ∧ x < b

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : LocallyFiniteOrderBot β
⊢ ∀ (a x : α ⊕ₗ β),
    x ∈
        ((Sum.elim (fun x ↦ map (Embedding.inl.trans toLex.toEmbedding) (Iic x)) fun x ↦
              map toLex.toEmbedding (univ.disjSum (Iic x))) ∘
            ⇑ofLex)
          a ↔
      x ≤ a

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : LocallyFiniteOrderBot β
⊢ ∀ (a x : α ⊕ₗ β),
    x ∈
        ((Sum.elim (fun x ↦ map (Embedding.inl.trans toLex.toEmbedding) (Iio x)) fun x ↦
              map toLex.toEmbedding (univ.disjSum (Iio x))) ∘
            ⇑ofLex)
          a ↔
      x < a

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : Fintype β
inst✝ : LocallyFiniteOrderTop β
⊢ ∀ (a x : α ⊕ₗ β),
    x ∈
        ((Sum.elim (fun x ↦ map toLex.toEmbedding ((Ici x).disjSum univ)) fun x ↦
              map (Embedding.inr.trans toLex.toEmbedding) (Ici x)) ∘
            ⇑ofLex)
          a ↔
      a ≤ x

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : Fintype β
inst✝ : LocallyFiniteOrderTop β
⊢ ∀ (a x : α ⊕ₗ β),
    x ∈
        ((Sum.elim (fun x ↦ map toLex.toEmbedding ((Ioi x).disjSum univ)) fun x ↦
              map (Embedding.inr.trans toLex.toEmbedding) (Ioi x)) ∘
            ⇑ofLex)
          a ↔
      a < x

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.ZMod.Factorial

Goal state before:
pp: n p : ℕ
h : n ≤ p
x : ℕ
hx : x ∈ range n
⊢ -1 + -↑x = -1 * ↑x + -1 * 1

Tactic:
neg_mul,

Goal state after:
n p : ℕ
h : n ≤ p
x : ℕ
hx : x ∈ range n
⊢ -1 + -↑x = -(1 * ↑x) + -1 * 1
Module: Mathlib.Data.WSeq.Defs

Goal state before:
pp: α : Type u
s✝ : WSeq α
s1 s2 : Computation ℕ
l : List α
a : α
s : WSeq α
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, cons a s) ∧
    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, cons a s))
⊢ Computation.corec
      (fun x ↦
        match Seq.destruct x.2 with
        | none => Sum.inl x.1
        | some (none, s') => Sum.inr (x.1, s')
        | some (some val, s') => Sum.inr (x.1 + 1, s'))
      (l.length + 1, s) =
    Computation.corec
      (fun x ↦
        match Seq.destruct x.2 with
        | none => Sum.inl x.1
        | some (none, s') => Sum.inr (x.1, s')
        | some (some val, s') => Sum.inr (x.1 + 1, s'))
      ((a :: l).length, s)

Tactic:
by simp

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

Goal state before:
pp: α : Type u
s✝ : WSeq α
s1 s2 : Computation ℕ
l : List α
a : α
s : WSeq α
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, cons a s) ∧
    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, cons a s))
⊢ Computation.map List.length
      (Computation.corec
        (fun x ↦
          match Seq.destruct x.2 with
          | none => Sum.inl x.1.reverse
          | some (none, s') => Sum.inr (x.1, s')
          | some (some a, s') => Sum.inr (a :: x.1, s'))
        (a :: l, s)) =
    Computation.map List.length
      (Computation.corec
        (fun x ↦
          match Seq.destruct x.2 with
          | none => Sum.inl x.1.reverse
          | some (none, s') => Sum.inr (x.1, s')
          | some (some a, s') => Sum.inr (a :: x.1, s'))
        (a :: l, s))

Tactic:
by simp

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

Goal state before:
pp: α : Type u
s✝ : WSeq α
s1 s2 : Computation ℕ
l : List α
s : WSeq α
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, s.think) ∧
    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, s.think))
⊢ Computation.corec
      (fun x ↦
        match Seq.destruct x.2 with
        | none => Sum.inl x.1
        | some (none, s') => Sum.inr (x.1, s')
        | some (some val, s') => Sum.inr (x.1 + 1, s'))
      (l.length, s) =
    Computation.corec
      (fun x ↦
        match Seq.destruct x.2 with
        | none => Sum.inl x.1
        | some (none, s') => Sum.inr (x.1, s')
        | some (some val, s') => Sum.inr (x.1 + 1, s'))
      (l.length, s)

Tactic:
by simp

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

Goal state before:
pp: α : Type u
s✝ : WSeq α
s1 s2 : Computation ℕ
l : List α
s : WSeq α
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, s.think) ∧
    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, s.think))
⊢ Computation.map List.length
      (Computation.corec
        (fun x ↦
          match Seq.destruct x.2 with
          | none => Sum.inl x.1.reverse
          | some (none, s') => Sum.inr (x.1, s')
          | some (some a, s') => Sum.inr (a :: x.1, s'))
        (l, s)) =
    Computation.map List.length
      (Computation.corec
        (fun x ↦
          match Seq.destruct x.2 with
          | none => Sum.inl x.1.reverse
          | some (none, s') => Sum.inr (x.1, s')
          | some (some a, s') => Sum.inr (a :: x.1, s'))
        (l, s))

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → α
x✝² : Set α
x✝¹ : MeasurableSet x✝²
x✝ : f ⁻¹' x✝² = x✝²
⊢ EventuallyConst x✝² (ae 0)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → α
hf : Measurable f
⊢ Measure.map f 0 ≪ 0

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → α
hf : Measurable f
⊢ Measure.map f 0 = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.MeasureTheory.Group.AEStabilizer

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
⊢ 1 ∈ {g | g • s =ᵐ[μ] s}

Tactic:
by simp

Goal state after:
Module: Mathlib.MeasureTheory.Group.AEStabilizer

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝² : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x✝¹ : G
x✝ : x✝¹ ∈ ⊤
⊢ x✝¹ ∈ aestabilizer G μ ∅

Tactic:
by simp

Goal state after:
Module: Mathlib.MeasureTheory.Group.AEStabilizer

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝² : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x✝¹ : G
x✝ : x✝¹ ∈ ⊤
⊢ x✝¹ ∈ aestabilizer G μ univ

Tactic:
by simp

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

Goal state before:
pp: x : ℝ
n : ℤ
⊢ translate (Multiplicative.ofAdd x) ^ n = translate (Multiplicative.ofAdd (↑n * x))

Tactic:
simp only [← zsmul_eq_mul, ofAdd_zsmul, map_zpow]

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

Goal state before:
pp: f✝ g✝ f g : CircleDeg1Lift
x : ℝ
⊢ min (f (x + 1)) (g (x + 1)) = min (f x) (g x) + 1

Tactic:
simp [min_add_add_right]

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

Goal state before:
pp: f : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) < 1 / (2 * 2 ^ n)

Tactic:
← pow_succ',

Goal state after:
f : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) < 1 / 2 ^ (n + 1)
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: ⊢ Tendsto (fun n ↦ (⇑1)^[n] 0 / ↑n) atTop (𝓝 0)

Tactic:
by simp

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

Goal state before:
pp: f : CircleDeg1Lift
⊢ τ (f ^ 0) = ↑0 * τ f

Tactic:
by simp

Goal state after:
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
⊢ ε / 3 + ε / 3 + ε / 3 = ε

Tactic:
by simp

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x ↦ g * x) μ
a : G
h : (range fun x ↦ g ^ x)ᶜ ∈ 𝓝 a
⊢ (match 1 with
    | (x, y) => a * x / y) =
    a

Tactic:
by simp

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

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
f : X → X
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμ : Ergodic f μ
hfν : MeasurePreserving f ν ν
hνμ : ν ≪ μ
this : ν.rnDeriv μ ∘ f =ᵐ[μ] ν.rnDeriv μ
c : ℝ≥0∞
hc : ν.rnDeriv μ =ᵐ[μ] const X c
s : Set X
hs : MeasurableSet s
⊢ ∫⁻ (x : X) in s, c ∂μ = (c • μ) s

Tactic:
by simp

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

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
f : X → X
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
hμ : Ergodic f μ
hfν : MeasurePreserving f ν ν
hνμ : ν ≪ μ
⊢ ν univ = μ univ

Tactic:
by simp

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 ?_

Goal state after:
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 : α) ∂ν, μ.rnDeriv ν x < ∞
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
G : Type u_2
inst✝¹ : TopologicalSpace A
inst✝ : DiscreteTopology A
U : Finset G
x : G → A
⊢ ∀ a ∈ ↑U, IsOpen[inst✝¹] {x a}

Tactic:
by simp

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

Goal state before:
pp: A : Type u_1
G : Type u_2
inst✝¹ : TopologicalSpace A
inst✝ : T1Space A
U : Finset G
x : G → A
⊢ ∀ a ∈ ↑U, IsClosed[inst✝¹] {x a}

Tactic:
by simp

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

Goal state before:
pp: A : Type u_3
G : Type u_4
inst✝¹ : Inhabited A
inst✝ : Monoid G
F : Set (Pattern A G)
h : G
⊢ MapsTo (mulShift h) (mulForbidden F) (mulForbidden F)

Tactic:
by
  -- unfold `MapsTo`
  intro x hx p hp g
  specialize hx p hp (h * g)
  contrapose! hx
  simpa [mulOccursInAt_mulShift] using hx

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✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ν.restrict s, f x < ∞

Tactic:
refine ae_restrict_of_ae ?_

Goal state after:
case refine_2
α : 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 ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ν, f x < ∞