mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Rat.Cast.OfScientific

Goal state before:
pp: K : Type u_1
inst✝¹ : _root_.Field K
inst✝ : CharZero K
m : ℕ
s : Bool
e : ℕ
⊢ OfScientific.ofScientific m s e = if s = true then ↑m / 10 ^ e else ↑m * 10 ^ e

Tactic:
← NNRat.cast_ofScientific,

Goal state after:
K : Type u_1
inst✝¹ : _root_.Field K
inst✝ : CharZero K
m : ℕ
s : Bool
e : ℕ
⊢ ↑(OfScientific.ofScientific m s e) = if s = true then ↑m / 10 ^ e else ↑m * 10 ^ e
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 : Cofix F α
⊢ mk x.dest = x

Tactic:
by
  apply Cofix.bisim_rel (fun x y : Cofix F α => x = Cofix.mk (Cofix.dest y)) _ _ _ rfl
  intro x y h
  rw [h]
  conv =>
    lhs
    congr
    rfl
    rw [Cofix.mk]
    rw [Cofix.dest_corec]
  rw [← comp_map, ← appendFun_comp, id_comp]
  rw [← comp_map, ← appendFun_comp, id_comp, ← Cofix.mk]
  congr 1
  apply congrArg
  funext x
  apply Quot.sound
  rfl

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)
⊢ LiftR' (α.RelLast' R) (Cofix.corec (g ∘ f) x).dest b.dest

