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

Goal state before:
pp: case ind
α : Type u
β : Type v
R : α → β → Prop
U : WSeq α → WSeq β → Prop
HU :
  ∀ (s1 : WSeq α) (s2 : WSeq β),
    (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) → U s1 s2
n : ℕ
IH :
  ∀ m < n,
    ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
      LiftRel (LiftRel R) S T →
        ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a m → ∃ b ∈ T.join.destruct, LiftRelO R U a b
⊢ ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
    LiftRel (LiftRel R) S T →
      ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a n → ∃ b ∈ T.join.destruct, LiftRelO R U a b

Tactic:
| _ n IH
   => 

Goal state after:
case ind
α : Type u
β : Type v
R : α → β → Prop
U : WSeq α → WSeq β → Prop
HU :
  ∀ (s1 : WSeq α) (s2 : WSeq β),
    (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) → U s1 s2
n : ℕ
IH :
  ∀ m < n,
    ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
      LiftRel (LiftRel R) S T →
        ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a m → ∃ b ∈ T.join.destruct, LiftRelO R U a b
⊢ ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
    LiftRel (LiftRel R) S T →
      ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a n → ∃ b ∈ T.join.destruct, LiftRelO R U a b
Module: Mathlib.Data.WSeq.Basic

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

Tactic:
induction s using WSeq.recOn

Goal state after:
case h1.nil
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
S : WSeq (WSeq α)
ej : nil.append S.join = cons b ss
m : a ∈ nil.append S.join
⊢ a ∈ nil ∨ ∃ s ∈ S, a ∈ s

case h1.cons
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
S : WSeq (WSeq α)
x✝ : α
s✝ : WSeq α
ej : (cons x✝ s✝).append S.join = cons b ss
m : a ∈ (cons x✝ s✝).append S.join
⊢ a ∈ cons x✝ s✝ ∨ ∃ s ∈ S, a ∈ s

case h1.think
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
S : WSeq (WSeq α)
s✝ : WSeq α
ej : s✝.think.append S.join = cons b ss
m : a ∈ s✝.think.append S.join
⊢ a ∈ s✝.think ∨ ∃ s ∈ S, a ∈ s
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
U : WSeq α → WSeq β → Prop
HU :
  ∀ (s1 : WSeq α) (s2 : WSeq β),
    (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) → U s1 s2
n : ℕ
IH :
  ∀ m < n,
    ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
      LiftRel (LiftRel R) S T →
        ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a m → ∃ b ∈ T.join.destruct, LiftRelO R U a b
S : WSeq (WSeq α)
T : WSeq (WSeq β)
ST : LiftRel (LiftRel R) S T
a : Option (α × WSeq α)
ra : (S.destruct.bind destruct_join.aux).Results a n
o : Option (WSeq α × WSeq (WSeq α))
m k : ℕ
rs1 : S.destruct.Results o m
rs2✝ : (destruct_join.aux o).Results a k
en : n = k + m
p : Option (WSeq β × WSeq (WSeq β))
mT✝ : p ∈ T.destruct
rop : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) o p
x✝¹ : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) none none
x✝ : S.destruct.Results none m
rs2 : (destruct_join.aux none).Results a k
mT : none ∈ T.destruct
⊢ LiftRelO R U a none

Tactic:
eq_of_pure_mem rs2.mem

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
U : WSeq α → WSeq β → Prop
HU :
  ∀ (s1 : WSeq α) (s2 : WSeq β),
    (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) → U s1 s2
n : ℕ
IH :
  ∀ m < n,
    ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
      LiftRel (LiftRel R) S T →
        ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a m → ∃ b ∈ T.join.destruct, LiftRelO R U a b
S : WSeq (WSeq α)
T : WSeq (WSeq β)
ST : LiftRel (LiftRel R) S T
a : Option (α × WSeq α)
ra : (S.destruct.bind destruct_join.aux).Results a n
o : Option (WSeq α × WSeq (WSeq α))
m k : ℕ
rs1 : S.destruct.Results o m
rs2✝ : (destruct_join.aux o).Results a k
en : n = k + m
p : Option (WSeq β × WSeq (WSeq β))
mT✝ : p ∈ T.destruct
rop : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) o p
x✝¹ : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) none none
x✝ : S.destruct.Results none m
rs2 : (destruct_join.aux none).Results a k
mT : none ∈ T.destruct
⊢ LiftRelO R U none none
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h2
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
s : WSeq α
S : WSeq (WSeq α)
ej : s.append S.join = ss.think
m : a ∈ s.append S.join
⊢ a ∈ s ∨ ∃ s ∈ S, a ∈ s

