mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
S✝ : WSeq (WSeq α)
T✝ : WSeq (WSeq β)
h✝ : LiftRel (LiftRel R) S✝ T✝
s1 : WSeq α
s2 : WSeq β
x✝¹ :
  (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2
s : WSeq α
t : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1 : s1 = s.append S.join
h2 : s2 = t.append T.join
st : LiftRel R s t
ST : LiftRel (LiftRel R) S T
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
x✝ : LiftRelO R (LiftRel R) none none
⊢ (∀ {a : Option (α × WSeq α)},
      a ∈ S.join.destruct →
        ∃ b ∈ T.join.destruct,
          LiftRelO R
            (fun s1 s2 ↦
              ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T)
            a b) ∧
    ∀ {b : Option (β × WSeq β)},
      b ∈ T.join.destruct →
        ∃ a ∈ S.join.destruct,
          LiftRelO R
            (fun s1 s2 ↦
              ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T)
            a b

Tactic:
;

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
S✝ : WSeq (WSeq α)
T✝ : WSeq (WSeq β)
h✝ : LiftRel (LiftRel R) S✝ T✝
s1 : WSeq α
s2 : WSeq β
x✝¹ :
  (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2
s : WSeq α
t : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1 : s1 = s.append S.join
h2 : s2 = t.append T.join
st : LiftRel R s t
ST : LiftRel (LiftRel R) S T
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
x✝ : LiftRelO R (LiftRel R) none none
⊢ (∀ {a : Option (α × WSeq α)},
      a ∈ S.join.destruct →
        ∃ b ∈ T.join.destruct,
          LiftRelO R
            (fun s1 s2 ↦
              ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T)
            a b) ∧
    ∀ {b : Option (β × WSeq β)},
      b ∈ T.join.destruct →
        ∃ a ∈ S.join.destruct,
          LiftRelO R
            (fun s1 s2 ↦
              ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T)
            a b
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
s1 s2 : WSeq α
f1 f2 : α → WSeq β
h1 : s1 ~ʷ s2
h2 : ∀ (a : α), f1 a ~ʷ f2 a
a b : α
h : a = b
⊢ LiftRel Eq (f1 b) (f2 b)

Tactic:
;

Goal state after:
α : Type u
β : Type v
s1 s2 : WSeq α
f1 f2 : α → WSeq β
h1 : s1 ~ʷ s2
h2 : ∀ (a : α), f1 a ~ʷ f2 a
a b : α
h : a = b
⊢ LiftRel Eq (f1 b) (f2 b)
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
s✝ s' s : WSeq α
h : (map ret s).join = s'
⊢ Computation.LiftRel (LiftRelO Eq fun s1 s2 ↦ (map ret s2).join = s1) s'.destruct s.destruct

Tactic:
;

Goal state after:
α : Type u
s✝ s' s : WSeq α
h : (map ret s).join = s'
⊢ Computation.LiftRel (LiftRelO Eq fun s1 s2 ↦ (map ret s2).join = s1) s'.destruct s.destruct
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case Hc
α : Type u
s✝ s' s : WSeq α
h : (map ret s).join = s'
⊢ ∃ s_1, (map ret s).join.destruct = (map ret s_1).join.destruct ∧ s.destruct = s_1.destruct

Tactic:
exact ⟨s, rfl, rfl⟩

Goal state after:
Module: Mathlib.Data.Sym.NatCard

Goal state before:
pp: case inl
α : Type u_1
k : ℕ
h✝ : Finite α
val✝ : Fintype α
⊢ Nat.card (Sym α k) = (Nat.card α).multichoose k

Tactic:
;

Goal state after:
case inl
α : Type u_1
k : ℕ
h✝ : Finite α
val✝ : Fintype α
⊢ Nat.card (Sym α k) = (Nat.card α).multichoose k
Module: Mathlib.Data.Sym.NatCard

Goal state before:
pp: case inl
α : Type u_1
h✝ : Finite α
val✝ : Fintype α
⊢ Nat.card { a // ¬a.IsDiag } = (Nat.card α).choose 2

Tactic:
;

Goal state after:
case inl
α : Type u_1
h✝ : Finite α
val✝ : Fintype α
⊢ Nat.card { a // ¬a.IsDiag } = (Nat.card α).choose 2
Module: Mathlib.Data.Sym.NatCard

Goal state before:
pp: case inl
α : Type u_1
h✝ : Finite α
val✝ : Fintype α
⊢ Nat.card (Sym2 α) = (Nat.card α + 1).choose 2

Tactic:
;

Goal state after:
case inl
α : Type u_1
h✝ : Finite α
val✝ : Fintype α
⊢ Nat.card (Sym2 α) = (Nat.card α + 1).choose 2
Module: Mathlib.Data.Sym.Sym2.Finsupp

Goal state before:
pp: case mk
α : Type u_1
M₀ : Type u_2
inst✝¹ : CommMonoidWithZero M₀
inst✝ : NoZeroDivisors M₀
f : α →₀ M₀
x✝ : Sym2 α
a b : α
⊢ Quot.mk (Rel α) (a, b) ∈ ↑f.support.sym2 ↔ Quot.mk (Rel α) (a, b) ∈ map ⇑f ⁻¹' Function.support mul

Tactic:
;

Goal state after:
case mk
α : Type u_1
M₀ : Type u_2
inst✝¹ : CommMonoidWithZero M₀
inst✝ : NoZeroDivisors M₀
f : α →₀ M₀
x✝ : Sym2 α
a b : α
⊢ Quot.mk (Rel α) (a, b) ∈ ↑f.support.sym2 ↔ Quot.mk (Rel α) (a, b) ∈ map ⇑f ⁻¹' Function.support mul
Module: Mathlib.Data.Tree.Traversable

Goal state before:
pp: case nil
α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
⊢ pure nil = Functor.Comp.mk (pure (pure nil))

Tactic:
;

Goal state after:
case nil
α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
⊢ pure nil = Functor.Comp.mk (pure (pure nil))
Module: Mathlib.Data.Vector.Snoc

Goal state before:
pp: α : Type u_1
n✝ : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = (replicate n val).snoc val
| (replicate (n + 1) val).snoc val

Tactic:
;

Goal state after:
α : Type u_1
n✝ : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = (replicate n val).snoc val
| (replicate (n + 1) val).snoc val
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case refine_1
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁
b : β₁
h : sumLexLift f₁ f₂ g₁ g₂ (inl a) (inl b) = ∅
⊢ f₁ a b = ∅

Tactic:
;

Goal state after:
case refine_1
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁
b : β₁
h : sumLexLift f₁ f₂ g₁ g₂ (inl a) (inl b) = ∅
⊢ f₁ a b = ∅
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case refine_2
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁
b : β₂
h : sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b) = ∅
⊢ g₁ a b = ∅ ∧ g₂ a b = ∅

Tactic:
;

Goal state after:
case refine_2
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁
b : β₂
h : sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b) = ∅
⊢ g₁ a b = ∅ ∧ g₂ a b = ∅
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case refine_3
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₂
b : β₂
h : sumLexLift f₁ f₂ g₁ g₂ (inr a) (inr b) = ∅
⊢ f₂ a b = ∅

Tactic:
;

Goal state after:
case refine_3
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₂
b : β₂
h : sumLexLift f₁ f₂ g₁ g₂ (inr a) (inr b) = ∅
⊢ f₂ a b = ∅
Module: Mathlib.Data.Vector3

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

Tactic:
;

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

Goal state before:
pp: α : Type u_1
m n : ℕ
C : Vector3 α (n + 1) → Sort u
H : (a : α) → (t : Vector3 α n) → C (a :: t)
v : Vector3 α (n + 1)
⊢ C (v.head :: v.tail)

Tactic:
;

Goal state after:
α : Type u_1
m n : ℕ
C : Vector3 α (n + 1) → Sort u
H : (a : α) → (t : Vector3 α n) → C (a :: t)
v : Vector3 α (n + 1)
⊢ C (v.head :: v.tail)
Module: Mathlib.Data.Vector3

Goal state before:
pp: α : Type u_1
f : Vector3 α 0 → Prop
x✝ : Exists f
v : Vector3 α 0
fv : f v
⊢ f v

Tactic:
;

Goal state after:
α : Type u_1
f : Vector3 α 0 → Prop
x✝ : Exists f
v : Vector3 α 0
fv : f v
⊢ f v
Module: Mathlib.Data.Vector3

Goal state before:
pp: α : Type u_1
n : ℕ
f : Vector3 α n.succ → Prop
x✝ : Exists f
v : Vector3 α n.succ
fv : f v
⊢ f v

Tactic:
;

Goal state after:
α : Type u_1
n : ℕ
f : Vector3 α n.succ → Prop
x✝ : Exists f
v : Vector3 α n.succ
fv : f v
⊢ f v
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₁ a₂ : α
⊢ Icc (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Icc a₁ a₂))

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
a₁ a₂ : α
⊢ Icc (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Icc a₁ a₂))
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₁ a₂ : α
⊢ Icc (inlₗ a₁) (inlₗ a₂) = map (Embedding.inl.trans toLex.toEmbedding) (Icc a₁ a₂)

