mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h.left
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ abs ⟨a, fun i ↦ ↑(f i)⟩ = Subtype.val <$> abs (repr y)

Tactic:
h,

Goal state after:
case h.left
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ abs ⟨a, fun i ↦ ↑(f i)⟩ = Subtype.val <$> abs ⟨a, f⟩
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case left
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
h_balanceable : ?m.286
⊢ Valid' a₁
    (match Ordering.gt with
    | Ordering.lt => (erase x t_l).balanceR t_x t_r
    | Ordering.eq => t_l.glue t_r
    | Ordering.gt => t_l.balanceL t_x (erase x t_r))
    a₂

Tactic:
exact Valid'.balanceL h.left t_r_valid h_balanceable

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

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

Tactic:
h,

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

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

Tactic:
h,

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

Goal state before:
pp: case ind
F : Type u → Type v
q : QPF F
x y : (P F).W
a : (P F).A
f f' : (P F).B a → (P F).W
a✝ : ∀ (x : (P F).B a), Wequiv (f x) (f' x)
ih : ∀ (x : (P F).B a), Wequiv (f' x) (f x)
⊢ Wequiv (WType.mk a f') (WType.mk a f)

Tactic:
exact Wequiv.ind _ _ _ ih

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

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

Tactic:
have : ∀ x y, r x y → r' x y := fun x y h => Or.inr h

Goal state after:
case h.inr
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
r' : Cofix F α → Cofix F α → Prop := fun x y ↦ x = y ∨ r x y
x✝ y✝ : Cofix F α
rxy : r x✝ y✝
x y : Cofix F α
r'xy : r x y
this : ∀ (x y : Cofix F α), r x y → r' x y
⊢ (TypeVec.id ::: Quot.mk r') <$$> x.dest = (TypeVec.id ::: Quot.mk r') <$$> y.dest
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mk.mk
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)
⊢ Mcongr x y

Tactic:
let r' x y := r (Quot.mk _ x) (Quot.mk _ y)

Goal state after:
case mk.mk
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)
⊢ Mcongr x y
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
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (α.PredLast p) x → p (mk x)
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), p (Quot.mk (⇑(wSetoid α)) (f i))
⊢ p (Quot.mk (⇑(wSetoid α)) ((P F).wMk a f' f))

Tactic:
change p ⟦q.P.wMk a f' f⟧
    rw [← Fix.ind_aux a f' f]
    apply h
    rw [MvQPF.liftP_iff]
    refine ⟨_, _, rfl, ?_⟩
    intro i j
    cases i
    · apply ih
    · trivial

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
β : Type u_1
Q : β → Prop
u v : β → Cofix F α
h :
  ∀ (x : β),
    Q x →
      ∃ a f' f₀ f₁,
        (u x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₀⟩ ∧
          (v x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₁⟩ ∧
            ∀ (i : (P F).last.B a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
x✝¹ : β
Qx : Q x✝¹
R : Cofix F α → Cofix F α → Prop := fun w z ↦ ∃ x', Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F α
x✝ : R x y
x' : β
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
⊢ LiftR (α.RelLast R) x.dest y.dest

Tactic:
by
      rcases h x' Qx' with ⟨a, f', f₀, f₁, ux'eq, vx'eq, h'⟩
      rw [liftR_iff]
      refine
        ⟨a, q.P.appendContents f' f₀, q.P.appendContents f' f₁, xeq.symm ▸ ux'eq,
          yeq.symm ▸ vx'eq, ?_⟩
      intro i; cases i
      · apply h'
      · intro j
        apply Eq.refl

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 : Cofix F α
h : x.dest = y.dest
⊢ mk x.dest = y

Tactic:
h,

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : Cofix F α
h : x.dest = y.dest
⊢ mk y.dest = y
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 : F (α ::: Cofix F α)
h : mk x = mk y
⊢ (mk x).dest = y

Tactic:
h,

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : F (α ::: Cofix F α)
h : mk x = mk y
⊢ (mk y).dest = y
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h.inr
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 := fun x y ↦ x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r x y
⊢ Quot.mk r' <$> x.dest = Quot.mk r' <$> y.dest

Tactic:
have : ∀ x y, r x y → r' x y := fun x y h => Or.inr h

Goal state after:
case h.inr
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 := fun x y ↦ x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
⊢ Quot.mk r' <$> x.dest = Quot.mk r' <$> y.dest
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inl
r : ℝ
hn : r.sign = -1
⊢ r.sign⁻¹ = r.sign

pp: case inr.inl
r : ℝ
hz : r.sign = 0
⊢ r.sign⁻¹ = r.sign

pp: case inr.inr
r : ℝ
hp : r.sign = 1
⊢ r.sign⁻¹ = r.sign

Tactic:
· rw [hn]
    simp

Goal state after:
case inr.inl
r : ℝ
hz : r.sign = 0
⊢ r.sign⁻¹ = r.sign

case inr.inr
r : ℝ
hp : r.sign = 1
⊢ r.sign⁻¹ = r.sign
Module: Mathlib.Data.Set.Enumerate

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

Tactic:
cases m with
      | zero => contradiction
      | succ m' =>
        simp only [enumerate, hs] at h ⊢
        have hm : n ≤ m' := Nat.le_of_succ_le_succ hm
        exact enumerate_eq_none h hm

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

Goal state before:
pp: α : Type u
s : WSeq α
a a' : α
s' : WSeq α
⊢ some (a', s') ∈ s.destruct → (a ∈ s ↔ a = a' ∨ a ∈ s')

Tactic:
generalize e : destruct s = c

Goal state after:
α : Type u
s : WSeq α
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
e : s.destruct = c
⊢ some (a', s') ∈ c → (a ∈ s ↔ a = a' ∨ a ∈ s')
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
⊢ ∀ {s t : WSeq α}, s ~ʷ t → s.head ~ t.head

Tactic:
by
  suffices ∀ {s t : WSeq α}, s ~ʷ t → ∀ {o}, o ∈ head s → o ∈ head t from fun s t h o =>
    ⟨this h, this h.symm⟩
  intro s t h o ho
  rcases @Computation.exists_of_mem_map _ _ _ _ (destruct s) ho with ⟨ds, dsm, dse⟩
  rw [← dse]
  obtain ⟨l, r⟩ := destruct_congr h
  rcases l dsm with ⟨dt, dtm, dst⟩
  rcases ds with - | a <;> rcases dt with - | b
  · apply Computation.mem_map _ dtm
  · cases b
    cases dst
  · cases a
    cases dst
  · 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: α : 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'
⊢ (match
      match parallel.aux2 l with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (match S.destruct with
          | none => (b, Seq.nil)
          | some (none, S') => (b, S')
          | some (some c, S') => (c :: b, S')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec parallel.aux1 b)) =
    Sum.inr ?m.158

Tactic:
h,

Goal state after:
α : 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'
⊢ (match
      match Sum.inr l' with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (match S.destruct with
          | none => (b, Seq.nil)
          | some (none, S') => (b, S')
          | some (some c, S') => (c :: b, S')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec parallel.aux1 b)) =
    Sum.inr ?m.158
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h1.inl
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : a = a'
⊢ some a ∈ (cons a' s').get? 0

Tactic:
simp only [get?, drop, head_cons]

Goal state after:
case h1.inl
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : a = a'
⊢ some a ∈ Computation.pure (some a')
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case none
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ s.get? n
om : none ∈ (s.drop n).destruct
this : Prod.fst <$> none = some a
⊢ ∃ s', some (a, s') ∈ (s.drop n).destruct

Tactic:
injection this

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

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

Tactic:
refine ⟨a :: l', s, ?_, ?_⟩ <;> simp

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

Goal state before:
pp: case inr.inr.inr
α : 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
c : Computation α
l val✝ : List (Computation α)
IH : F l (Sum.inr val✝)
c' : Computation α
h : c.destruct = Sum.inr c'
a' : α
d : Computation α
dm : d ∈ c' :: val✝
ad : a' ∈ d
dl : d ∈ val✝
⊢ ∃ c_1 ∈ c :: l, a' ∈ c_1

Tactic:
obtain ⟨d, dm⟩ := IH a' ⟨d, dl, ad⟩

Goal state after:
case inr.inr.inr
α : 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
c : Computation α
l val✝ : List (Computation α)
IH : F l (Sum.inr val✝)
c' : Computation α
h : c.destruct = Sum.inr c'
a' : α
d✝ : Computation α
dm✝ : d✝ ∈ c' :: val✝
ad : a' ∈ d✝
dl : d✝ ∈ val✝
d : Computation α
dm : d ∈ l ∧ a' ∈ d
⊢ ∃ c_1 ∈ c :: l, a' ∈ c_1
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case nil.nil
⊢ ltb { s := ofList [], i := 0 } { s := ofList [], i := 0 } = true ↔ [] < []

Tactic:
unfold ltb; decide

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

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
a' : α
v' : Vector α n
h : v = a' ::ᵥ v'
⊢ a ∈ v.toList ↔ a = v.head ∨ a ∈ v.tail.toList

Tactic:
h,

Goal state after:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
a' : α
v' : Vector α n
h : v = a' ::ᵥ v'
⊢ a ∈ (a' ::ᵥ v').toList ↔ a = (a' ::ᵥ v').head ∨ a ∈ (a' ::ᵥ v').tail.toList
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case mpr.inr.inl
α₁ : 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 : β₂
c : γ₁
hc : c ∈ g₁ a b
⊢ inl c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b)

pp: case mpr.inr.inr.inl
α₁ : 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 : β₂
c : γ₂
hc : c ∈ g₂ a b
⊢ inr c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b)

pp: case mpr.inr.inr.inr
α₁ : 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 : β₂
c : γ₂
hc : c ∈ f₂ a b
⊢ inr c ∈ sumLexLift f₁ f₂ g₁ g₂ (inr a) (inr b)

Tactic:
· exact inl_mem_disjSum.2 hc

Goal state after:
case mpr.inr.inr.inl
α₁ : 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 : β₂
c : γ₂
hc : c ∈ g₂ a b
⊢ inr c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b)

case mpr.inr.inr.inr
α₁ : 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 : β₂
c : γ₂
hc : c ∈ f₂ a b
⊢ inr c ∈ sumLexLift f₁ f₂ g₁ g₂ (inr a) (inr b)
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
f' : α → β
s✝ : σ
h : ∀ (a : α) (s : σ), (f a s).2 = f' a
a : α
s s' : σ
x✝¹ : s ∈ Set.univ
x✝ : s' ∈ Set.univ
⊢ (f a s).2 = (f a s').2

Tactic:
h,

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
f' : α → β
s✝ : σ
h : ∀ (a : α) (s : σ), (f a s).2 = f' a
a : α
s s' : σ
x✝¹ : s ∈ Set.univ
x✝ : s' ∈ Set.univ
⊢ f' a = (f a s').2
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
f' : α → β → γ
s✝ : σ
h : ∀ (a : α) (b : β) (s : σ), (f a b s).2 = f' a b
a : α
b : β
s s' : σ
x✝¹ : s ∈ Set.univ
x✝ : s' ∈ Set.univ
⊢ (f a b s).2 = (f a b s').2

Tactic:
h,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
f' : α → β → γ
s✝ : σ
h : ∀ (a : α) (b : β) (s : σ), (f a b s).2 = f' a b
a : α
b : β
s s' : σ
x✝¹ : s ∈ Set.univ
x✝ : s' ∈ Set.univ
⊢ f' a b = (f a b s').2
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
x : ℝ
g : G
this : τ (f₂ g⁻¹) = -τ (f₂ g)
⊢ (f₂ g⁻¹) (x + τ (f₁ g) + 1) = (f₂ g⁻¹) (x + τ (f₂ g)) + 1

Tactic:
h,

Goal state after:
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
x : ℝ
g : G
this : τ (f₂ g⁻¹) = -τ (f₂ g)
⊢ (f₂ g⁻¹) (x + τ (f₂ g) + 1) = (f₂ g⁻¹) (x + τ (f₂ g)) + 1
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: case mp
p : ℝ
inst✝ : Fact (0 < p)
a : AddCircle p
ha : addOrderOf a ≠ 0
hd : addOrderOf a = 0
⊢ False

Tactic:
exact ha hd

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j ↦ ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
⊢ EventuallyConst s (ae volume)

Tactic:
have hu₀ : ∀ j, addOrderOf (u j) = n.natAbs ^ j := fun j => by
        convert!
          addOrderOf_div_of_gcd_eq_one (p := T) (m := 1) (pow_pos (pos_of_gt hn) j) (gcd_one_left _)
        norm_cast

Goal state after:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j ↦ ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
⊢ EventuallyConst s (ae volume)
Module: Mathlib.Dynamics.Ergodic.Function

Goal state before:
pp: α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : Nonempty X
inst✝¹ : MeasurableSpace X
inst✝ : MeasurableSpace.CountablySeparated X
f : α → α
g : α → X
h : PreErgodic f μ
hgm : Measurable g
hg_eq : g ∘ f = g
U : Set X
hU : MeasurableSet U
⊢ g ∘ f ⁻¹' U = g ⁻¹' U

Tactic:
hg_eq

Goal state after:
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : Nonempty X
inst✝¹ : MeasurableSpace X
inst✝ : MeasurableSpace.CountablySeparated X
f : α → α
g : α → X
h : PreErgodic f μ
hgm : Measurable g
hg_eq : g ∘ f = g
U : Set X
hU : MeasurableSet U
⊢ g ⁻¹' U = g ⁻¹' U
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x : AddCircle T
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
h : n - 1 ≠ 0
⊢ n • DivisibleBy.div x (n - 1) = (n - 1) • DivisibleBy.div x (n - 1) + DivisibleBy.div x (n - 1)

Tactic:
rw [sub_smul, one_smul, sub_add_cancel]

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

Goal state before:
pp: A : Type u_1
G : Type u_2
inst✝¹ : Monoid G
inst✝ : TopologicalSpace A
g : G
⊢ Continuous[Pi.topologicalSpace, Pi.topologicalSpace] (mulShift g)

Tactic:
unfold mulShift

Goal state after:
A : Type u_1
G : Type u_2
inst✝¹ : Monoid G
inst✝ : TopologicalSpace A
g : G
⊢ Continuous[Pi.topologicalSpace, Pi.topologicalSpace] fun x h ↦ x (g * h)
Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
inst✝ : UniformSpace X
h : Continuous[inst✝.toTopologicalSpace, inst✝.toTopologicalSpace] T
U_uni : U ∈ 𝓤 X
n : ℕ
x : X
⊢ ∀ (a : ℕ) (b : a ∈ Ico 0 n), ball x ((map T T)^[↑⟨a, b⟩] ⁻¹' U) ∈ 𝓝 x

Tactic:
intro k

Goal state after:
X : Type u_1
T : X → X
U : SetRel X X
inst✝ : UniformSpace X
h : Continuous[inst✝.toTopologicalSpace, inst✝.toTopologicalSpace] T
U_uni : U ∈ 𝓤 X
n : ℕ
x : X
k : ℕ
⊢ ∀ (b : k ∈ Ico 0 n), ball x ((map T T)^[↑⟨k, b⟩] ⁻¹' U) ∈ 𝓝 x
Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage

Goal state before:
pp: X : Type u_1
T : X → X
U V : SetRel X X
n : ℕ
⊢ ∀ i < n,
    (⋂ k, ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' U) ○ ⋂ k, ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' V ⊆
      map T^[i] T^[i] ⁻¹' (U ○ V)

Tactic:
intro k

Goal state after:
X : Type u_1
T : X → X
U V : SetRel X X
n k : ℕ
⊢ k < n →
    (⋂ k, ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' U) ○ ⋂ k, ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' V ⊆
      map T^[k] T^[k] ⁻¹' (U ○ V)
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: case inr
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝ : Nonempty X
s_nemp : (↑s).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
t : Fin n → ↥s
y z : X
y_int : ∀ (i : Fin n), ∀ i_1 < m, (T^[i_1] ↑(t i), T^[i_1] (T^[m * ↑i] y)) ∈ U
z_int : ∀ (i : Fin n), ∀ i_1 < m, (T^[i_1] ↑(t i), T^[i_1] (T^[m * ↑i] z)) ∈ U
⊢ ∀ i < m * n, ∃ b, (T^[i] y, b) ∈ U ∧ (b, T^[i] z) ∈ U

Tactic:
intro k

Goal state after:
case inr
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝ : Nonempty X
s_nemp : (↑s).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
t : Fin n → ↥s
y z : X
y_int : ∀ (i : Fin n), ∀ i_1 < m, (T^[i_1] ↑(t i), T^[i_1] (T^[m * ↑i] y)) ∈ U
z_int : ∀ (i : Fin n), ∀ i_1 < m, (T^[i_1] ↑(t i), T^[i_1] (T^[m * ↑i] z)) ∈ U
k : ℕ
⊢ k < m * n → ∃ b, (T^[k] y, b) ∈ U ∧ (b, T^[k] z) ∈ U