Tactic:
induction s using WSeq.recOn

Goal state after:
case h2.nil
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
S : WSeq (WSeq α)
ej : nil.append S.join = ss.think
m : a ∈ nil.append S.join
⊢ a ∈ nil ∨ ∃ s ∈ S, a ∈ s

case h2.cons
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
S : WSeq (WSeq α)
x✝ : α
s✝ : WSeq α
ej : (cons x✝ s✝).append S.join = ss.think
m : a ∈ (cons x✝ s✝).append S.join
⊢ a ∈ cons x✝ s✝ ∨ ∃ s ∈ S, a ∈ s

case h2.think
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
S : WSeq (WSeq α)
s✝ : WSeq α
ej : s✝.think.append S.join = ss.think
m : a ∈ s✝.think.append S.join
⊢ a ∈ s✝.think ∨ ∃ s ∈ S, a ∈ s
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case bisim
α : Type u
β : Type v
f : α → β
s✝ : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
s : WSeq α
h : c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct
⊢ BisimO (fun c1 c2 ↦ ∃ s, c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    (map f s).destruct.destruct (Computation.map (Option.map (Prod.map f (map f))) s.destruct).destruct

Tactic:
induction s using WSeq.recOn

Goal state after:
case bisim.nil
α : Type u
β : Type v
f : α → β
s : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
h : c1 = (map f nil).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) nil.destruct
⊢ BisimO (fun c1 c2 ↦ ∃ s, c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    (map f nil).destruct.destruct (Computation.map (Option.map (Prod.map f (map f))) nil.destruct).destruct

case bisim.cons
α : Type u
β : Type v
f : α → β
s : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
x✝ : α
s✝ : WSeq α
h : c1 = (map f (cons x✝ s✝)).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (cons x✝ s✝).destruct
⊢ BisimO (fun c1 c2 ↦ ∃ s, c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    (map f (cons x✝ s✝)).destruct.destruct
    (Computation.map (Option.map (Prod.map f (map f))) (cons x✝ s✝).destruct).destruct

case bisim.think
α : Type u
β : Type v
f : α → β
s : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
s✝ : WSeq α
h : c1 = (map f s✝.think).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s✝.think.destruct
⊢ BisimO (fun c1 c2 ↦ ∃ s, c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    (map f s✝.think).destruct.destruct (Computation.map (Option.map (Prod.map f (map f))) s✝.think.destruct).destruct
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case cons.cons
head✝¹ : Char
tail✝¹ : List Char
tail_ih✝ : ∀ (s₂ : List Char), ltb { s := ofList tail✝¹, i := 0 } { s := ofList s₂, i := 0 } = true ↔ tail✝¹ < s₂
head✝ : Char
tail✝ : List Char
⊢ ltb { s := ofList (head✝¹ :: tail✝¹), i := 0 } { s := ofList (head✝ :: tail✝), i := 0 } = true ↔
    head✝¹ :: tail✝¹ < head✝ :: tail✝

Tactic:
rename_i c₁ cs₁ ih c₂ cs₂; unfold ltb
    simp only [Legacy.Iterator.hasNext, Pos.Raw.byteIdx_zero, rawEndPos_ofList, utf8Len_cons,
      add_pos_iff, Char.utf8Size_pos, or_true, decide_true, ↓reduceIte, Legacy.Iterator.curr,
      Pos.Raw.get, String.toList_ofList, Pos.Raw.utf8GetAux, Legacy.Iterator.next, Pos.Raw.next,
      Bool.ite_eq_true_distrib, decide_eq_true_eq]
    split_ifs with h
    · subst c₂
      suffices ltb ⟨ofList (c₁ :: cs₁), (0 : Pos.Raw) + c₁⟩
          ⟨ofList (c₁ :: cs₂), (0 : Pos.Raw) + c₁⟩ =
            ltb ⟨ofList cs₁, 0⟩ ⟨ofList cs₂, 0⟩ by
        rw [this]; exact (ih cs₂).trans List.lex_cons_iff.symm
      apply ltb_cons_addChar
    · refine ⟨List.Lex.rel, fun e ↦ ?_⟩
      cases e <;> rename_i h'
      · assumption
      · contradiction

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

Goal state before:
pp: α : Type u
s✝ t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
s t : WSeq α
h : c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)
⊢ BisimO (fun c1 c2 ↦ ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (s.append t).destruct.destruct (s.destruct.bind (destruct_append.aux t)).destruct

Tactic:
induction s using WSeq.recOn

Goal state after:
case nil
α : Type u
s t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
t : WSeq α
h : c1 = (nil.append t).destruct ∧ c2 = nil.destruct.bind (destruct_append.aux t)
⊢ BisimO (fun c1 c2 ↦ ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (nil.append t).destruct.destruct (nil.destruct.bind (destruct_append.aux t)).destruct

case cons
α : Type u
s t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
t : WSeq α
x✝ : α
s✝ : WSeq α
h : c1 = ((cons x✝ s✝).append t).destruct ∧ c2 = (cons x✝ s✝).destruct.bind (destruct_append.aux t)
⊢ BisimO (fun c1 c2 ↦ ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    ((cons x✝ s✝).append t).destruct.destruct ((cons x✝ s✝).destruct.bind (destruct_append.aux t)).destruct

case think
α : Type u
s t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
t s✝ : WSeq α
h : c1 = (s✝.think.append t).destruct ∧ c2 = s✝.think.destruct.bind (destruct_append.aux t)
⊢ BisimO (fun c1 c2 ↦ ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (s✝.think.append t).destruct.destruct (s✝.think.destruct.bind (destruct_append.aux t)).destruct
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case bisim
α : Type u
β : Type v
f : α → β
S✝ : WSeq (WSeq α)
s : WSeq β
S : WSeq (WSeq α)
⊢ Seq.BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join)
    (Seq.destruct (s.append (map f S.join))) (Seq.destruct (s.append (map (map f) S).join))

Tactic:
induction s using WSeq.recOn

Goal state after:
case bisim.nil
α : Type u
β : Type v
f : α → β
S✝ S : WSeq (WSeq α)
⊢ Seq.BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join)
    (Seq.destruct (nil.append (map f S.join))) (Seq.destruct (nil.append (map (map f) S).join))

case bisim.cons
α : Type u
β : Type v
f : α → β
S✝ S : WSeq (WSeq α)
x✝ : β
s✝ : WSeq β
⊢ Seq.BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join)
    (Seq.destruct ((cons x✝ s✝).append (map f S.join))) (Seq.destruct ((cons x✝ s✝).append (map (map f) S).join))

case bisim.think
α : Type u
β : Type v
f : α → β
S✝ S : WSeq (WSeq α)
s✝ : WSeq β
⊢ Seq.BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join)
    (Seq.destruct (s✝.think.append (map f S.join))) (Seq.destruct (s✝.think.append (map (map f) S).join))
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
s✝¹ s' s✝ : WSeq α
h : (map ret s✝).join = s'
c1 c2 : Computation (Option (α × WSeq α))
s : WSeq α
this : ∀ (s : WSeq α), ∃ s', (map ret s).join.destruct = (map ret s').join.destruct ∧ s.destruct = s'.destruct
⊢ LiftRelAux (LiftRelO Eq fun s1 s2 ↦ (map ret s2).join = s1)
    (fun c1 c2 ↦ ∃ s, c1 = (map ret s).join.destruct ∧ c2 = s.destruct) (map ret s).join.destruct.destruct
    s.destruct.destruct

Tactic:
induction s using WSeq.recOn

Goal state after:
case nil
α : Type u
s✝ s' s : WSeq α
h : (map ret s).join = s'
c1 c2 : Computation (Option (α × WSeq α))
this : ∀ (s : WSeq α), ∃ s', (map ret s).join.destruct = (map ret s').join.destruct ∧ s.destruct = s'.destruct
⊢ LiftRelAux (LiftRelO Eq fun s1 s2 ↦ (map ret s2).join = s1)
    (fun c1 c2 ↦ ∃ s, c1 = (map ret s).join.destruct ∧ c2 = s.destruct) (map ret nil).join.destruct.destruct
    nil.destruct.destruct

case cons
α : Type u
s✝¹ s' s : WSeq α
h : (map ret s).join = s'
c1 c2 : Computation (Option (α × WSeq α))
this : ∀ (s : WSeq α), ∃ s', (map ret s).join.destruct = (map ret s').join.destruct ∧ s.destruct = s'.destruct
x✝ : α
s✝ : WSeq α
⊢ LiftRelAux (LiftRelO Eq fun s1 s2 ↦ (map ret s2).join = s1)
    (fun c1 c2 ↦ ∃ s, c1 = (map ret s).join.destruct ∧ c2 = s.destruct) (map ret (cons x✝ s✝)).join.destruct.destruct
    (cons x✝ s✝).destruct.destruct

case think
α : Type u
s✝¹ s' s : WSeq α
h : (map ret s).join = s'
c1 c2 : Computation (Option (α × WSeq α))
this : ∀ (s : WSeq α), ∃ s', (map ret s).join.destruct = (map ret s').join.destruct ∧ s.destruct = s'.destruct
s✝ : WSeq α
⊢ LiftRelAux (LiftRelO Eq fun s1 s2 ↦ (map ret s2).join = s1)
    (fun c1 c2 ↦ ∃ s, c1 = (map ret s).join.destruct ∧ c2 = s.destruct) (map ret s✝.think).join.destruct.destruct
    s✝.think.destruct.destruct
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
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
⊢ 1⁻¹ = 1

Tactic:
inv_one

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
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
⊢ 1 = 1
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: x : ℝ
n : ℤ
⊢ translate (Multiplicative.ofAdd x) ^ n = translate (Multiplicative.ofAdd (↑n * x))

Tactic:
by
  simp only [← zsmul_eq_mul, ofAdd_zsmul, map_zpow]

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

Goal state before:
pp: f : CircleDeg1Lift
⊢ Tendsto (fun n ↦ (f ^ (n + 1)) 0 / (↑n + 1)) atTop (𝓝 (τ f))

Tactic:
refine
    tendsto_iff_dist_tendsto_zero.2 <|
      squeeze_zero (fun _ => dist_nonneg) (fun n => ?_)
        ((tendsto_const_div_atTop_nhds_zero_nat 1).comp (tendsto_add_atTop_nat 1))
  dsimp
  have : (0 : ℝ) < n + 1 := n.cast_add_one_pos
  rw [Real.dist_eq, div_sub' (ne_of_gt this), abs_div, ← Real.dist_eq, abs_of_pos this,
    Nat.cast_add_one, div_le_div_iff_of_pos_right this, ← Nat.cast_add_one]
  apply dist_pow_map_zero_mul_translationNumber_le

Goal state after:
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)
⊢ ∃ F, ∀ (g : G), Semiconj ⇑F ⇑(f₁ g) ⇑(f₂ g)

Tactic:
by
  -- Equality of translation number guarantees that for each `x`
  -- the set `{f₂ g⁻¹ (f₁ g x) | g : G}` is bounded above.
  have : ∀ x, BddAbove (range fun g => f₂ g⁻¹ (f₁ g x)) := by
    refine fun x => ⟨x + 2, ?_⟩
    rintro _ ⟨g, rfl⟩
    have : τ (f₂ g⁻¹) = -τ (f₂ g) := by
      rw [← MonoidHom.coe_toHomUnits, map_inv, translationNumber_units_inv,
        MonoidHom.coe_toHomUnits]
    calc
      f₂ g⁻¹ (f₁ g x) ≤ f₂ g⁻¹ (x + τ (f₁ g) + 1) :=
        mono _ (map_lt_add_translationNumber_add_one _ _).le
      _ = f₂ g⁻¹ (x + τ (f₂ g)) + 1 := by rw [h, map_add_one]
      _ ≤ x + τ (f₂ g) + τ (f₂ g⁻¹) + 1 + 1 := by grw [map_lt_add_translationNumber_add_one]
      _ = x + 2 := by simp [this, add_assoc, one_add_one_eq_two]
  -- We have a theorem about actions by `OrderIso`, so we introduce auxiliary maps
  -- to `ℝ ≃o ℝ`.
  set F₁ := toOrderIso.comp f₁.toHomUnits
  set F₂ := toOrderIso.comp f₂.toHomUnits
  have hF₁ : ∀ g, ⇑(F₁ g) = f₁ g := fun _ => rfl
  have hF₂ : ∀ g, ⇑(F₂ g) = f₂ g := fun _ => rfl
  -- Now we apply `csSup_div_semiconj` and go back to `f₁` and `f₂`.
  refine ⟨⟨⟨fun x ↦ ⨆ g', (F₂ g')⁻¹ (F₁ g' x), fun x y hxy => ?_⟩, fun x => ?_⟩,
    csSup_div_semiconj F₂ F₁ fun x => ?_⟩ <;> simp only [hF₁, hF₂, ← map_inv]
  · exact ciSup_mono (this y) fun g => mono _ (mono _ hxy)
  · simp only [map_add_one]
    exact (Monotone.map_ciSup_of_continuousAt (by fun_prop)
      (monotone_id.add_const (1 : ℝ)) (this x)).symm
  · exact this x

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

Goal state before:
pp: 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
⊢ μ s = 0 ∨ μ s = ENNReal.ofReal T

Tactic:
rcases eq_or_ne (μ s) 0 with h | h

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

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

Goal state before:
pp: case inr
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
this : (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν ∘ f =ᵐ[ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
hμν : ¬μ ≪ ν
⊢ μ.rnDeriv ν ∘ f =ᵐ[ν] μ.rnDeriv ν

Tactic:
refine .trans (.trans ?_ this) (rnDeriv_withDensity ν (measurable_rnDeriv μ ν))

Goal state after:
case inr
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
this : (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν ∘ f =ᵐ[ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
hμν : ¬μ ≪ ν
⊢ μ.rnDeriv ν ∘ f =ᵐ[ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν ∘ f
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h : μ ≪ ν
this : μ.singularPart ν = 0
⊢ ν.withDensity (μ.rnDeriv ν) = μ

Tactic:
conv_rhs => rw [haveLebesgueDecomposition_add μ ν, this, zero_add]

Goal state after:
Module: Mathlib.Dynamics.FixedPoints.Support

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ HasCompactFixedSupport id

Tactic:
by
  simp [HasCompactFixedSupport, fixedSupport]

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

Goal state before:
pp: A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
p : Pattern A G
v h : G
hmem : h ∉ Finset.image (fun x ↦ v * x) p.support
⊢ A

Tactic:
exact default

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

Goal state before:
pp: A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Inhabited A
G : Type u_2
inst✝² : Monoid G
inst✝¹ : IsLeftCancelMul G
inst✝ : DiscreteTopology A
F : Set (Pattern A G)
⊢ IsClosed[Pi.topologicalSpace] (mulForbidden F)

Tactic:
rw [mulForbidden]

Goal state after:
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Inhabited A
G : Type u_2
inst✝² : Monoid G
inst✝¹ : IsLeftCancelMul G
inst✝ : DiscreteTopology A
F : Set (Pattern A G)
⊢ IsClosed[Pi.topologicalSpace] {x | ∀ p ∈ F, ∀ (g : G), ¬p.mulOccursInAt x g}
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
⊢ ∃ u ∈ f, closure[inst✝] (image2 ϕ u s) ⊆ n

Tactic:
let k := closure (image2 ϕ v s)

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)
⊢ ∃ u ∈ f, closure[inst✝] (image2 ϕ u s) ⊆ n
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
⊢ (ν.restrict tᶜ).withDensity (μ.rnDeriv (ν + ν')) = (ν.restrict tᶜ).withDensity (μ.rnDeriv ν)

Tactic:
have : (ν.restrict tᶜ).withDensity (μ.rnDeriv (ν + ν'))
      = ((ν + ν').restrict tᶜ).withDensity (μ.rnDeriv (ν + ν')) := by simp [t]

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

Goal state before:
pp: case inr.inr.refine_2
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
dyncover : (Fin n → ↥s) → X
h_dyncover :
  ∀ (t : Fin n → ↥s),
    ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
⊢ #sn.toFinset ≤ #s ^ n

Tactic:
toFinset_card

Goal state after:
case inr.inr.refine_2
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
dyncover : (Fin n → ↥s) → X
h_dyncover :
  ∀ (t : Fin n → ↥s),
    ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
⊢ Fintype.card ↑sn ≤ #s ^ n
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: case inr.inr.inr
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst✝ : U.IsSymm
m n : ℕ
F_nonempty : F.Nonempty
hn : n ≠ 0
h : coverMincard T F U m < ⊤
s : Finset X
s_cover : IsDynCoverOf T F U m ↑s
s_coverMincard : ↑(#s) = coverMincard T F U m
t : Finset X
t_cover : IsDynCoverOf T F (U ○ U) (m * n) ↑t
t_sn : #t ≤ #s ^ n
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n

Tactic:
rw [← s_coverMincard]

Goal state after:
case inr.inr.inr
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst✝ : U.IsSymm
m n : ℕ
F_nonempty : F.Nonempty
hn : n ≠ 0
h : coverMincard T F U m < ⊤
s : Finset X
s_cover : IsDynCoverOf T F U m ↑s
s_coverMincard : ↑(#s) = coverMincard T F U m
t : Finset X
t_cover : IsDynCoverOf T F (U ○ U) (m * n) ↑t
t_sn : #t ≤ #s ^ n
⊢ coverMincard T F (U ○ U) (m * n) ≤ ↑(#s) ^ n