Tactic:
rw [← Finset.map_map]; rfl

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₁ a₂ : α
⊢ Ico (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Ico a₁ a₂))

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
a₁ a₂ : α
⊢ Ico (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Ico a₁ a₂))
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₁ a₂ : α
⊢ Ico (inlₗ a₁) (inlₗ a₂) = map (Embedding.inl.trans toLex.toEmbedding) (Ico a₁ a₂)

Tactic:
rw [← Finset.map_map]; rfl

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₁ a₂ : α
⊢ Ioc (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Ioc a₁ a₂))

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
a₁ a₂ : α
⊢ Ioc (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Ioc a₁ a₂))
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₁ a₂ : α
⊢ Ioc (inlₗ a₁) (inlₗ a₂) = map (Embedding.inl.trans toLex.toEmbedding) (Ioc a₁ a₂)

Tactic:
rw [← Finset.map_map]; rfl

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₁ a₂ : α
⊢ Ioo (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Ioo a₁ a₂))

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
a₁ a₂ : α
⊢ Ioo (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Ioo a₁ a₂))
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₁ a₂ : α
⊢ Ioo (inlₗ a₁) (inlₗ a₂) = map (Embedding.inl.trans toLex.toEmbedding) (Ioo a₁ a₂)

Tactic:
rw [← Finset.map_map]; rfl

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 β
b₁ b₂ : β
⊢ Icc (inrₗ b₁) (inrₗ b₂) = map toLex.toEmbedding (map Embedding.inr (Icc b₁ b₂))

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
b₁ b₂ : β
⊢ Icc (inrₗ b₁) (inrₗ b₂) = map toLex.toEmbedding (map Embedding.inr (Icc b₁ b₂))
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 β
b₁ b₂ : β
⊢ Icc (inrₗ b₁) (inrₗ b₂) = map (Embedding.inr.trans toLex.toEmbedding) (Icc b₁ b₂)

