mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
⊢ IsPrecongr r'

Tactic:
intro a

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a : (P F).M α
⊢ ∀ ⦃y : (P F).M α⦄,
    r' a y →
      MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) a) =
        MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) y)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
x : Fix F
⊢ mk x.dest = x

Tactic:
by
  change (Fix.mk ∘ Fix.dest) x = id x
  apply Fix.ind_rec (mk ∘ dest) id
  intro x
  rw [Function.comp_apply, id_eq, Fix.dest, Fix.rec_eq, id_map, comp_map]
  intro h
  rw [h]

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

Goal state before:
pp: F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
x✝ : Cofix F
x : (P F).M
y✝ : Cofix F
y : (P F).M
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M → (P F).M → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
⊢ IsPrecongr r'

Tactic:
intro a

Goal state after:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
x✝ : Cofix F
x : (P F).M
y✝ : Cofix F
y : (P F).M
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M → (P F).M → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a : (P F).M
⊢ ∀ ⦃y : (P F).M⦄, r' a y → abs ((P F).map (Quot.mk r') a.dest) = abs ((P F).map (Quot.mk r') y.dest)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α✝ α : TypeVec.{u} n
⊢ ∀ (a : (P F).W α), Quot.mk WEquiv (fixToW (Quot.mk (⇑(wSetoid α)) a)) = Quot.mk (⇑(wSetoid α)) a

Tactic:
intro a

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α✝ α : TypeVec.{u} n
a : (P F).W α
⊢ Quot.mk WEquiv (fixToW (Quot.mk (⇑(wSetoid α)) a)) = Quot.mk (⇑(wSetoid α)) a
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := ⋯
x y : Cofix F
rxy : r x y
⊢ ∀ (x y : Cofix F), r' x y → Quot.mk r' <$> x.dest = Quot.mk r' <$> y.dest

Tactic:
intro x y r'xy
    rcases r'xy with r'xy | r'xy
    · rw [r'xy]
    have : ∀ x y, r x y → r' x y := fun x y h => Or.inr h
    rw [← Quot.factor_mk_eq _ _ this]
    dsimp [r']
    rw [@comp_map _ q _ _ _ (Quot.mk r), @comp_map _ q _ _ _ (Quot.mk r)]
    rw [h _ _ r'xy]

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
X Y : Type u
x₀ : X
f : X → Y
g : Y → F (α ::: X)
R : Cofix F α → Cofix F α → Prop :=
  fun a b ↦ ∃ x, a = Cofix.corec (g ∘ f) x ∧ b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
a b : Cofix F α
x : X
Ha : a = Cofix.corec (g ∘ f) x
Hb : b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
⊢ ∀ (x : X), R (Cofix.corec (g ∘ f) x) ((Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) ∘ f) x)

Tactic:
intro a

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
X Y : Type u
x₀ : X
f : X → Y
g : Y → F (α ::: X)
R : Cofix F α → Cofix F α → Prop :=
  fun a b ↦ ∃ x, a = Cofix.corec (g ∘ f) x ∧ b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
a✝ b : Cofix F α
x : X
Ha : a✝ = Cofix.corec (g ∘ f) x
Hb : b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
a : X
⊢ R (Cofix.corec (g ∘ f) a) ((Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) ∘ f) a)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
u : α
⊢ (∀ (a_1 : (P F).A) (f_1 : (P F).B a_1 → α), abs ⟨a_1, f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 '' univ) → u ∈ f '' univ

Tactic:
intro h'
    apply h' _ _ rfl

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

Goal state before:
pp: α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
⊢ ∀ (a : α) {l : List (Computation α)} {S : WSeq (Computation α)}, pure a ∈ l → (corec parallel.aux1 (l, S)).Terminates

Tactic:
intro a

Goal state after:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
a : α
⊢ ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, pure a ∈ l → (corec parallel.aux1 (l, S)).Terminates
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
⊢ ∀ (a : α) {l : List (Computation α)} {S : WSeq (Computation α)}, pure a ∈ l → (corec parallel.aux1 (l, S)).Terminates

Tactic:
intro a l S m

Goal state after:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
a : α
l : List (Computation α)
S : WSeq (Computation α)
m : pure a ∈ l
⊢ (corec parallel.aux1 (l, S)).Terminates
Module: Mathlib.Data.Set.Enumerate

Goal state before:
pp: case some.zero
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
h : enumerate sel s (n + 1) = none
val✝ : α
hs : sel s = some val✝
hm : n + 1 ≤ 0
⊢ enumerate sel s 0 = none

Tactic:
| zero =>

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

Goal state before:
pp: case zero.zero
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s 0 = some a
h₂ : enumerate sel s (0 + 0) = some a
⊢ 0 = 0 + 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m : ℕ
s : Set α
h₁ : enumerate sel s 0 = some a
h₂ : enumerate sel s (0 + m) = some a
⊢ 0 = 0 + m

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u
a : α
s : WSeq α
⊢ (cons a s).drop (0 + 1) = s.drop 0

Tactic:
| zero =>

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

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

Tactic:
| zero =>

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
⊢ ⋃ n, ∅ = s

Tactic:
simp [Set.not_nonempty_iff_eq_empty'.mp h]

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
c1✝ : Computation (WSeq α)
c2✝ : Computation (WSeq β)
h✝¹ : Computation.LiftRel (LiftRel R) c1✝ c2✝
S : WSeq α → WSeq β → Prop := ⋯
s : WSeq α
t : WSeq β
h✝ : S s t
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h : Computation.LiftRel (LiftRel R) c1 c2
⊢ ∀ {a : WSeq α} {b : WSeq β}, LiftRel R a b → Computation.LiftRel (LiftRelO R S) a.destruct b.destruct

Tactic:
intro a

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
c1✝ : Computation (WSeq α)
c2✝ : Computation (WSeq β)
h✝¹ : Computation.LiftRel (LiftRel R) c1✝ c2✝
S : WSeq α → WSeq β → Prop := fun s t ↦ ∃ c1 c2, s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2
s : WSeq α
t : WSeq β
h✝ : S s t
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h : Computation.LiftRel (LiftRel R) c1 c2
a : WSeq α
⊢ ∀ {b : WSeq β}, LiftRel R a b → Computation.LiftRel (LiftRelO R S) a.destruct b.destruct
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
c1✝ : Computation (WSeq α)
c2✝ : Computation (WSeq β)
h✝¹ : Computation.LiftRel (LiftRel R) c1✝ c2✝
S : WSeq α → WSeq β → Prop := ⋯
s : WSeq α
t : WSeq β
h✝ : S s t
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h : Computation.LiftRel (LiftRel R) c1 c2
a : WSeq α
b : WSeq β
ab : LiftRel R a b
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)}, LiftRelO R (LiftRel R) a b → LiftRelO R S a b

Tactic:
intro a

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
c1✝ : Computation (WSeq α)
c2✝ : Computation (WSeq β)
h✝¹ : Computation.LiftRel (LiftRel R) c1✝ c2✝
S : WSeq α → WSeq β → Prop := fun s t ↦ ∃ c1 c2, s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2
s : WSeq α
t : WSeq β
h✝ : S s t
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h : Computation.LiftRel (LiftRel R) c1 c2
a✝ : WSeq α
b : WSeq β
ab : LiftRel R a✝ b
a : Option (α × WSeq α)
⊢ ∀ {b : Option (β × WSeq β)}, LiftRelO R (LiftRel R) a b → LiftRelO R S a b
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ ∀ {a b : Option (α × WSeq α)},
    BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b →
      Computation.LiftRel Equiv ((Computation.pure ∘ fun o ↦ Option.rec nil Prod.snd o) a)
        ((Computation.pure ∘ fun o ↦ Option.rec nil Prod.snd o) b)

Tactic:
intro a

Goal state after:
α : Type u
s t : WSeq α
h : s ~ʷ t
a : Option (α × WSeq α)
⊢ ∀ {b : Option (α × WSeq α)},
    BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b →
      Computation.LiftRel Equiv ((Computation.pure ∘ fun o ↦ Option.rec nil Prod.snd o) a)
        ((Computation.pure ∘ fun o ↦ Option.rec nil Prod.snd o) b)
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case refine_2
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
⊢ ∀ {a b : Option (α × WSeq α)},
    a ∈ s.destruct → b ∈ t.destruct → LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) a b

Tactic:
intro a

Goal state after:
case refine_2
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
a : Option (α × WSeq α)
⊢ ∀ {b : Option (α × WSeq α)},
    a ∈ s.destruct → b ∈ t.destruct → LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) a b
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
⊢ F [] (Sum.inr [])

Tactic:
intro a

Goal state after:
α : Type u
S : WSeq (Computation α)
a✝ : α
h : a✝ ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
a : α
⊢ (∃ c ∈ [], a ∈ c) → ∃ c ∈ [], a ∈ c
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : 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✝
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      LiftRelO R (fun s t ↦ LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) a b

Tactic:
intro a

Goal state after:
α : 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✝
s : WSeq α
t : WSeq β
h : LiftRel R s t
a : Option (α × WSeq α)
⊢ ∀ {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      LiftRelO R (fun s t ↦ LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) a b
Module: Mathlib.Data.Setoid.Partition.Card

Goal state before:
pp: α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
f : ↑(Function.support fun t ↦ (s ∩ ↑t).ncard) → ↑s :=
  fun x ↦
    match x with
    | ⟨t, ht⟩ => ⟨Exists.choose ⋯, ⋯⟩
hf : ∀ (t : ↑(Function.support fun t ↦ (s ∩ ↑t).ncard)), ↑↑t ∈ P ∧ ↑(f t) ∈ ↑↑t
this : Finite ↑s
t t' : ↑(Function.support fun t ↦ (s ∩ ↑t).ncard)
h : f t = f t'
⊢ t = t'

Tactic:
simp only [← Subtype.coe_inj]

Goal state after:
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
f : ↑(Function.support fun t ↦ (s ∩ ↑t).ncard) → ↑s :=
  fun x ↦
    match x with
    | ⟨t, ht⟩ => ⟨Exists.choose ⋯, ⋯⟩
hf : ∀ (t : ↑(Function.support fun t ↦ (s ∩ ↑t).ncard)), ↑↑t ∈ P ∧ ↑(f t) ∈ ↑↑t
this : Finite ↑s
t t' : ↑(Function.support fun t ↦ (s ∩ ↑t).ncard)
h : f t = f t'
⊢ ↑↑t = ↑↑t'
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: case refine_1.right.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i✝ : ι
b a : α i✝
hba : b ≤ a
hab : a < b
⊢ False

Tactic:
· exact hab.not_ge hba

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

Goal state before:
pp: α : 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
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      LiftRelO R (fun s t ↦ LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x) a b

Tactic:
intro a

Goal state after:
α : 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
a : Option (α × WSeq α)
⊢ ∀ {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      LiftRelO R (fun s t ↦ LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x) a b
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]
        apply Computation.LiftRel.imp _ _ _ (liftRel_destruct h2)
        intro a b
        apply LiftRelO.imp_right
        intro s t
        apply Or.inl

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

Goal state before:
pp: case zero
α : Type u_1
n : ℕ
val : α
⊢ replicate (0 + 1) val = (replicate 0 val).snoc val

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u_1
n : ℕ
a : α
v : Vector α 0
ha : a ∈ v.tail.toList
⊢ a ∈ v.toList

Tactic:
| zero =>

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

Goal state before:
pp: a : ℤ
p : ℕ
pp : Fact (Nat.Prime p)
⊢ ↑a = 0 ↔ a.gcd ↑p ≠ 1

Tactic:
by
  rw [Ne, Int.gcd_comm, ← Int.isCoprime_iff_gcd_eq_one,
    (Nat.prime_iff_prime_int.1 pp.1).coprime_iff_not_dvd, Classical.not_not,
    intCast_zmod_eq_zero_iff_dvd]

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

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

Tactic:
simpa [hs] using hf.measure_self_or_compl_eq_zero hs hs'

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
e : α ≃ᵐ α
he : Ergodic (⇑e) μ
s : Set α
hsm : MeasurableSet s
hs : ⇑e.symm ⁻¹' s = s
| ⇑e ⁻¹' s

Tactic:
← hs,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
e : α ≃ᵐ α
he : Ergodic (⇑e) μ
s : Set α
hsm : MeasurableSet s
hs : ⇑e.symm ⁻¹' s = s
| ⇑e ⁻¹' ⇑e.symm ⁻¹' s
Module: Mathlib.Dynamics.FixedPoints.Prufer

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
g' : G
hg' : g' ^ n ^ j = 1
y : G
hy : y ∈ (fun x ↦ x ^ n)^[j] ⁻¹' s
⊢ (fun x ↦ g' • x) y ∈ (fun x ↦ x ^ n)^[j] ⁻¹' s

Tactic:
change (zpowGroupHom n)^[j] (g' * y) ∈ s

Goal state after:
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
g' : G
hg' : g' ^ n ^ j = 1
y : G
hy : y ∈ (fun x ↦ x ^ n)^[j] ⁻¹' s
⊢ (⇑(zpowGroupHom n))^[j] (g' * y) ∈ s
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C
⊢ ℕ → ℝ

pp: f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C
⊢ ∀ (t : ℕ), dist (f.transnumAuxSeq t) (x (2 ^ t) / 2 ^ t) ≤ ?m.45 t

pp: f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C
⊢ Tendsto ?m.45 atTop (𝓝 0)

Tactic:
· exact fun n => C / 2 ^ n

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

f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C
⊢ Tendsto (fun n ↦ C / 2 ^ n) atTop (𝓝 0)
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) μ
⊢ DenseRange fun x ↦ g ^ x

Tactic:
intro a

Goal state after:
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
⊢ a ∈ closure[inst✝⁴] (range fun x ↦ g ^ x)
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
this :
  Tendsto
    (fun x ↦
      match x with
      | (x, y) => a * x / y)
    (𝓝 1.1 ×ˢ 𝓝 1.2) (𝓝 a)
⊢ ∃ V, 1 ∈ V ∧ IsOpen[inst✝⁴] V ∧ ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y

Tactic:
simpa [(nhds_basis_opens (1 : G)).prod_self.mem_iff, prod_subset_iff, and_assoc] using this h

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: case inr.mpr
a b : ℝ
hb : b ≠ 0
h : ¬Dense ↑(AddSubgroup.closure {a, b})
c : ℝ
hc : AddSubgroup.closure {a, b} = AddSubgroup.closure {c}
⊢ ¬Irrational (a / b)

Tactic:
have : {a, b} ⊆ range (· • c : ℤ → ℝ) := by
      rw [← AddSubgroup.coe_zmultiples, AddSubgroup.zmultiples_eq_closure, ← hc]
      apply AddSubgroup.subset_closure

Goal state after:
case inr.mpr
a b : ℝ
hb : b ≠ 0
h : ¬Dense ↑(AddSubgroup.closure {a, b})
c : ℝ
hc : AddSubgroup.closure {a, b} = AddSubgroup.closure {c}
this : {a, b} ⊆ range fun x ↦ x • c
⊢ ¬Irrational (a / b)
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: case succ.refine_2
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : μ s ≠ 0
x : α
left✝ : x ∈ s
hx : {n | f^[n] x ∈ s}.Infinite
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD n.succ]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
⊢ f^[l - k + k] x ∈ s

Tactic:
tsub_add_cancel_of_le

Goal state after:
case succ.refine_2
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : μ s ≠ 0
x : α
left✝ : x ∈ s
hx : {n | f^[n] x ∈ s}.Infinite
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD n.succ]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
⊢ f^[l] x ∈ s

case succ.refine_2
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : μ s ≠ 0
x : α
left✝ : x ∈ s
hx : {n | f^[n] x ∈ s}.Infinite
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD n.succ]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
⊢ k ≤ l
Module: Mathlib.Topology.Order.CountableSeparating

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s : Set X
t : Set (Set X)
htc : t.Countable
ht_sub : ∀ s ∈ t, s ∈ range Ioi
ht : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ t, x ∈ s ↔ y ∈ s) → x = y
⊢ ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ compl '' t, x ∈ s ↔ y ∈ s) → x = y

Tactic:
by simpa [not_iff_not]

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

Goal state before:
pp: case zero
X : Type u_1
T : X → X
U : SetRel X X
inst✝ : UniformSpace X
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
⊢ ⋂ k, (map T T)^[↑k] ⁻¹' U ∈ 𝓤 X

Tactic:
| zero =>

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

Goal state before:
pp: case mp
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : ⨆ x, ↑(↑x).card = ⊤
k : ℕ
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card

Tactic:
iSup_eq_top

Goal state after:
case mp
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : ∀ b < ⊤, ∃ i, b < ↑(↑i).card
k : ℕ
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
x : ↑G
⊢ G.domRestrict φ (MapsTo.restrict S G G hG x) = T (G.domRestrict φ x)

Tactic:
rw [G.domRestrict_apply, G.domRestrict_apply, hG.val_restrict_apply, h.eq x]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
⊢ Semiconj (G.domRestrict φ) (MapsTo.restrict S G G hG) T

Tactic:
intro a

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
a : ↑G
⊢ G.domRestrict φ (MapsTo.restrict S G G hG a) = T (G.domRestrict φ a)