mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation
α : TypeVec.{u} n
a a' : (P F).A
f : (P F).B a ⟹ α
f' : (P F).B a' ⟹ α
h' : abs ⟨a, f⟩ = abs ⟨a', f'⟩
i : Fin2 n
⊢ f i '' univ = f' i '' univ

Tactic:
← MvPFunctor.supp_eq,

Goal state after:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation
α : TypeVec.{u} n
a a' : (P F).A
f : (P F).B a ⟹ α
f' : (P F).B a' ⟹ α
h' : abs ⟨a, f⟩ = abs ⟨a', f'⟩
i : Fin2 n
⊢ supp ⟨a, f⟩ i = f' i '' univ
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation
α : TypeVec.{u} n
a a' : (P F).A
f : (P F).B a ⟹ α
f' : (P F).B a' ⟹ α
h' : abs ⟨a, f⟩ = abs ⟨a', f'⟩
i : Fin2 n
⊢ supp ⟨a, f⟩ i = f' i '' univ

Tactic:
← MvPFunctor.supp_eq,

Goal state after:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation
α : TypeVec.{u} n
a a' : (P F).A
f : (P F).B a ⟹ α
f' : (P F).B a' ⟹ α
h' : abs ⟨a, f⟩ = abs ⟨a', f'⟩
i : Fin2 n
⊢ supp ⟨a, f⟩ i = supp ⟨a', f'⟩ i
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ ∃ u, abs u = x ∧ ∀ (i : (P F).B u.fst), p (u.snd i)

Tactic:
use ⟨a, fun i => (f i).val⟩

Goal state after:
case h
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ abs ⟨a, fun i ↦ ↑(f i)⟩ = x ∧ ∀ (i : (P F).B ⟨a, fun i ↦ ↑(f i)⟩.fst), p (⟨a, fun i ↦ ↑(f i)⟩.snd i)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.lt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → (erase x t_l).size = t_l.size - 1
t_ih_r' : x ∈ t_r → (erase x t_r).size = t_r.size - 1
h_mem : mem x t_l = true
⊢ ((erase x t_l).balanceR t_x t_r).size = (node size✝ t_l t_x t_r).size - 1

Tactic:
have t_ih_l := t_ih_l' h_mem

Goal state after:
case node.lt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → (erase x t_l).size = t_l.size - 1
t_ih_r' : x ∈ t_r → (erase x t_r).size = t_r.size - 1
h_mem : mem x t_l = true
t_ih_l : (erase x t_l).size = t_l.size - 1
⊢ ((erase x t_l).balanceR t_x t_r).size = (node size✝ t_l t_x t_r).size - 1
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mk.mk
F : Type u → Type v
q : QPF F
a✝¹ : (P F).A
f✝¹ : (P F).B a✝¹ → WType (P F).B
a✝ : (P F).A
f✝ : (P F).B a✝ → WType (P F).B
h : QPF.abs (PFunctor.W.dest (WType.mk a✝¹ f✝¹)) = QPF.abs (PFunctor.W.dest (WType.mk a✝ f✝))
⊢ Wequiv (WType.mk a✝¹ f✝¹) (WType.mk a✝ f✝)

Tactic:
apply Wequiv.abs

Goal state after:
case mk.mk
F : Type u → Type v
q : QPF F
a✝¹ : (P F).A
f✝¹ : (P F).B a✝¹ → WType (P F).B
a✝ : (P F).A
f✝ : (P F).B a✝ → WType (P F).B
h : QPF.abs (PFunctor.W.dest (WType.mk a✝¹ f✝¹)) = QPF.abs (PFunctor.W.dest (WType.mk a✝ f✝))
⊢ QPF.abs ⟨a✝¹, f✝¹⟩ = QPF.abs ⟨a✝, f✝⟩
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
⊢ abs ⟨a, fixToW ∘ fun x ↦ ⟦f x⟧⟩ = abs (Wrepr (WType.mk a f)).dest

Tactic:
simp only [Wrepr, recF_eq, PFunctor.W.dest_mk, abs_repr, Function.comp]

Goal state after:
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
⊢ abs ⟨a, fixToW ∘ fun x ↦ ⟦f x⟧⟩ = abs ((P F).map (recF (PFunctor.W.mk ∘ repr)) (PFunctor.W.dest (WType.mk a f)))
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u_1
Q : α → Prop
u v : α → Cofix F
h :
  ∀ (x : α),
    Q x →
      ∃ a f f',
        (u x).dest = abs ⟨a, f⟩ ∧ (v x).dest = abs ⟨a, f'⟩ ∧ ∀ (i : (P F).B a), ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x'
x✝¹ : α
Qx : Q x✝¹
R : Cofix F → Cofix F → Prop := fun w z ↦ ∃ x', Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F
x✝ : R x y
x' : α
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f f' : (P F).B a → Cofix F
ux'eq : (u x').dest = abs ⟨a, f⟩
vx'eq : (v x').dest = abs ⟨a, f'⟩
h' : ∀ (i : (P F).B a), ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x'
⊢ Liftr R x.dest y.dest

Tactic:
liftr_iff

Goal state after:
F : Type u → Type u
q : QPF F
α : Type u_1
Q : α → Prop
u v : α → Cofix F
h :
  ∀ (x : α),
    Q x →
      ∃ a f f',
        (u x).dest = abs ⟨a, f⟩ ∧ (v x).dest = abs ⟨a, f'⟩ ∧ ∀ (i : (P F).B a), ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x'
x✝¹ : α
Qx : Q x✝¹
R : Cofix F → Cofix F → Prop := fun w z ↦ ∃ x', Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F
x✝ : R x y
x' : α
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f f' : (P F).B a → Cofix F
ux'eq : (u x').dest = abs ⟨a, f⟩
vx'eq : (v x').dest = abs ⟨a, f'⟩
h' : ∀ (i : (P F).B a), ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x'
⊢ ∃ a f₀ f₁, x.dest = abs ⟨a, f₀⟩ ∧ y.dest = abs ⟨a, f₁⟩ ∧ ∀ (i : (P F).B a), R (f₀ i) (f₁ i)
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: r : ℝ
hr : r ≠ 0
⊢ 0 < r.sign * r

Tactic:
refine lt_of_le_of_ne (sign_mul_nonneg r) fun h => hr ?_

Goal state after:
r : ℝ
hr : r ≠ 0
h : 0 = r.sign * r
⊢ r = 0
Module: Mathlib.Data.QPF.Univariate.Basic

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

Tactic:
exact ⟨a, f, haf.symm, fun i => mem_image_of_mem _ (mem_univ _)⟩

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

Goal state before:
pp: α : Type u
s : WSeq α
⊢ LiftRel Eq s.think s

Tactic:
simpa using! Equiv.refl _

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a b : α i
h : a < b
c : α i
ha : a < c
hb : c < b
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨i, b⟩

Tactic:
exact ⟨⟨i, c⟩, LT.fiber i a c ha, LT.fiber i c b hb⟩

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

Goal state before:
pp: α : Type u
s : Seq α
⊢ Computation.pure (Option.map (Prod.fst ∘ fun a ↦ (a, ↑s.tail)) s.head) = Computation.pure s.head

Tactic:
cases Seq.head s <;> rfl

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ ⟨k, c⟩ ∈ sigmaLift (fun x ↦ Icc) ⟨i, a⟩ ⟨j, b⟩ ↔ ⟨i, a⟩ ≤ ⟨k, c⟩ ∧ ⟨k, c⟩ ≤ ⟨j, b⟩

Tactic:
simp_rw [mem_sigmaLift, le_def, mem_Icc, exists_and_left, ← exists_and_right, ← exists_prop]

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ (∃ (h : i = k) (_ : ⋯ ▸ a ≤ c) (x : j = k), c ≤ ⋯ ▸ b) ↔ ∃ (h : i = k) (_ : ⋯ ▸ a ≤ c) (h : k = j), ⋯ ▸ c ≤ b
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
⊢ (⟨j, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Ioi a)) ↔
    ⟨i, a⟩ < ⟨j, b⟩

Tactic:
obtain rfl | hij := eq_or_ne i j
    · simp
    · simp [hij, lt_def]

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

Goal state before:
pp: α : Type u
S : WSeq (WSeq α)
⊢ S.join.destruct = S.destruct.bind destruct_join.aux

Tactic:
apply
    Computation.eq_of_bisim
      (fun c1 c2 =>
        c1 = c2 ∨ ∃ S, c1 = destruct (join S) ∧ c2 = (destruct S).bind destruct_join.aux)
      _ (Or.inr ⟨S, rfl, rfl⟩)
  intro c1 c2 h
  exact
    match c1, c2, h with
    | c, _, Or.inl <| rfl => by cases c.destruct <;> simp
    | _, _, Or.inr ⟨S, rfl, rfl⟩ => by
      induction S using WSeq.recOn
      case nil | cons => simp
      case think S => exact Or.inr ⟨S, by simp⟩

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

Goal state before:
pp: α : Type u
S T : WSeq (WSeq α)
s1 : WSeq α
⊢ ∀ {t : WSeq α},
    (fun s1 s2 ↦ ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)) s1 t →
      Computation.LiftRel
        (LiftRelO Eq fun s1 s2 ↦ ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
        s1.destruct t.destruct

Tactic:
s2

Goal state after:
α : Type u
S T : WSeq (WSeq α)
s1 s2 : WSeq α
⊢ (fun s1 s2 ↦ ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)) s1 s2 →
    Computation.LiftRel
      (LiftRelO Eq fun s1 s2 ↦ ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
      s1.destruct s2.destruct
Module: Mathlib.Data.Tree.Traversable

Goal state before:
pp: α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
t : BinaryTree α
⊢ traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) t = Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g t)

Tactic:
induction t with

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

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

Tactic:
funext c

Goal state after:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun c ↦ map (fun a ↦ (a, c)) c) S
c : Computation α
⊢ id c = ((map fun c ↦ c.1) ∘ fun c ↦ map (fun a ↦ (a, c)) c) c
Module: Mathlib.Data.Tree.Traversable

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
t : BinaryTree α
⊢ traverse (pure ∘ f) t = pure (map f t)

Tactic:
induction t with

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

Goal state before:
pp: α : Type u
SS : WSeq (WSeq (WSeq α))
s1 : WSeq α
⊢ ∀ {t : WSeq α},
    (fun s1 s2 ↦ ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)) s1
        t →
      Computation.LiftRel
        (LiftRelO Eq fun s1 s2 ↦
          ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
        s1.destruct t.destruct

Tactic:
s2

Goal state after:
α : Type u
SS : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
⊢ (fun s1 s2 ↦ ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)) s1
      s2 →
    Computation.LiftRel
      (LiftRelO Eq fun s1 s2 ↦
        ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
      s1.destruct s2.destruct
Module: Mathlib.Data.Tree.Traversable

Goal state before:
pp: α : Type u_1
F : Type u → Type u_3
G : Type u → Type u_4
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
β : Type u
f : α → F β
t : BinaryTree α
⊢ (fun {α} ↦ η.app α) (traverse f t) = traverse (η.app β ∘ f) t

Tactic:
induction t with

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : WSeq α
f : α → WSeq β
g : β → WSeq γ
⊢ (s.bind f).bind g ~ʷ s.bind fun x ↦ (f x).bind g

Tactic:
by
  exact bind_assoc_comp s f g

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 =ᵐ[μ] ∅ ∨ s =ᵐ[μ] univ

Tactic:
ae_eq_empty,

Goal state after:
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 =ᵐ[μ] univ
Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : MeasurableSpace X
inst✝⁸ : BorelSpace X
inst✝⁷ : R1Space X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : BorelSpace Y
inst✝³ : R1Space Y
inst✝² : TopologicalSpace Z
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
f : Z → C(X, Y)
hf : Continuous[inst✝², _] f
hfm : ∀ (z : Z), MeasurePreserving (⇑(f z)) μ ν
s : Set X
t : Set Y
htm : NullMeasurableSet t ν
ht : ν t ≠ ∞
⊢ IsOpen[inst✝²] {z | ⇑(f z) ⁻¹' t =ᵐ[μ] s}ᶜ

Tactic:
isOpen_iff_mem_nhds

Goal state after:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : MeasurableSpace X
inst✝⁸ : BorelSpace X
inst✝⁷ : R1Space X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : BorelSpace Y
inst✝³ : R1Space Y
inst✝² : TopologicalSpace Z
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
f : Z → C(X, Y)
hf : Continuous[inst✝², _] f
hfm : ∀ (z : Z), MeasurePreserving (⇑(f z)) μ ν
s : Set X
t : Set Y
htm : NullMeasurableSet t ν
ht : ν t ≠ ∞
⊢ ∀ x ∈ {z | ⇑(f z) ⁻¹' t =ᵐ[μ] s}ᶜ, {z | ⇑(f z) ⁻¹' t =ᵐ[μ] s}ᶜ ∈ 𝓝 x
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x ↦ g * x) μ
a : G
h : a ∉ closure[inst✝⁴] (range fun x ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst✝⁴] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ m, g ^ m • V
hso : IsOpen[inst✝⁴] s
hsne : s.Nonempty
m : ℤ
x : G
hx : x ∈ V
y : G
hy : y ∈ V
hxy : (fun x ↦ a • x) y = (fun x ↦ g ^ m • x) x
⊢ False

Tactic:
apply hV y hy x hx m

Goal state after:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x ↦ g * x) μ
a : G
h : a ∉ closure[inst✝⁴] (range fun x ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst✝⁴] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋯
hso : IsOpen[inst✝⁴] s
hsne : s.Nonempty
m : ℤ
x : G
hx : x ∈ V
y : G
hy : y ∈ V
hxy : (fun x ↦ a • x) y = (fun x ↦ g ^ m • x) x
⊢ g ^ m = a * y / x
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: case inl
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : ε ≤ 0
⊢ closedBall x ε =ᵐ[volume] ∅

Tactic:
ae_eq_empty,

Goal state after:
case inl
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : ε ≤ 0
⊢ volume (closedBall x ε) = 0
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: case map_eq
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hs : MeasurableSet s
⊢ (ν.withDensity (μ.rnDeriv ν)) (f ⁻¹' s) + (μ.singularPart ν) s =
    (ν.withDensity (μ.rnDeriv ν)) s + (μ.singularPart ν) s

Tactic:
← add_apply,

Goal state after:
case map_eq
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hs : MeasurableSet s
⊢ (ν.withDensity (μ.rnDeriv ν)) (f ⁻¹' s) + (μ.singularPart ν) s = (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν) s
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: case map_eq
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hs : MeasurableSet s
⊢ (ν.withDensity (μ.rnDeriv ν)) (f ⁻¹' s) + (μ.singularPart ν) (f ⁻¹' s) = μ s

Tactic:
← add_apply,

Goal state after:
case map_eq
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hs : MeasurableSet s
⊢ (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν) (f ⁻¹' s) = μ s
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this✝ : IsFiniteMeasure μ
S : Set (Measure X) := ⋯
h : μ ∈ extremePoints ℝ≥0∞ S
this : ∀ {s : Set X}, MeasurableSet s → f ⁻¹' s = s → μ s ≠ 0 → c • μ[|s] ∈ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
H : ¬EventuallyConst s (ae μ)
hs : μ s ≠ 0
hs' : μ sᶜ ≠ 0
⊢ μ ∈ openSegment ℝ≥0∞ (c • μ[|s]) (c • μ[|sᶜ])

Tactic:
refine ⟨μ s / c, μ sᶜ / c, ENNReal.div_pos hs hc, ENNReal.div_pos hs' hc, ?_, ?_⟩

Goal state after:
case refine_1
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this✝ : IsFiniteMeasure μ
S : Set (Measure X) := {ν | MeasurePreserving f ν ν ∧ ν univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
this : ∀ {s : Set X}, MeasurableSet s → f ⁻¹' s = s → μ s ≠ 0 → c • μ[|s] ∈ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
H : ¬EventuallyConst s (ae μ)
hs : μ s ≠ 0
hs' : μ sᶜ ≠ 0
⊢ μ s / c + μ sᶜ / c = 1

case refine_2
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this✝ : IsFiniteMeasure μ
S : Set (Measure X) := {ν | MeasurePreserving f ν ν ∧ ν univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
this : ∀ {s : Set X}, MeasurableSet s → f ⁻¹' s = s → μ s ≠ 0 → c • μ[|s] ∈ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
H : ¬EventuallyConst s (ae μ)
hs : μ s ≠ 0
hs' : μ sᶜ ≠ 0
⊢ (μ s / c) • c • μ[|s] + (μ sᶜ / c) • c • μ[|sᶜ] = μ
Module: Mathlib.Dynamics.Flow

Goal state before:
pp: τ : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace τ
inst✝² : TopologicalSpace α
inst✝¹ : SubtractionCommMonoid τ
inst✝ : ContinuousNeg τ
ϕ : Flow τ α
x✝ : α
⊢ ϕ.toFun 0 x✝ = x✝

Tactic:
map_zero_apply

Goal state after:
τ : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace τ
inst✝² : TopologicalSpace α
inst✝¹ : SubtractionCommMonoid τ
inst✝ : ContinuousNeg τ
ϕ : Flow τ α
x✝ : α
⊢ x✝ = x✝
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_3
G : Type u_4
inst✝¹ : Inhabited A
inst✝ : Monoid G
F : Set (Pattern A G)
h : G
x : G → A
hx : x ∈ mulForbidden F
p : Pattern A G
hp : p ∈ F
g : G
⊢ ¬p.mulOccursInAt (mulShift h x) g

Tactic:
specialize hx p hp (h * g)

Goal state after:
A : Type u_3
G : Type u_4
inst✝¹ : Inhabited A
inst✝ : Monoid G
F : Set (Pattern A G)
h : G
x : G → A
p : Pattern A G
hp : p ∈ F
g : G
hx : ¬p.mulOccursInAt x (h * g)
⊢ ¬p.mulOccursInAt (mulShift h x) g
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_3
G : Type u_4
inst✝¹ : Inhabited A
inst✝ : Monoid G
F : Set (Pattern A G)
h : G
x : G → A
p : Pattern A G
hp : p ∈ F
g : G
hx : p.mulOccursInAt (mulShift h x) g
⊢ p.mulOccursInAt x (h * g)

Tactic:
simpa [mulOccursInAt_mulShift] using hx

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

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

Tactic:
rw [Filter.EventuallyEq, ae_restrict_iff' ht]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν'
inst✝ : SigmaFinite ν'
h✝ : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h✝.nullSet
ht : MeasurableSet t
h : (μ.restrict t).rnDeriv ν' =ᵐ[ν] t.indicator (μ.rnDeriv ν')
⊢ ∀ᵐ (x : α) ∂ν, x ∈ t → μ.rnDeriv ν' x = (μ.restrict t).rnDeriv ν' x
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ 1 ≤ netMaxcard T F U n ↔ F.Nonempty

Tactic:
by
  rw [Order.one_le_iff_ne_zero, nonempty_iff_ne_empty]
  exact not_iff_not.2 (netMaxcard_eq_zero_iff T F U n)

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

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

Tactic:
by
  classical
  rcases eq_top_or_lt_top (coverMincard S F ((map φ φ) ⁻¹' V) n) with h' | h'
  · exact h' ▸ le_top
  obtain ⟨s, s_cover, s_card⟩ := (coverMincard_finite_iff S F ((map φ φ) ⁻¹' V) n).1 h'
  rw [← s_card]
  have := s_cover.image h
  rw [← s.coe_image] at this
  exact this.coverMincard_le_card.trans (WithTop.coe_le_coe.2 s.card_image_le)

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case pos
F : Type u_1
inst✝ : Field F
n : ℕ
hn : n = 0
⊢ Group.IsSolvable (X ^ 0 - 1).Gal

Tactic:
pow_zero,

Goal state after:
case pos
F : Type u_1
inst✝ : Field F
n : ℕ
hn : n = 0
⊢ Group.IsSolvable (1 - 1).Gal
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case pos
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : n = 0
⊢ Group.IsSolvable (X ^ 0 - C a).Gal

Tactic:
pow_zero,

Goal state after:
case pos
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : n = 0
⊢ Group.IsSolvable (1 - C a).Gal
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
| map f μ

Tactic:
μ.haveLebesgueDecomposition_add ν

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
| map f (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν))
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case h
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (X ^ n - C a)).Splits
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := (map i (X ^ n - C a)).roots
hs : map i (X ^ n - C a) = (Multiset.map (fun x ↦ X - C x) s).prod
hs' : s.card = n
⊢ map i (X ^ n - 1) = (Multiset.map (fun x ↦ X - C x) (Multiset.map (fun c ↦ c / b) s)).prod

Tactic:
Multiset.map_map

Goal state after:
case h
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (X ^ n - C a)).Splits
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := (map i (X ^ n - C a)).roots
hs : map i (X ^ n - C a) = (Multiset.map (fun x ↦ X - C x) s).prod
hs' : s.card = n
⊢ map i (X ^ n - 1) = (Multiset.map ((fun x ↦ X - C x) ∘ fun c ↦ c / b) s).prod