Tactic:
rw [← Finset.map_map]; rfl

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

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

Tactic:
;

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

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

Tactic:
;

Goal state after:
α : Type u
s : WSeq α
inst✝ : s.Productive
n m : ℕ
⊢ (s.get? (n + m)).Terminates
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 β
b₁ b₂ : β
⊢ Ico (inrₗ b₁) (inrₗ b₂) = map toLex.toEmbedding (map Embedding.inr (Ico b₁ b₂))

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
b₁ b₂ : β
⊢ Ico (inrₗ b₁) (inrₗ b₂) = map toLex.toEmbedding (map Embedding.inr (Ico b₁ b₂))
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 β
b₁ b₂ : β
⊢ Ico (inrₗ b₁) (inrₗ b₂) = map (Embedding.inr.trans toLex.toEmbedding) (Ico b₁ b₂)

Tactic:
rw [← Finset.map_map]; rfl

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

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ (Computation.pure (s.get? n)).Terminates

Tactic:
;

Goal state after:
α : Type u
s : Seq α
n : ℕ
⊢ (Computation.pure (s.get? n)).Terminates
Module: Mathlib.Data.WSeq.Productive

Goal state before:
pp: α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ (∀ (n : ℕ), (s.get? n).Terminates) ↔ ∀ (n : ℕ), (t.get? n).Terminates

