mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos.nil
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rx : α
rr : Ordnode α
h : delta * ls < rs
hr : (node rs nil rx rr).Balanced
sr : (node rs nil rx rr).Sized
rd : delta ≤ nil.size + rr.size
⊢ (node ls ll lx lr).rotateL x (node rs nil rx rr) =
    rec nil
      (fun size l x_1 r l_ih r_ih ↦
        rec nil
          (fun size_1 l_1 x_2 r_1 l_ih r_ih ↦
            if size < ratio * size_1 then node (ls + rs + 1) (node (ls + size + 1) (node ls ll lx lr) x nil) rx rr
            else
              node (ls + rs + 1) (node (ls + l.size + 1) (node ls ll lx lr) x l) x_1
                (node (r.size + size_1 + 1) r rx rr))
          rr)
      nil

Tactic:
rw [size, zero_add] at rd

Goal state after:
case pos.nil
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rx : α
rr : Ordnode α
h : delta * ls < rs
hr : (node rs nil rx rr).Balanced
sr : (node rs nil rx rr).Sized
rd : delta ≤ rr.size
⊢ (node ls ll lx lr).rotateL x (node rs nil rx rr) =
    rec nil
      (fun size l x_1 r l_ih r_ih ↦
        rec nil
          (fun size_1 l_1 x_2 r_1 l_ih r_ih ↦
            if size < ratio * size_1 then node (ls + rs + 1) (node (ls + size + 1) (node ls ll lx lr) x nil) rx rr
            else
              node (ls + rs + 1) (node (ls + l.size + 1) (node ls ll lx lr) x l) x_1
                (node (r.size + size_1 + 1) r rx rr))
          rr)
      nil
Module: Mathlib.Data.Pi.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
a : (i : ι) → α i
⊢ #(Ioi a) = ∏ i, #(Ici (a i)) - 1

Tactic:
card_Ioi_eq_card_Ici_sub_one,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
a : (i : ι) → α i
⊢ #(Ici a) - 1 = ∏ i, #(Ici (a i)) - 1
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
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂✝ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := fun b₁ b₂ ↦ ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : (P F).M β
a₁✝ a₂✝ : (P F).M α
ra₁a₂ : r a₁✝ a₂✝
b₁eq : b₁ = g <$$> a₁✝
b₂eq : b₂ = g <$$> a₂✝
a₁ a₂ : (P F).M α
⊢ r a₁ a₂ → Quot.mk r' (g <$$> a₁) = Quot.mk r' (g <$$> a₂)

Tactic:
ra₁a₂

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂✝¹ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := fun b₁ b₂ ↦ ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : (P F).M β
a₁✝ a₂✝ : (P F).M α
ra₁a₂✝ : r a₁✝ a₂✝
b₁eq : b₁ = g <$$> a₁✝
b₂eq : b₂ = g <$$> a₂✝
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
⊢ Quot.mk r' (g <$$> a₁) = Quot.mk r' (g <$$> a₂)
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
g : β → F (α ::: β)
x : β
⊢ (corec g x).dest = (TypeVec.id ::: corec g) <$$> g x

Tactic:
conv =>
    lhs
    rw [Cofix.dest, Cofix.corec]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: β)
x : β
⊢ Quot.lift (fun x ↦ (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯ (Quot.mk Mcongr (corecF g x)) =
    (TypeVec.id ::: corec g) <$$> g x
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
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (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), g₁ (Quot.mk (⇑(wSetoid α)) (f i)) = g₂ (Quot.mk (⇑(wSetoid α)) (f i))
⊢ g₁ (Quot.mk (⇑(wSetoid α)) ((P F).wMk a f' f)) = g₂ (Quot.mk (⇑(wSetoid α)) ((P F).wMk a f' f))

Tactic:
change g₁ ⟦q.P.wMk a f' f⟧ = g₂ ⟦q.P.wMk a f' f⟧

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (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), g₁ (Quot.mk (⇑(wSetoid α)) (f i)) = g₂ (Quot.mk (⇑(wSetoid α)) (f i))
⊢ g₁ ⟦(P F).wMk a f' f⟧ = g₂ ⟦(P F).wMk a f' f⟧
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
⊢ rec g = h

Tactic:
by
  ext x
  apply Fix.ind_rec
  intro x hyp'
  rw [hyp, ← hyp', Fix.rec_eq]

Goal state after:
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
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)
⊢ rec g = h

Tactic:
by
  ext x
  apply Fix.ind_rec
  intro x hyp'
  rw [hyp, ← hyp', Fix.rec_eq]

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

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
⊢ (corec g x).dest = corec g <$> g x

Tactic:
conv =>
    lhs
    rw [Cofix.dest, Cofix.corec]

Goal state after:
F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
⊢ Quot.lift (fun x ↦ Quot.mk Mcongr <$> abs x.dest) ⋯ (Quot.mk Mcongr (corecF g x)) = corec g <$> g x
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inl
r : ℝ
hn : r < 0
⊢ 1 = - -1

Tactic:
neg_neg

Goal state after:
case inl
r : ℝ
hn : r < 0
⊢ 1 = 1
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inl
⊢ (-0).sign = -sign 0

pp: case inr.inr
r : ℝ
hp : 0 < r
⊢ (-r).sign = -r.sign

Tactic:
· rw [sign_zero, neg_zero, sign_zero]

Goal state after:
case inr.inr
r : ℝ
hp : 0 < r
⊢ (-r).sign = -r.sign
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mpr
F : Type u → Type u
q : QPF F
α : Type u
x : F α
u : α
h : ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ
⊢ ∀ ⦃p : α → Prop⦄, Liftp p x → p u

Tactic:
p

Goal state after:
case mpr
F : Type u → Type u
q : QPF F
α : Type u
x : F α
u : α
h : ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ
p : α → Prop
⊢ Liftp p x → p u
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mpr
F : Type u → Type u
q : QPF F
⊢ IsUniform → SuppPreservation

Tactic:
· rintro h α ⟨a, f⟩
    rwa [supp_eq_of_isUniform, PFunctor.supp_eq]

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

Goal state before:
pp: α : Type u
s : WSeq α
a : α
o : Option (α × WSeq α)
md : o ∈ s.tail.destruct
e : Prod.fst <$> o = some a
⊢ ∃ a', some a' ∈ s.head

Tactic:
rcases o with - | o <;> [injection e; injection e with h']

Goal state after:
case some
α : Type u
s : WSeq α
a : α
o : α × WSeq α
md : some o ∈ s.tail.destruct
h' : o.1 = a
⊢ ∃ a', some a' ∈ s.head
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case succ
α : Type u
s : WSeq α
n : ℕ
IH : ∀ {a : α}, some a ∈ s.get? n → ∃ a', some a' ∈ s.head
a : α
h : some a ∈ s.get? (n + 1)
a' : α
h' : some a' ∈ (s.drop n).head
⊢ ∃ a', some a' ∈ s.head

Tactic:
exact IH h'

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:
by
  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.Seq.Parallel

Goal state before:
pp: α : Type u
S : WSeq (Computation α)
c : Computation α
h : c ∈ S
T : c.Terminates
⊢ ∀ (n : ℕ) (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates

Tactic:
intro n

Goal state after:
α : Type u
S : WSeq (Computation α)
c : Computation α
h : c ∈ S
T : c.Terminates
n : ℕ
⊢ ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝ : (fun s1 s2 ↦ ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h : LiftRel R s t
o : Option (α × WSeq α)
⊢ ∀ {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) o b →
      LiftRelO S (fun s1 s2 ↦ ∃ s, s1 = map f1 s ∧ ∃ x, s2 = map f2 x ∧ LiftRel R s x)
        (Option.map (Prod.map f1 (map f1)) o) (Option.map (Prod.map f2 (map f2)) b)

Tactic:
p

Goal state after:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝ : (fun s1 s2 ↦ ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h : LiftRel R s t
o : Option (α × WSeq α)
p : Option (β × WSeq β)
⊢ LiftRelO R (LiftRel R) o p →
    LiftRelO S (fun s1 s2 ↦ ∃ s, s1 = map f1 s ∧ ∃ x, s2 = map f2 x ∧ LiftRel R s x)
      (Option.map (Prod.map f1 (map f1)) o) (Option.map (Prod.map f2 (map f2)) p)
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
o : Option (α × WSeq α)
⊢ ∀ {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) o b →
      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 o) (destruct_append.aux t2 b)

Tactic:
p

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
o : Option (α × WSeq α)
p : Option (β × WSeq β)
⊢ LiftRelO R (LiftRel R) o p →
    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 o) (destruct_append.aux t2 p)
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case cons
α : Type u
a : α
l : List α
IH : l ∈ (↑l).toList
⊢ a :: l ∈ (↑(a :: l)).toList

Tactic:
| cons a l IH =>

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

Goal state before:
pp: case intro
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
x✝ : α
s✝ : WSeq α
m : a ∈ (cons x✝ s✝).append S.join
o :
  a = x✝ ∨
    ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)),
      s.append S_1.join = s✝.append S.join → a ∈ s.append S_1.join → a ∈ s ∨ ∃ s ∈ S_1, a ∈ s
ej : (cons x✝ s✝).append S.join = cons x✝ (s✝.append S.join)
⊢ a ∈ cons x✝ s✝ ∨ ∃ s ∈ S, a ∈ s

Tactic:
simp only [cons_append, mem_cons_iff] at m ⊢

Goal state after:
case intro
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
x✝ : α
s✝ : WSeq α
o :
  a = x✝ ∨
    ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)),
      s.append S_1.join = s✝.append S.join → a ∈ s.append S_1.join → a ∈ s ∨ ∃ s ∈ S_1, a ∈ s
ej : (cons x✝ s✝).append S.join = cons x✝ (s✝.append S.join)
m : a = x✝ ∨ a ∈ s✝.append S.join
⊢ (a = x✝ ∨ a ∈ s✝) ∨ ∃ s ∈ S, a ∈ s
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
⊢ Computation.LiftRel
    (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)
    (s.destruct.bind (destruct_append.aux S.join)) (t.append T.join).destruct

Tactic:
destruct_append

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
⊢ Computation.LiftRel
    (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)
    (s.destruct.bind (destruct_append.aux S.join)) (t.destruct.bind (destruct_append.aux T.join))
Module: Mathlib.Data.Sum.Interval

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

Tactic:
exact mem_map_of_mem _ hc

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

Tactic:
exact inl_mem_disjSum.2 hc

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

Goal state before:
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 mem_map_of_mem _ hc

Goal state after:
Module: Mathlib.Data.W.Constructions

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

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

Goal state after:
Module: Mathlib.Data.Vector3

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector3 α n
⊢ insert a v fz = a :: v

Tactic:
refine funext fun j => j.cases' ?_ ?_ <;> intros <;> rfl

Goal state after:
Module: Mathlib.Order.SemiconjSup

Goal state before:
pp: α : Type u_1
G : Type u_4
inst✝¹ : PartialOrder α
inst✝ : Group G
f₁ f₂ : G →* α ≃o α
h : α → α
H : ∀ (x : α), IsLUB (range fun g' ↦ (f₁ g')⁻¹ ((f₂ g') x)) (h x)
g : G
y : α
this : IsLUB (⇑(f₁ g) '' range fun g' ↦ (f₁ g')⁻¹ ((f₂ g') y)) ((f₁ g) (h y))
⊢ IsLUB (range fun g' ↦ (f₁ g')⁻¹ ((f₂ g') ((f₂ g) y))) ((f₁ g) (h y))

Tactic:
← range_comp,

Goal state after:
α : Type u_1
G : Type u_4
inst✝¹ : PartialOrder α
inst✝ : Group G
f₁ f₂ : G →* α ≃o α
h : α → α
H : ∀ (x : α), IsLUB (range fun g' ↦ (f₁ g')⁻¹ ((f₂ g') x)) (h x)
g : G
y : α
this : IsLUB (range (⇑(f₁ g) ∘ fun g' ↦ (f₁ g')⁻¹ ((f₂ g') y))) ((f₁ g) (h y))
⊢ IsLUB (range fun g' ↦ (f₁ g')⁻¹ ((f₂ g') ((f₂ g) y))) ((f₁ g) (h y))
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: 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

Tactic:
intro n

Goal state after:
f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C
n : ℕ
⊢ dist (f.transnumAuxSeq n) (x (2 ^ n) / 2 ^ n) ≤ C / 2 ^ n
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: case mpr
f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
⊢ (∃ x, f x = x + ↑m) → τ f = ↑m

Tactic:
· rintro ⟨x, hx⟩
    exact f.translationNumber_of_eq_add_int hx

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

Goal state before:
pp: X : Type u_2
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : R1Space X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
M : Type u_3
inst✝⁶ : Monoid M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : MulAction M X
inst✝³ : ContinuousSMul M X
g : M
hg : DenseRange fun x ↦ g ^ x
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul M X μ
this✝¹ : MeasurableSpace M := borel M
this✝ : BorelSpace M
s : Set X
hsm : MeasurableSet s
hs : (fun x ↦ g • x) ⁻¹' s = s
⊢ EventuallyConst s (ae μ)

Tactic:
refine aeconst_of_dense_setOfPred_preimage_smul_eq hsm.nullMeasurableSet (hg.mono ?_)

Goal state after:
X : Type u_2
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : R1Space X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
M : Type u_3
inst✝⁶ : Monoid M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : MulAction M X
inst✝³ : ContinuousSMul M X
g : M
hg : DenseRange fun x ↦ g ^ x
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul M X μ
this✝¹ : MeasurableSpace M := borel M
this✝ : BorelSpace M
s : Set X
hsm : MeasurableSet s
hs : (fun x ↦ g • x) ⁻¹' s = s
⊢ (range fun x ↦ g ^ x) ⊆ {g | (fun x ↦ g • x) ⁻¹' s = s}
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
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) := ⋯
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[μ] s
n : ι → ℕ := ⋯
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : μ s ≠ 0
⊢ μ s = ENNReal.ofReal T

Tactic:
obtain ⟨d, -, hd⟩ : ∃ d, d ∈ s ∧ ∀ {ι'} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[>] 0) → (∀ᶠ j in l, d ∈ closedBall (w j) (1 * δ j)) →
      Tendsto (fun j => μ (s ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1) :=
    exists_mem_of_measure_ne_zero_of_ae h
      (IsUnifLocDoublingMeasure.ae_tendsto_measure_inter_div μ s 1)

Goal state after:
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
d : AddCircle T
hd :
  ∀ {ι' : Type ?u.149} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (fun j ↦ μ (s ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1)
⊢ μ s = ENNReal.ofReal T
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: case refine_2
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := ⋯
n : ℕ := ⋯
B : Set (AddCircle T) := ⋯
hI : I =ᵐ[volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
hBg : g +ᵥ B = ball (g + x) (T / (2 * ↑n))
⊢ T / (2 * ↑n) + T / (2 * ↑n) ≤ dist (g + x) x

Tactic:
dist_eq_norm,

Goal state after:
case refine_2
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
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
hBg : g +ᵥ B = ball (g + x) (T / (2 * ↑n))
⊢ T / (2 * ↑n) + T / (2 * ↑n) ≤ ‖g + x - x‖
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
⊢ ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, a ∈ s → ∃ b, i ≤ b ∧ f^[b] a ∈ s

Tactic:
intro n

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
n : ℕ
⊢ ∀ᵐ (a : α) ∂μ, a ∈ s → ∃ b, n ≤ b ∧ f^[b] a ∈ s
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: case succ
α : 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
⊢ ∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[n + 1]^[m] x ∈ s

Tactic:
refine ⟨f^[k] x, hk, m, ?_, ?_⟩

Goal state after:
case succ.refine_1
α : 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
⊢ m ≠ 0

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^[n + 1]^[m] (f^[k] x) ∈ s
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
⊢ ∀ᵐ (x : α) ∂ν.withDensity (μ.rnDeriv ν), 0 < (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x

Tactic:
ae_withDensity_iff (Measure.measurable_rnDeriv _ _),

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
⊢ ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x ≠ 0 → 0 < (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ ((ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν =ᵐ[ν]
    ((ν.withDensity (μ.rnDeriv ν)).withDensity f + (μ.singularPart ν).withDensity f).rnDeriv ν

Tactic:
have : SigmaFinite ((μ.singularPart ν).withDensity f) :=
    SigmaFinite.withDensity_of_ne_top (ae_mono (Measure.singularPart_le _ _) hf_ne_top)

Goal state after:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
this : SigmaFinite ((μ.singularPart ν).withDensity f)
⊢ ((ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν =ᵐ[ν]
    ((ν.withDensity (μ.rnDeriv ν)).withDensity f + (μ.singularPart ν).withDensity f).rnDeriv ν