mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case right.right.right.right.left
a b : ℕ+
d : ℕ+ := ⋯
w : ℕ+ := ⋯
x : ℕ := ⋯
y : ℕ := ⋯
z : ℕ+ := ⋯
a' : ℕ+ := ⋯
b' : ℕ+ := ⋯
u : XgcdType := ⋯
ur : XgcdType := ⋯
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ w * b' = (y * ↑a').succPNat

Tactic:
apply eq
    rw [succPNat_coe, Nat.succ_eq_add_one, mul_coe, hwb']

Goal state after:
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: a b : ℕ+
left✝² : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left✝¹ : a.gcdZ b * a.gcdA' b = (a.gcdX b * ↑(a.gcdB' b)).succPNat
left✝ : a.gcdW b * a.gcdB' b = (a.gcdY b * ↑(a.gcdA' b)).succPNat
h₅ : ↑(a.gcdZ b) * ↑a = a.gcdX b * ↑b + ↑(a.gcdD b)
right✝ : ↑(a.gcdW b) * ↑b = a.gcdY b * ↑a + ↑(a.gcdD b)
⊢ a.gcdD b = a.gcd b

Tactic:
apply dvd_antisymm

Goal state after:
case a
a b : ℕ+
left✝² : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left✝¹ : a.gcdZ b * a.gcdA' b = (a.gcdX b * ↑(a.gcdB' b)).succPNat
left✝ : a.gcdW b * a.gcdB' b = (a.gcdY b * ↑(a.gcdA' b)).succPNat
h₅ : ↑(a.gcdZ b) * ↑a = a.gcdX b * ↑b + ↑(a.gcdD b)
right✝ : ↑(a.gcdW b) * ↑b = a.gcdY b * ↑a + ↑(a.gcdD b)
⊢ a.gcdD b ∣ a.gcd b

case a
a b : ℕ+
left✝² : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left✝¹ : a.gcdZ b * a.gcdA' b = (a.gcdX b * ↑(a.gcdB' b)).succPNat
left✝ : a.gcdW b * a.gcdB' b = (a.gcdY b * ↑(a.gcdA' b)).succPNat
h₅ : ↑(a.gcdZ b) * ↑a = a.gcdX b * ↑b + ↑(a.gcdD b)
right✝ : ↑(a.gcdW b) * ↑b = a.gcdY b * ↑a + ↑(a.gcdD b)
⊢ a.gcd b ∣ a.gcdD b
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
t_ih_l :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ l✝ a₂ → Valid' (Option.map f a₁) (map f l✝) (Option.map f a₂) ∧ (map f l✝).size = l✝.size
t_ih_r :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ r✝ a₂ → Valid' (Option.map f a₁) (map f r✝) (Option.map f a₂) ∧ (map f r✝).size = r✝.size
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
⊢ Valid' (Option.map f a₁) (map f (Ordnode.node size✝ l✝ x✝ r✝)) (Option.map f a₂) ∧
    (map f (Ordnode.node size✝ l✝ x✝ r✝)).size = (Ordnode.node size✝ l✝ x✝ r✝).size

Tactic:
| node _ _ _ _ t_ih_l t_ih_r =>

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

Goal state before:
pp: case a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
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), WEquiv (wrepr (f i)) (f i)
⊢ WEquiv ((P F).wMk' ((TypeVec.id ::: wrepr) <$$> ⟨a, (P F).appendContents f' f⟩)) ((P F).wMk a f' f)

Tactic:
q.P.map_eq,

Goal state after:
case a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
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), WEquiv (wrepr (f i)) (f i)
⊢ WEquiv ((P F).wMk' ⟨a, (TypeVec.id ::: wrepr) ⊚ (P F).appendContents f' f⟩) ((P F).wMk a f' f)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
a : (P F).A
f : (P F).B a → α
xeq : x = abs ⟨a, f⟩
h' : ∀ (i : (P F).B a), f i ∈ supp x
a' : (P F).A
f' : (P F).B a' → α
h'' : abs ⟨a', f'⟩ = x
u : α
i : (P F).B a
left✝ : i ∈ univ
hfi : f i = u
this : u ∈ supp x
⊢ u ∈ f' '' univ

Tactic:
exact (mem_supp x u).mp this _ _ h''

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

Goal state before:
pp: α : Type u
s : WSeq α
a : α
h : some a ∈ Computation.map (fun x ↦ Prod.fst <$> x) s.tail.destruct
⊢ ∃ a', some a' ∈ s.head

Tactic:
rcases Computation.exists_of_mem_map h with ⟨o, md, e⟩

Goal state after:
α : Type u
s : WSeq α
a : α
h : some a ∈ Computation.map (fun x ↦ Prod.fst <$> x) s.tail.destruct
o : Option (α × WSeq α)
md : o ∈ s.tail.destruct
e : Prod.fst <$> o = some a
⊢ ∃ a', some a' ∈ s.head
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some.none
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
a : α × WSeq α
dsm : some a ∈ s.destruct
dse : Prod.fst <$> some a = o
dtm : none ∈ t.destruct
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some a) none
⊢ Prod.fst <$> some a ∈ t.head