Tactic:
;

Goal state after:
α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ (∀ (n : ℕ), (s.get? n).Terminates) ↔ ∀ (n : ℕ), (t.get? n).Terminates
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 β
b₁ b₂ : β
⊢ Ioc (inrₗ b₁) (inrₗ b₂) = map toLex.toEmbedding (map Embedding.inr (Ioc b₁ b₂))

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
b₁ b₂ : β
⊢ Ioc (inrₗ b₁) (inrₗ b₂) = map toLex.toEmbedding (map Embedding.inr (Ioc b₁ b₂))
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 β
b₁ b₂ : β
⊢ Ioc (inrₗ b₁) (inrₗ b₂) = map (Embedding.inr.trans toLex.toEmbedding) (Ioc b₁ b₂)

Tactic:
rw [← Finset.map_map]; rfl

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

Goal state before:
pp: α : Type u
s : Seq α
⊢ ↑(↑s).toSeq = ↑s

Tactic:
;

Goal state after:
α : Type u
s : Seq α
⊢ ↑(↑s).toSeq = ↑s
Module: Mathlib.Data.WSeq.Productive

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ ((↑s).get? n).get = s.get? n

Tactic:
;

Goal state after:
α : Type u
s : Seq α
n : ℕ
⊢ ((↑s).get? n).get = s.get? n
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 β
b₁ b₂ : β
⊢ Ioo (inrₗ b₁) (inrₗ b₂) = map toLex.toEmbedding (map Embedding.inr (Ioo b₁ b₂))

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
b₁ b₂ : β
⊢ Ioo (inrₗ b₁) (inrₗ b₂) = map toLex.toEmbedding (map Embedding.inr (Ioo b₁ b₂))
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 β
b₁ b₂ : β
⊢ Ioo (inrₗ b₁) (inrₗ b₂) = map (Embedding.inr.trans toLex.toEmbedding) (Ioo b₁ b₂)

Tactic:
rw [← Finset.map_map]; rfl

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

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ s.get? n ∈ Computation.pure (s.get? n)

Tactic:
;

Goal state after:
α : Type u
s : Seq α
n : ℕ
⊢ s.get? n ∈ Computation.pure (s.get? n)
Module: Mathlib.Dynamics.Ergodic.Ergodic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : PreErgodic f μ
hs : MeasurableSet s
hs' : f ⁻¹' s = s
⊢ μ s = 0 ∨ μ sᶜ = 0

Tactic:
simpa using hf.ae_empty_or_univ hs hs'

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

Goal state before:
pp: case bc
f g : CircleDeg1Lift
⊢ ↑⌈g 0⌉ < g 0 + 1

Tactic:
;

Goal state after:
case bc
f g : CircleDeg1Lift
⊢ ↑⌈g 0⌉ < g 0 + 1
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: case bc
f g : CircleDeg1Lift
⊢ g 0 - 1 < ↑⌊g 0⌋

Tactic:
;

Goal state after:
case bc
f g : CircleDeg1Lift
⊢ g 0 - 1 < ↑⌊g 0⌋
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: case h
f : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ dist ((f ^ 2 ^ n) 0 + (f ^ 2 ^ n) 0) ((f ^ 2 ^ n) ((f ^ 2 ^ n) 0)) < 1