Tactic:
Hb,

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)
⊢ LiftR' (α.RelLast' R) (Cofix.corec (g ∘ f) x).dest (Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)).dest
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case inl
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x✝ : β
i : Cofix F α
R : Cofix F α → Cofix F α → Prop :=
  fun a b ↦
    ∃ x,
      a =
          corec
            (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
              Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    corec
      (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
        Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
      (Sum.inl x)
Hb : b = x
⊢ LiftR' (α.RelLast' R)
    (corec
        (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
          Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
        (Sum.inl x)).dest
    b.dest

Tactic:
Hb,

Goal state after:
case inl
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x✝ : β
i : Cofix F α
R : Cofix F α → Cofix F α → Prop :=
  fun a b ↦
    ∃ x,
      a =
          corec
            (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
              Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    corec
      (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
        Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
      (Sum.inl x)
Hb : b = x
⊢ LiftR' (α.RelLast' R)
    (corec
        (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
          Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
        (Sum.inl x)).dest
    x.dest
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s1 : WSeq α
s2 : WSeq β
h✝ : LiftRel R s1 s2
s : WSeq β
t : WSeq α
h : LiftRel R t s
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct s.destruct

Tactic:
apply liftRel_destruct h

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

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

Tactic:
cases hs : sel s
    · exact enumerate_eq_none_of_sel sel hs
    · 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
n : ℕ
⊢ nil.drop n = nil

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

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

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

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

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

Goal state before:
pp: α : Type u
s : WSeq α
a : α × WSeq α
h : some a ∈ s.tail.destruct
⊢ ∃ a', some a' ∈ s.destruct

Tactic:
unfold tail Functor.map at h; simp only [destruct_flatten] at h
  rcases exists_of_mem_bind h with ⟨t, tm, td⟩; clear h
  rcases Computation.exists_of_mem_map tm with ⟨t', ht', ht2⟩; clear tm
  rcases t' with - | t' <;> rw [← ht2] at td <;> simp only [destruct_nil] at td
  · have := mem_unique td (ret_mem _)
    contradiction
  · exact ⟨_, ht'⟩

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
⊢ IsTrans (WSeq α) (LiftRel R)

Tactic:
refine ⟨fun s t u h1 h2 ↦ ?_⟩
  refine ⟨fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u, ⟨t, h1, h2⟩, fun {s u} h => ?_⟩
  rcases h with ⟨t, h1, h2⟩
  have h1 := liftRel_destruct h1
  have h2 := liftRel_destruct h2
  refine
    Computation.liftRel_def.2
      ⟨(Computation.terminates_of_liftRel h1).trans (Computation.terminates_of_liftRel h2),
        fun {a c} ha hc => ?_⟩
  rcases h1.left ha with ⟨b, hb, t1⟩
  have t2 := Computation.rel_of_liftRel h2 hb hc
  obtain - | a := a <;> obtain - | c := c
  · trivial
  · cases b
    · cases t2
    · cases t1
  · cases a
    rcases b with - | b
    · cases t1
    · cases b
      cases t2
  · obtain ⟨a, s⟩ := a
    rcases b with - | b
    · cases t1
    obtain ⟨b, t⟩ := b
    obtain ⟨c, u⟩ := c
    obtain ⟨ab, st⟩ := t1
    obtain ⟨bc, tu⟩ := t2
    exact ⟨trans_of R ab bc, t, st, tu⟩

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

Goal state before:
pp: α : Type u
s : WSeq α
a : α
n : ℕ
⊢ some a ∈ s.get? n → a ∈ s

Tactic:
by
  induction n generalizing s <;> intro h
  case zero =>
    rcases Computation.exists_of_mem_map h with ⟨o, h1, h2⟩
    rcases o with - | o
    · injection h2
    injection h2 with h'
    obtain ⟨a', s'⟩ := o
    exact (eq_or_mem_iff_mem h1).2 (Or.inl h'.symm)
  case succ n IH =>
    have := @IH (tail s)
    rw [get?_tail] at this
    exact mem_of_mem_tail (this h)

Goal state after:
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
c : Computation α
l : List (Computation α)
IH :
  F l
    (List.foldr
      (fun c o ↦
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)
      (Sum.inr []) l)
⊢ F (c :: l)
    (match
      List.foldr
        (fun c o ↦
          match o with
          | Sum.inl a => Sum.inl a
          | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)
        (Sum.inr []) l with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)

Tactic:
revert IH

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
c : Computation α
l : List (Computation α)
⊢ F l
      (List.foldr
        (fun c o ↦
          match o with
          | Sum.inl a => Sum.inl a
          | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)
        (Sum.inr []) l) →
    F (c :: l)
      (match
        List.foldr
          (fun c o ↦
            match o with
            | Sum.inl a => Sum.inl a
            | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)
          (Sum.inr []) l with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
a : α
s : WSeq α
⊢ (cons a s).toList.destruct = Sum.inr (List.cons a <$> s.toList)

Tactic:
by
    unfold toList
    simp only [toList'_cons, Computation.destruct_think, Sum.inr.injEq]
    rw [toList'_map]
    simp only [List.reverse_cons, List.reverse_nil, List.nil_append, List.singleton_append]
    rfl

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

Goal state before:
pp: α : Type u
s : Seq α
⊢ (match
      match Option.map (fun a' ↦ (a', (some <$> s).tail)) ((some <$> s).get? 0) with
      | none => Sum.inl none
      | some (none, s') => Sum.inr s'
      | some (some a, s') => Sum.inl (some (a, s')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b =>
      Sum.inr
        (Computation.corec
          (fun s ↦
            match Option.map (fun a' ↦ (a', Seq.tail s)) (Seq.get? s 0) with
            | none => Sum.inl none
            | some (none, s') => Sum.inr s'
            | some (some a, s') => Sum.inl (some (a, s')))
          b)) =
    Sum.inl (Option.map (fun a ↦ (a, some <$> s.tail)) (s.get? 0))

Tactic:
show Seq.get? (some <$> s) 0 = some <$> Seq.get? s 0 by apply Seq.map_get?

Goal state after:
α : Type u
s : Seq α
⊢ (match
      match Option.map (fun a' ↦ (a', (some <$> s).tail)) (some <$> s.get? 0) with
      | none => Sum.inl none
      | some (none, s') => Sum.inr s'
      | some (some a, s') => Sum.inl (some (a, s')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b =>
      Sum.inr
        (Computation.corec
          (fun s ↦
            match Option.map (fun a' ↦ (a', Seq.tail s)) (Seq.get? s 0) with
            | none => Sum.inl none
            | some (none, s') => Sum.inr s'
            | some (some a, s') => Sum.inl (some (a, s')))
          b)) =
    Sum.inl (Option.map (fun a ↦ (a, some <$> s.tail)) (s.get? 0))
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case h1.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
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = pure a
l' : List (Computation α)
this : F l (Sum.inr l')
e' :
  rmap (corec parallel.aux1)
      (rmap
        (fun l' ↦
          match Seq.destruct S with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        (Sum.inr l')) =
    Sum.inl a
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
injection e'

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

Goal state before:
pp: case h2.inl
α : 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
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = C'.think
a' : α
this : F l (Sum.inl a')
e' :
  rmap (corec parallel.aux1)
      (rmap
        (fun l' ↦
          match Seq.destruct S with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        (Sum.inl a')) =
    Sum.inr C'
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
injection e'

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

Goal state before:
pp: α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun c ↦ map (fun a ↦ (a, c)) c) S
c : Computation α
⊢ c = map ((fun c ↦ c.1) ∘ fun a ↦ (a, c)) c

Tactic:
exact (map_id _).symm

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

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

Tactic:
exact map_eq_empty.2 (h.1 _ _ rfl rfl)

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

Goal state before:
pp: case succ
α : Type u_1
n✝ : ℕ
a : α
n : ℕ
a✝ : ∀ (v : Vector α n), a ∈ v.tail.toList → a ∈ v.toList
v : Vector α (n + 1)
ha : a ∈ v.tail.toList
⊢ a ∈ v.toList

Tactic:
| succ n _ =>

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

Goal state before:
pp: case mp.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 γ₂
c : γ₁ ⊕ γ₂
a : α₂
b : β₂
⊢ c ∈ sumLexLift f₁ f₂ g₁ g₂ (inr a) (inr b) →
    (∃ a₁ b₁ c₁, inr a = inl a₁ ∧ inr b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
      (∃ a₁ b₂ c₁, inr a = inl a₁ ∧ inr b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ a₁ b₂ c₂, inr a = inl a₁ ∧ inr b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
          ∃ a₂ b₂ c₂, inr a = inr a₂ ∧ inr b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂

Tactic:
· rw [sumLexLift, mem_map]
      rintro ⟨c, hc, rfl⟩
      exact Or.inr (Or.inr <| Or.inr <| ⟨a, b, c, rfl, rfl, rfl, hc⟩)

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

Goal state before:
pp: case mpr
α₁ : 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 : γ₁ ⊕ γ₂
⊢ ((∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
      (∃ a₁ b₂ c₁, a = inl a₁ ∧ b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ a₁ b₂ c₂, a = inl a₁ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
          ∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂) →
    c ∈ sumLexLift f₁ f₂ g₁ g₂ a b

Tactic:
· rintro (⟨a, b, c, rfl, rfl, rfl, hc⟩ | ⟨a, b, c, rfl, rfl, rfl, hc⟩ |
      ⟨a, b, c, rfl, rfl, rfl, hc⟩ | ⟨a, b, c, rfl, rfl, rfl, hc⟩)
    · exact mem_map_of_mem _ hc
    · exact inl_mem_disjSum.2 hc
    · exact inr_mem_disjSum.2 hc
    · exact mem_map_of_mem _ hc

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

Goal state before:
pp: case snoc
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
f : α → β → σ → σ × γ
f' : β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a b s = f' b s
n✝ : ℕ
xs : Vector α n✝
ys : Vector β n✝
x : α
y : β
ih : ∀ {s : σ}, mapAccumr₂ f xs ys s = mapAccumr f' ys s
s : σ
⊢ mapAccumr₂ f (xs.snoc x) (ys.snoc y) s = mapAccumr f' (ys.snoc y) s

Tactic:
| snoc xs ys x y ih =>

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

Goal state before:
pp: case snoc
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
f : α → β → σ → σ × γ
f' : α → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a b s = f' a s
n✝ : ℕ
xs : Vector α n✝
ys : Vector β n✝
x : α
y : β
ih : ∀ {s : σ}, mapAccumr₂ f xs ys s = mapAccumr f' xs s
s : σ
⊢ mapAccumr₂ f (xs.snoc x) (ys.snoc y) s = mapAccumr f' (xs.snoc x) s

Tactic:
| snoc xs ys x y ih =>

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

Goal state before:
pp: case refine_4.inl.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 γ₂
val✝¹ : α₁
val✝ : β₁
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inl val✝¹ = inl a₁ → inl val✝ = inl b₁ → f₁ a₁ b₁ = ∅) ∧
    (∀ (a₁ : α₁) (b₂ : β₂), inl val✝¹ = inl a₁ → inl val✝ = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
      ∀ (a₂ : α₂) (b₂ : β₂), inl val✝¹ = inr a₂ → inl val✝ = inr b₂ → f₂ a₂ b₂ = ∅
⊢ sumLexLift f₁ f₂ g₁ g₂ (inl val✝¹) (inl val✝) = ∅

Tactic:
exact map_eq_empty.2 (h.1 _ _ rfl rfl)

Goal state after:
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 []

Tactic:
← eq_nil v

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

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

Tactic:
gcongr; exact (f ^ 2 ^ n).dist_map_map_zero_lt (f ^ 2 ^ n)

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hsm : NullMeasurableSet s μ
hs₀ : μ s ≠ 0
t : Set α
hsub : t ⊆ s
htm : MeasurableSet t
hts : t =ᵐ[μ] s
⊢ μ t ≠ 0

Tactic:
rwa [measure_congr hts]

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

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

Tactic:
rw [← hx2, hx, hx1]

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

Goal state before:
pp: A : Type u_1
G : Type u_2
inst✝ : Monoid G
x : G → A
⊢ mulShift 1 x = x

Tactic:
ext h

Goal state after:
A : Type u_1
G : Type u_2
inst✝ : Monoid G
x : G → A
h : G
⊢ mulShift 1 x h = x h
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
G : Type u_2
inst✝ : Monoid G
g₁ g₂ : G
x : G → A
⊢ mulShift (g₁ * g₂) x = mulShift g₂ (mulShift g₁ x)

Tactic:
ext h

Goal state after:
A : Type u_1
G : Type u_2
inst✝ : Monoid G
g₁ g₂ : G
x : G → A
h : G
⊢ mulShift (g₁ * g₂) x h = mulShift g₂ (mulShift g₁ x) h
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst✝] n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst✝] (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u ↦ (closure[inst✝] (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen[inst✝] (j u)
⊢ k \ n ⊆ ⋃ u ∈ f, j u

Tactic:
have : ⋃ u ∈ f, j u = ⋃ u : (↥f.sets), j u := biUnion_eq_iUnion _ _

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst✝] n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst✝] (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u ↦ (closure[inst✝] (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen[inst✝] (j u)
this : ⋃ u ∈ f, j u = ⋃ u, j ↑u
⊢ k \ n ⊆ ⋃ u ∈ f, j u
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : μ.HaveLebesgueDecomposition ν
inst✝¹ : μ.HaveLebesgueDecomposition (ν + ν')
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hνν' : ν ⟂ₘ ν'
t : Set α := hνν'.nullSet
ht : MeasurableSet t
⊢ μ.rnDeriv (ν + ν') =ᵐ[ν.restrict tᶜ] μ.rnDeriv ν

Tactic:
rw [← withDensity_eq_iff_of_sigmaFinite (μ := ν.restrict tᶜ)
    (Measure.measurable_rnDeriv _ _).aemeasurable (Measure.measurable_rnDeriv _ _).aemeasurable]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : μ.HaveLebesgueDecomposition ν
inst✝¹ : μ.HaveLebesgueDecomposition (ν + ν')
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hνν' : ν ⟂ₘ ν'
t : Set α := hνν'.nullSet
ht : MeasurableSet t
⊢ (ν.restrict tᶜ).withDensity (μ.rnDeriv (ν + ν')) = (ν.restrict tᶜ).withDensity (μ.rnDeriv ν)
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
inst✝ : V.IsSymm
n : ℕ
h' : coverMincard T (φ '' F) V n = ⊤
⊢ coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) V n

Tactic:
exact h' ▸ le_top

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

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : SetRel Y Y
n : ℕ
h' : coverMincard S F (map φ φ ⁻¹' V) n = ⊤
⊢ coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n

Tactic:
exact h' ▸ le_top

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

Goal state before:
pp: case inr
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
inst✝¹ : U.IsRefl
inst✝ : U.IsSymm
n : ℕ
h : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_card : ↑s.card = netMaxcard T F U n
⊢ IsDynCoverOf T F (U ○ U) n ↑s

Tactic:
IsDynCoverOf,

Goal state after:
case inr
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
inst✝¹ : U.IsRefl
inst✝ : U.IsSymm
n : ℕ
h : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_card : ↑s.card = netMaxcard T F U n
⊢ (dynEntourage T (U ○ U) n).IsCover F ↑s
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: case inl
X : Type u_1
T : X → X
V : SetRel X X
inst✝ : UniformSpace X
h : Continuous T
F : Set X
U : SetRel X X
V_uni : V ∈ 𝓤 X
n : ℕ
h' : coverMincard T F U n = ⊤
⊢ coverMincard T (closure F) (V ○ U) n ≤ coverMincard T F U n

Tactic:
exact h' ▸ le_top

Goal state after:
Module: Mathlib.Dynamics.Transitive

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Monoid M
inst✝ : MulAction M α
h : ContinuousConstSMul M α
⊢ IsTopologicallyTransitive M α ↔
    ∀ {U : Set α}, IsOpen U → U.Nonempty → (∀ (m : M), (fun x ↦ m • x) ⁻¹' U ⊆ U) → Dense U

Tactic:
refine ⟨fun _ _ h₀ h₁ h₂ ↦ h₀.dense_of_preimage_smul_invariant M h₁ h₂, fun h₄ ↦ ?_⟩
  refine (isTopologicallyTransitive_iff_dense_iUnion_preimage M).mpr ?_
  refine fun hU _ ↦ h₄ (isOpen_iUnion fun a ↦ hU.preimage (h.1 a)) ?_ fun b _ ↦ ?_
  · exact nonempty_iUnion.mpr ⟨1, by simpa only [one_smul]⟩
  · simp only [preimage_iUnion, mem_iUnion, mem_preimage, smul_smul, forall_exists_index]
    exact fun c hc ↦ ⟨c * b, hc⟩

Goal state after: