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

Goal state before:
pp: a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
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
⊢ ↑w * ↑b' = y * ↑a' + 1

Tactic:
rw [ha', hb', mul_add, mul_add, hdet']

Goal state after:
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
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
⊢ ↑w * y + (x * y + 1) = y * ↑w + y * x + 1
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
⊢ SuppPreservation ↔ LiftPPreservation

Tactic:
constructor <;> intro h

Goal state after:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation
⊢ LiftPPreservation

case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : LiftPPreservation
⊢ SuppPreservation
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case sz.left
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : (map f l✝).size = l✝.size
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : (map f r✝).size = r✝.size
⊢ size✝ = l✝.size + r✝.size + 1

Tactic:
exact h.sz.1

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
x y : (P F).W α
h : abs ((P F).wDest' x) = abs ((P F).wDest' y)
⊢ WEquiv x y

Tactic:
by
  revert h
  induction x using q.P.wCases
  case ih a₀ f'₀ f₀ =>
    induction y using q.P.wCases
    apply WEquiv.abs

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

Goal state before:
pp: case mk.a
F : Type u → Type v
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
this : Wrepr (WType.mk a f) = PFunctor.W.mk (repr (abs ((P F).map Wrepr ⟨a, f⟩)))
⊢ abs (Wrepr (WType.mk a f)).dest = abs (PFunctor.W.mk ((P F).map Wrepr ⟨a, f⟩)).dest

Tactic:
rw [this, PFunctor.W.dest_mk, abs_repr]

Goal state after:
case mk.a
F : Type u → Type v
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
this : Wrepr (WType.mk a f) = PFunctor.W.mk (repr (abs ((P F).map Wrepr ⟨a, f⟩)))
⊢ abs ((P F).map Wrepr ⟨a, f⟩) = abs (PFunctor.W.mk ((P F).map Wrepr ⟨a, f⟩)).dest
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
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
⊢ ∀ (x y : Cofix F α), r x y → x = y

Tactic:
let r' (x y) := x = y ∨ r x y
  intro x y rxy
  apply Cofix.bisim_aux r'
  · intro x
    left
    rfl
  · intro x y r'xy
    cases r'xy with
    | inl h =>
      rw [h]
    | inr r'xy =>
      have : ∀ x y, r x y → r' x y := fun x y h => Or.inr h
      rw [← Quot.factor_mk_eq _ _ this]
      dsimp [r']
      rw [appendFun_comp_id]
      rw [@comp_map _ _ q _ _ _ (appendFun id (Quot.mk r)),
        @comp_map _ _ q _ _ _ (appendFun id (Quot.mk r))]
      rw [h _ _ r'xy]
  right; exact rxy

Goal state after:
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
a : (P F).A
f : (P F).B a → α
xeq : x = abs ⟨a, f⟩
h' : ∀ (i : (P F).B a), p (f i)
⊢ p u

Tactic:
rcases h a f xeq.symm with ⟨i, _, hi⟩

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
a : (P F).A
f : (P F).B a → α
xeq : x = abs ⟨a, f⟩
h' : ∀ (i : (P F).B a), p (f i)
i : (P F).B a
left✝ : i ∈ univ
hi : f i = u
⊢ p u
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
⊢ SuppPreservation ↔ LiftpPreservation

Tactic:
constructor <;> intro h

Goal state after:
case mp
F : Type u → Type u
q : QPF F
h : SuppPreservation
⊢ LiftpPreservation

case mpr
F : Type u → Type u
q : QPF F
h : LiftpPreservation
⊢ SuppPreservation
Module: Mathlib.Data.QPF.Univariate.Basic

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

Tactic:
simp only [supp, h]

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

Goal state before:
pp: α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
⊢ some (some a) ∈ some none :: f ↔ some (some a) ∈ f

Tactic:
constructor <;> intro h

Goal state after:
case mp
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
h : some (some a) ∈ some none :: f
⊢ some (some a) ∈ f

case mpr
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
h : some (some a) ∈ f
⊢ some (some a) ∈ some none :: f
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
b : β
h : b ∈ t
⊢ ∃ a ∈ s, R a b

Tactic:
rw [← LiftRel.swap] at H

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : swap (LiftRel fun x y ↦ R y x) s t
b : β
h : b ∈ t
⊢ ∃ a ∈ s, R a b
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
⊢ Computation.LiftRel (LiftRelO S fun s1 s2 ↦ ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) (map f1 s).destruct
    (map f2 t).destruct

Tactic:
by
      simp only [exists_and_left, destruct_map]
      apply Computation.liftRel_map _ _ (liftRel_destruct h)
      intro o p h
      rcases o with - | a <;> rcases p with - | b
      · simp
      · cases b; cases h
      · cases a; cases h
      · obtain ⟨a, s⟩ := a; obtain ⟨b, t⟩ := b
        obtain ⟨r, h⟩ := h
        exact ⟨h2 r, s, rfl, t, rfl, h⟩

Goal state after:
Module: Mathlib.Data.Setoid.Partition.Card

Goal state before:
pp: case left_inv
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : Function.HasFiniteSupport fun t ↦ (s ∩ ↑t).ncard
t : ↑P
x y : α
⊢ y ∈ s → y ∈ ↑t → Finite ↑(s ∩ ↑t) → x ∈ s → x ∈ ↑t → ⟨⋯.choose, ⋯⟩ = t

Tactic:
hy

Goal state after:
case left_inv
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : Function.HasFiniteSupport fun t ↦ (s ∩ ↑t).ncard
t : ↑P
x y : α
hy : y ∈ s
⊢ y ∈ ↑t → Finite ↑(s ∩ ↑t) → x ∈ s → x ∈ ↑t → ⟨⋯.choose, ⋯⟩ = t
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 (parallel.aux2 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:
simp only [parallel.aux2] at IH
      -- Porting note: `revert IH` & `intro IH` are required.
      revert IH
      cases List.foldr (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c)) (Sum.inr List.nil) l <;>
        intro IH <;> simp only
      · rcases IH with ⟨c', cl, ac⟩
        exact ⟨c', List.Mem.tail _ cl, ac⟩
      · rcases h : destruct c with a | c' <;> simp only [rmap]
        · refine ⟨c, List.mem_cons_self, ?_⟩
          rw [destruct_eq_pure h]
          apply ret_mem
        · intro a' h
          rcases h with ⟨d, dm, ad⟩
          rcases List.mem_cons.mp dm with e | dl
          · rw [e] at ad
            refine ⟨c, List.mem_cons_self, ?_⟩
            rw [destruct_eq_think h]
            exact think_mem ad
          · obtain ⟨d, dm⟩ := IH a' ⟨d, dl, ad⟩
            obtain ⟨dm, ad⟩ := dm
            exact ⟨d, List.Mem.tail _ dm, ad⟩

Goal state after:
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
s : WSeq α
S' : WSeq (WSeq α)
t : WSeq β
T' : WSeq (WSeq β)
st : LiftRel R s t
ST' : LiftRel (LiftRel R) S' T'
x✝² : S.destruct.Results (some (s, S')) m
mT : some (t, T') ∈ T.destruct
rs2 : (s.destruct.bind (destruct_append.aux S'.join)).think.Results a k
k1 : ℕ
rs3 : (s.destruct.bind (destruct_append.aux S'.join)).Results a k1
ek : k = k1 + 1
o' : Option (α × WSeq α)
m1 n1 : ℕ
rs4 : s.destruct.Results o' m1
rs5 : (destruct_append.aux S'.join o').Results a n1
ek1 : k1 = n1 + m1
p' : Option (β × WSeq β)
mt✝ : p' ∈ t.destruct
rop' : LiftRelO R (LiftRel R) o' p'
x✝¹ : LiftRelO R (LiftRel R) none none
x✝ : s.destruct.Results none m1
rs5' : (destruct_append.aux S'.join none).Results a n1
mt : none ∈ t.destruct
⊢ n1 < n

Tactic:
en,

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
s : WSeq α
S' : WSeq (WSeq α)
t : WSeq β
T' : WSeq (WSeq β)
st : LiftRel R s t
ST' : LiftRel (LiftRel R) S' T'
x✝² : S.destruct.Results (some (s, S')) m
mT : some (t, T') ∈ T.destruct
rs2 : (s.destruct.bind (destruct_append.aux S'.join)).think.Results a k
k1 : ℕ
rs3 : (s.destruct.bind (destruct_append.aux S'.join)).Results a k1
ek : k = k1 + 1
o' : Option (α × WSeq α)
m1 n1 : ℕ
rs4 : s.destruct.Results o' m1
rs5 : (destruct_append.aux S'.join o').Results a n1
ek1 : k1 = n1 + m1
p' : Option (β × WSeq β)
mt✝ : p' ∈ t.destruct
rop' : LiftRelO R (LiftRel R) o' p'
x✝¹ : LiftRelO R (LiftRel R) none none
x✝ : s.destruct.Results none m1
rs5' : (destruct_append.aux S'.join none).Results a n1
mt : none ∈ t.destruct
⊢ n1 < k + m
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case pos
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : c₁ = c₂
⊢ ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ } { s := ofList (c₂ :: cs₂), i := 0 + c₂ } = true ↔ c₁ :: cs₁ < c₂ :: cs₂

Tactic:
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

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

Goal state before:
pp: case mp
α₁ : 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 : γ₁ ⊕ γ₂
⊢ c ∈ sumLexLift f₁ f₂ g₁ g₂ a b →
    (∃ 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₂

Tactic:
obtain a | a := a

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

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x y : G
s : Set α
hs : x • s =ᵐ[μ] s
hy : y ∈ Subgroup.zpowers x
⊢ y • s =ᵐ[μ] s

Tactic:
← MulAction.mem_aestabilizer,

Goal state after:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x y : G
s : Set α
hs : x ∈ MulAction.aestabilizer G μ s
hy : y ∈ Subgroup.zpowers x
⊢ y • s =ᵐ[μ] s
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f g : CircleDeg1Lift
⊢ f 0 + ↑⌈g 0⌉ < f 0 + (g 0 + 1)

Tactic:
by gcongr; exact ceil_lt_add_one _

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)
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
this : ν.InnerRegularCompactLTTop
s : Set Y
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
ε : ℝ≥0∞
hε : ε > 0
hso : IsOpen[inst✝⁵] s
⊢ ∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε

Tactic:
have hνs' : μ (g ⁻¹' s) ≠ ∞ := by rwa [hg.measure_preimage hs]

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)
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
this : ν.InnerRegularCompactLTTop
s : Set Y
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
ε : ℝ≥0∞
hε : ε > 0
hso : IsOpen[inst✝⁵] s
hνs' : μ (⇑g ⁻¹' s) ≠ ∞
⊢ ∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: M : Type u_1
inst✝⁹ : TopologicalSpace M
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : SMul M X
inst✝³ : ContinuousSMul M X
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul M X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : Dense {g | (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s}
⊢ EventuallyConst s (ae μ)

Tactic:
borelize M
  refine aeconst_of_forall_preimage_smul_ae_eq M hsm ?_
  rwa [dense_iff_closure_eq, IsClosed.closure_eq, eq_univ_iff_forall] at hd
  let f : C(M × X, X) := ⟨(· • ·).uncurry, continuous_smul⟩
  exact isClosed_setOfPred_preimage_ae_eq f.curry.continuous (measurePreserving_smul · μ) _ hsm
    (measure_ne_top _ _)

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

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

Tactic:
rwa [← iterate_mul, this, ← iterate_add_apply, tsub_add_cancel_of_le]
    exact hkl.le

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:
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.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
s : Set α
α' : Type u_5
β' : Type u_6
inst✝ : TopologicalSpace β'
f : Filter τ
ϕ : τ → α → β
ϕ' : τ → α' → β'
ga : α → α'
s' : Set α'
hs : MapsTo ga s s'
gb : β → β'
hg : ∀ᶠ (t : τ) in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s
hgc : Continuous[inst✝¹, inst✝] gb
y : β
⊢ (∀ i ∈ f, y ∈ closure[inst✝¹] (image2 ϕ i s)) → ∀ i ∈ f, gb y ∈ closure[inst✝] (image2 ϕ' i s')

Tactic:
hy

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
s : Set α
α' : Type u_5
β' : Type u_6
inst✝ : TopologicalSpace β'
f : Filter τ
ϕ : τ → α → β
ϕ' : τ → α' → β'
ga : α → α'
s' : Set α'
hs : MapsTo ga s s'
gb : β → β'
hg : ∀ᶠ (t : τ) in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s
hgc : Continuous[inst✝¹, inst✝] gb
y : β
hy : ∀ i ∈ f, y ∈ closure[inst✝¹] (image2 ϕ i s)
⊢ ∀ i ∈ f, gb y ∈ closure[inst✝] (image2 ϕ' i s')
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case mp
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
⊢ y ∈ ω f ϕ (s₁ ∪ s₂) → y ∈ ω f ϕ s₁ ∪ ω f ϕ s₂

Tactic:
simp only [mem_union, mem_omegaLimit_iff_frequently, union_inter_distrib_right, union_nonempty,
      frequently_or_distrib]

Goal state after:
case mp
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
⊢ (∀ n ∈ 𝓝 y, (∃ᶠ (x : τ) in f, (s₁ ∩ ϕ x ⁻¹' n).Nonempty) ∨ ∃ᶠ (x : τ) in f, (s₂ ∩ ϕ x ⁻¹' n).Nonempty) →
    (∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, (s₁ ∩ ϕ t ⁻¹' n).Nonempty) ∨ ∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, (s₂ ∩ ϕ t ⁻¹' n).Nonempty
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)
hj₂ : k \ n ⊆ ⋃ u ∈ f, j u
g : Set (Set τ)
hg₁ : ∀ u ∈ g, u ∈ f
hg₂ : g.Finite
hg₃ : k \ n ⊆ ⋃ i ∈ g, j i
w : Set τ := (⋂ u ∈ g, u) ∩ v
hw₂ : w ∈ f
hw₃ : k \ n ⊆ (closure[inst✝] (image2 ϕ w s))ᶜ
⊢ ∃ u ∈ f, closure[inst✝] (image2 ϕ u s) ⊆ n

Tactic:
have hw₄ : kᶜ ⊆ (closure (image2 ϕ w s))ᶜ := by
    simp only [compl_subset_compl]
    exact closure_mono (image2_subset inter_subset_right Subset.rfl)

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)
hj₂ : k \ n ⊆ ⋃ u ∈ f, j u
g : Set (Set τ)
hg₁ : ∀ u ∈ g, u ∈ f
hg₂ : g.Finite
hg₃ : k \ n ⊆ ⋃ i ∈ g, j i
w : Set τ := (⋂ u ∈ g, u) ∩ v
hw₂ : w ∈ f
hw₃ : k \ n ⊆ (closure[inst✝] (image2 ϕ w s))ᶜ
hw₄ : kᶜ ⊆ (closure[inst✝] (image2 ϕ w s))ᶜ
⊢ ∃ u ∈ f, closure[inst✝] (image2 ϕ u s) ⊆ n
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν + ν']
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᵐ[ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
⊢ μ.singularPart ν' ⟂ₘ ν'

Tactic:
exact mutuallySingular_singularPart μ ν'

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

Goal state before:
pp: X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ netMaxcard T F U 0 = 1

Tactic:
apply (iSup₂_le _).antisymm ((one_le_netMaxcard_iff T F U 0).2 h)

Goal state after:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ ∀ (i : Finset X), IsDynNetIn T F U 0 ↑i → ↑i.card ≤ 1