Tactic:
;

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

Goal state before:
pp: f : CircleDeg1Liftˣ
n : ℕ
⊢ -((↑n + 1) * τ ↑f) = (-1 + -↑n) * τ ↑f

Tactic:
;

Goal state after:
f : CircleDeg1Liftˣ
n : ℕ
⊢ -((↑n + 1) * τ ↑f) = (-1 + -↑n) * τ ↑f
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: case hab
f g : CircleDeg1Lift
h : f ≤ g
n : ℕ
⊢ (f ^ n) 0 ≤ (g ^ n) 0

Tactic:
;

Goal state after:
case hab
f g : CircleDeg1Lift
h : f ≤ g
n : ℕ
⊢ (f ^ n) 0 ≤ (g ^ n) 0
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: case h₂
f : CircleDeg1Lift
x : ℝ
⊢ ↑⌊τ f⌋ ≤ τ f

Tactic:
;

Goal state after:
case h₂
f : CircleDeg1Lift
x : ℝ
⊢ ↑⌊τ f⌋ ≤ τ f
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: case inl
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : μ s = 0
⊢ μ s = 0 ∨ μ s = ENNReal.ofReal T

pp: case inr
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : μ s ≠ 0
⊢ μ s = 0 ∨ μ s = ENNReal.ofReal T

Tactic:
;

Goal state after:
case inl
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : μ s = 0
⊢ μ s = 0 ∨ μ s = ENNReal.ofReal T

case inr
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : μ s ≠ 0
⊢ μ s = 0 ∨ μ s = ENNReal.ofReal T
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᵐ[volume] B
⊢ 1 ≤ n

Tactic:
;

Goal state after:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᵐ[volume] B
⊢ 1 ≤ n
Module: Mathlib.Dynamics.Ergodic.AddCircleAdd

Goal state before:
pp: p : ℝ
inst✝ : Fact (0 < p)
a : AddCircle p
⊢ Ergodic (fun x ↦ x + a) volume ↔ addOrderOf a = 0

Tactic:
by
  simp only [add_comm, ← ergodic_add_left]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : μ s ≠ 0
t : ℕ → Set α := fun n ↦ s ∩ f^[n] ⁻¹' s
H : ¬{n | μ (s ∩ f^[n] ⁻¹' s) ≠ 0}.Infinite
⊢ ∃ N, μ (t N) ≠ 0 ∧ ∀ n > N, μ (t n) = 0

Tactic:
not_infinite

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : μ s ≠ 0
t : ℕ → Set α := fun n ↦ s ∩ f^[n] ⁻¹' s
H : {n | μ (s ∩ f^[n] ⁻¹' s) ≠ 0}.Finite
⊢ ∃ N, μ (t N) ≠ 0 ∧ ∀ n > N, μ (t n) = 0
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : μ s ≠ 0
t : ℕ → Set α := fun n ↦ s ∩ f^[n] ⁻¹' s
H : ¬∃ᶠ (m : ℕ) in atTop, μ (s ∩ f^[m] ⁻¹' s) ≠ 0
N : ℕ
hN : μ (t N) ≠ 0
hmax : ∀ n > N, μ (t n) = 0
⊢ False

Tactic:
have htm {n : ℕ} : NullMeasurableSet (t n) μ :=
    hs.inter <| hs.preimage <| hf.toQuasiMeasurePreserving.iterate n

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : μ s ≠ 0
t : ℕ → Set α := fun n ↦ s ∩ f^[n] ⁻¹' s
H : ¬∃ᶠ (m : ℕ) in atTop, μ (s ∩ f^[m] ⁻¹' s) ≠ 0
N : ℕ
hN : μ (t N) ≠ 0
hmax : ∀ n > N, μ (t n) = 0
htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ
⊢ False