Tactic:
cases a
    cases dst

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

Goal state before:
pp: case inr.inl
α : 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)
a : α
h : parallel.aux2 l = Sum.inl a
C : corec parallel.aux1 (l, S) = pure a
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
C

Goal state after:
case inr.inl
α : 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)
a : α
h : parallel.aux2 l = Sum.inl a
C : corec parallel.aux1 (l, S) = pure a
⊢ (pure a).Terminates
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inr.inr
α : 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'
C :
  corec parallel.aux1 (l, S) =
    (corec parallel.aux1
        (match some (some c, S.tail) with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))).think
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
C

Goal state after:
case inr.inr
α : 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'
C :
  corec parallel.aux1 (l, S) =
    (corec parallel.aux1
        (match some (some c, S.tail) with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))).think
⊢ (corec parallel.aux1
        (match some (some c, S.tail) with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))).think.Terminates
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inr.inl
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
n : ℕ
IH :
  ∀ (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
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a✝ : some (some c) = S.get? (n + 1)
a : α
h : parallel.aux2 l = Sum.inl a
C : corec parallel.aux1 (l, S) = pure a
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
C

Goal state after:
case inr.inl
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
n : ℕ
IH :
  ∀ (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
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a✝ : some (some c) = S.get? (n + 1)
a : α
h : parallel.aux2 l = Sum.inl a
C : corec parallel.aux1 (l, S) = pure a
⊢ (pure a).Terminates
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inr.inr
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
n : ℕ
IH :
  ∀ (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
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? (n + 1)
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    (corec parallel.aux1
        (match S.destruct with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))).think
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
C

Goal state after:
case inr.inr
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
n : ℕ
IH :
  ∀ (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
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? (n + 1)
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    (corec parallel.aux1
        (match S.destruct with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))).think
⊢ (corec parallel.aux1
        (match S.destruct with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))).think.Terminates
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inr.inr.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
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
e : d = c'
⊢ ∃ c_1 ∈ c :: l, a' ∈ c_1

Tactic:
rw [e] at ad

Goal state after:
case inr.inr.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
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' ∈ c'
e : d = c'
⊢ ∃ c_1 ∈ c :: l, a' ∈ c_1
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderTop ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderTop (α ⊤)
x✝ : Σₗ (i : ι), α i
a : ι
b : α a
⊢ ⟨a, b⟩ ≤ ⟨⊤, ⊤⟩

Tactic:
by
    obtain rfl | ha := eq_top_or_lt_top a
    · exact Lex.right _ _ le_top
    · exact Lex.left _ _ ha

Goal state after:
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: case left
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨j, b⟩

Tactic:
obtain ⟨c, ha⟩ := exists_gt a

Goal state after:
case left
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
c : α i
ha : a < c
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨j, b⟩
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₁ : γ₁
⊢ ((∃ a₁ b₁ c₁_1, a = inl a₁ ∧ b = inl b₁ ∧ inl c₁ = inl c₁_1 ∧ c₁_1 ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ inl c₁ = inr c₂ ∧ c₂ ∈ g a₂ b₂) ↔
    ∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ c₁ ∈ f a₁ b₁

Tactic:
or_iff_left

Goal state after:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₁ : γ₁
⊢ (∃ a₁ b₁ c₁_1, a = inl a₁ ∧ b = inl b₁ ∧ inl c₁ = inl c₁_1 ∧ c₁_1 ∈ f a₁ b₁) ↔
    ∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ c₁ ∈ f a₁ b₁

α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₁ : γ₁
⊢ ¬∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ inl c₁ = inr c₂ ∧ c₂ ∈ g a₂ b₂
Module: Mathlib.Dynamics.FixedPoints.Prufer

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

Tactic:
rwa [iterate_map_mul, hg', one_mul]

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

Goal state before:
pp: f : CircleDeg1Lift
n : ℕ
⊢ Function.Commute ⇑f fun x ↦ x - ↑n

Tactic:
simpa only [sub_eq_add_neg] using!
    (f.commute_add_nat n).inverses_right (Equiv.addRight _).right_inv (Equiv.addRight _).left_inv

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

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
m : ℤ
h : f x = x + ↑m
n : ℕ
⊢ (⇑f)^[n] x = x + ↑n * ↑m

Tactic:
by
  simpa only [nsmul_eq_mul, add_right_iterate] using (f.commute_add_int m).iterate_eq_of_map_eq n h

Goal state after:
Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
s : Set Y
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
this✝ : ν.InnerRegularCompactLTTop
ε : ℝ≥0∞
hε : ε > 0
this :
  ∀ {s : Set Y},
    NullMeasurableSet s ν → ν s ≠ ∞ → ∀ ε > 0, IsOpen[inst✝⁵] s → ∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε
hso : ¬IsOpen[inst✝⁵] s
H : 0 < ε / 3
U : Set Y
hUo : IsOpen[inst✝⁵] U
hU : ν U < ∞
hmU : NullMeasurableSet U ν
hUs : ν (U ∆ s) ≤ ε / 3
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : μ ((⇑(f a) ⁻¹' U) ∆ (⇑g ⁻¹' U)) ≤ ε / 3
⊢ μ ((⇑(f a) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤
    μ ((⇑(f a) ⁻¹' s) ∆ (⇑(f a) ⁻¹' U)) + μ ((⇑(f a) ⁻¹' U) ∆ (⇑g ⁻¹' U)) + μ ((⇑g ⁻¹' U) ∆ (⇑g ⁻¹' s))

Tactic:
refine (measure_symmDiff_le _ (g ⁻¹' U) _).trans ?_

Goal state after:
α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
s : Set Y
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
this✝ : ν.InnerRegularCompactLTTop
ε : ℝ≥0∞
hε : ε > 0
this :
  ∀ {s : Set Y},
    NullMeasurableSet s ν → ν s ≠ ∞ → ∀ ε > 0, IsOpen[inst✝⁵] s → ∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε
hso : ¬IsOpen[inst✝⁵] s
H : 0 < ε / 3
U : Set Y
hUo : IsOpen[inst✝⁵] U
hU : ν U < ∞
hmU : NullMeasurableSet U ν
hUs : ν (U ∆ s) ≤ ε / 3
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : μ ((⇑(f a) ⁻¹' U) ∆ (⇑g ⁻¹' U)) ≤ ε / 3
⊢ μ ((⇑(f a) ⁻¹' s) ∆ (⇑g ⁻¹' U)) + μ ((⇑g ⁻¹' U) ∆ (⇑g ⁻¹' s)) ≤
    μ ((⇑(f a) ⁻¹' s) ∆ (⇑(f a) ⁻¹' U)) + μ ((⇑(f a) ⁻¹' U) ∆ (⇑g ⁻¹' U)) + μ ((⇑g ⁻¹' U) ∆ (⇑g ⁻¹' s))
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
⊢ f x < x + ↑⌊τ f⌋ + 1

Tactic:
add_assoc

Goal state after:
f : CircleDeg1Lift
x : ℝ
⊢ f x < x + (↑⌊τ f⌋ + 1)
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

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

Tactic:
rcases (AddSubgroup.dense_or_cyclic _).resolve_left h with ⟨c, hc⟩

Goal state after:
case inr.mpr
a b : ℝ
hb : b ≠ 0
h : ¬Dense ↑(AddSubgroup.closure {a, b})
c : ℝ
hc : AddSubgroup.closure {a, b} = AddSubgroup.closure {c}
⊢ ¬Irrational (a / b)
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: a p : ℝ
⊢ Dense ↑(AddSubgroup.closure {a} ⊔ AddSubgroup.closure {p}) ↔ Dense ↑(AddSubgroup.closure {a, p})

Tactic:
← AddSubgroup.closure_union,

Goal state after:
a p : ℝ
⊢ Dense ↑(AddSubgroup.closure ({a} ∪ {p})) ↔ Dense ↑(AddSubgroup.closure {a, p})
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: 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
⊢ g +ᵥ B = g +ᵥ thickening (T / (2 * ↑n)) {x}

Tactic:
thickening_singleton

Goal state after:
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
⊢ g +ᵥ B = g +ᵥ ball x (T / (2 * ↑n))
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : μ s ≠ 0
⊢ ∃ᶠ (m : ℕ) in atTop, μ (s ∩ f^[m] ⁻¹' s) ≠ 0

Tactic:
by
  set t : ℕ → Set α := fun n ↦ s ∩ f^[n] ⁻¹' s
  -- Assume that `μ (t n) ≠ 0`, where `t n = s ∩ f^[n] ⁻¹' s`, only for finitely many `n`.
  by_contra H
  -- Let `N` be the maximal `n` such that `μ (t n) ≠ 0`.
  obtain ⟨N, hN, hmax⟩ : ∃ N, μ (t N) ≠ 0 ∧ ∀ n > N, μ (t n) = 0 := by
    rw [Nat.frequently_atTop_iff_infinite, not_infinite] at H
    convert! exists_max_image _ (·) H ⟨0, by simpa⟩ using 4
    rw [gt_iff_lt, ← not_le, not_imp_comm, mem_ofPred]
  have htm {n : ℕ} : NullMeasurableSet (t n) μ :=
    hs.inter <| hs.preimage <| hf.toQuasiMeasurePreserving.iterate n
  -- Then all `t n`, `n > N`, are null sets, hence `T = t N \ ⋃ n > N, t n` has positive measure.
  set T := t N \ ⋃ n > N, t n with hT
  have hμT : μ T ≠ 0 := by
    rwa [hT, measure_sdiff_null]
    exact (measure_biUnion_null_iff {n | N < n}.to_countable).2 hmax
  have hTm : NullMeasurableSet T μ := htm.diff <| .biUnion {n | N < n}.to_countable fun _ _ ↦ htm
  -- Take `x ∈ T` and `m ≠ 0` such that `f^[m] x ∈ T`.
  rcases hf.exists_mem_iterate_mem hTm hμT with ⟨x, hxt, m, hm₀, hmt⟩
  -- Then `N + m > N`, `x ∈ s`, and `f^[N + m] x = f^[N] (f^[m] x) ∈ s`.
  -- This contradicts `x ∈ T ⊆ (⋃ n > N, t n)ᶜ`.
  refine hxt.2 <| mem_iUnion₂.2 ⟨N + m, ?_, hxt.1.1, ?_⟩
  · simpa [pos_iff_ne_zero]
  · simpa only [iterate_add] using! hmt.1.2

Goal state after:
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 : ℕ) in atTop, f^[n] x ∈ s
⊢ ∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[n + 1]^[m] x ∈ s

Tactic:
Nat.frequently_atTop_iff_infinite

Goal state after:
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
⊢ ∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[n + 1]^[m] x ∈ s
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
⊢ Ergodic (fun y ↦ n • y + x) volume

Tactic:
by
  set f : AddCircle T → AddCircle T := fun y => n • y + x
  let e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x <| n - 1)
  have he : MeasurePreserving e volume volume :=
    measurePreserving_add_left volume (DivisibleBy.div x <| n - 1)
  suffices e ∘ f ∘ e.symm = fun y => n • y by
    rw [← he.ergodic_conjugate_iff, this]; exact ergodic_zsmul h
  replace h : n - 1 ≠ 0 := by
    rw [← abs_one] at h; rw [sub_ne_zero]; exact ne_of_apply_ne _ (ne_of_gt h)
  have hnx : n • DivisibleBy.div x (n - 1) = x + DivisibleBy.div x (n - 1) := by
    conv_rhs => congr; rw [← DivisibleBy.div_cancel x h]
    rw [sub_smul, one_smul, sub_add_cancel]
  ext y
  simp only [f, e, hnx, MeasurableEquiv.coe_addLeft, MeasurableEquiv.symm_addLeft, comp_apply,
    smul_add, zsmul_neg', neg_smul, neg_add_rev]
  abel

Goal state after:
Module: Mathlib.Topology.Order.CountableSeparating

Goal state before:
pp: case inl
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s✝ s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x | ∃ y, y ⋖ x}
x y : X
h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s
hne : x ≠ y
hlt : x < y
he : Ioo x y = ∅
⊢ False

Tactic:
specialize h (Iio y) (mem_image_of_mem _ (.inr ⟨x, hlt, by simpa using Set.ext_iff.mp he⟩))
      simp [hlt.not_ge] at h

Goal state after:
Module: Mathlib.Topology.Order.CountableSeparating

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s : Set X
⊢ HasCountableSeparatingOn X (fun x ↦ x ∈ range Iio) s

Tactic:
by
  constructor
  rcases TopologicalSpace.exists_countable_dense X with ⟨s, hsc, hsd⟩
  set t := s ∪ {x | ∃ y, y ⋖ x}
  refine ⟨Iio '' t, .image ?_ _, ?_, ?_⟩
  · exact hsc.union countable_setOfPred_covBy_left
  · exact image_subset_range _ _
  · rintro x - y - h
    by_contra! hne
    wlog hlt : x < y generalizing x y
    · refine this y x ?_ hne.symm (hne.lt_or_gt.resolve_left hlt)
      simpa only [iff_comm] using h
    cases (Ioo x y).eq_empty_or_nonempty with
    | inl he =>
      specialize h (Iio y) (mem_image_of_mem _ (.inr ⟨x, hlt, by simpa using Set.ext_iff.mp he⟩))
      simp [hlt.not_ge] at h
    | inr hne =>
      rcases hsd.inter_open_nonempty _ isOpen_Ioo hne with ⟨z, ⟨hxz, hzy⟩, hzs⟩
      simpa [hxz, hzy.not_gt] using h (Iio z) (mem_image_of_mem _ (.inl hzs))

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
  fun_prop

Goal state after: