mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case cons.inl
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c✝ : Computation α
T : c✝.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : s.think ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
e' :
  (match
      List.foldr
        (fun c o ↦
          match o with
          | Sum.inl a => Sum.inl a
          | Sum.inr ls =>
            match c.destruct with
            | Sum.inl a => Sum.inl a
            | Sum.inr b => Sum.inr (b :: ls))
        (Sum.inr []) l with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls =>
      match c.destruct with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls)) =
    Sum.inr l'
e : s.think = c
⊢ s ∈ l'

Tactic:
← e

Goal state after:
case cons.inl
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c✝ : Computation α
T : c✝.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : s.think ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
e' :
  (match
      List.foldr
        (fun c o ↦
          match o with
          | Sum.inl a => Sum.inl a
          | Sum.inr ls =>
            match c.destruct with
            | Sum.inl a => Sum.inl a
            | Sum.inr b => Sum.inr (b :: ls))
        (Sum.inr []) l with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls =>
      match s.think.destruct with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls)) =
    Sum.inr l'
e : s.think = c
⊢ s ∈ l'
Module: Mathlib.Data.Set.Finite.List

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
n : ℕ
⊢ {l | l.length < n}.Finite

Tactic:
convert! (Finset.range n).finite_toSet.biUnion fun i _ ↦ finite_length_eq α i; ext; simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Monad

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
f : Set (α → β)
s : Set α
inst✝¹ : Finite ↑f
inst✝ : Finite ↑s
⊢ Finite ↑(f.seq s)

Tactic:
by
  rw [seq_def]
  infer_instance

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

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

Tactic:
induction n <;> intro l S c o T

Goal state after:
case zero
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : c✝.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
o : c ∈ l ∨ some (some c) = S.get? 0
T : c.Terminates
⊢ (corec parallel.aux1 (l, S)).Terminates

case succ
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : c✝.Terminates
n✝ : ℕ
a✝ :
  ∀ (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 α
o : c ∈ l ∨ some (some c) = S.get? (n✝ + 1)
T : c.Terminates
⊢ (corec parallel.aux1 (l, S)).Terminates
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some.some
α : 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 : α
s' : WSeq α
dsm : some (a, s') ∈ s.destruct
dse : Prod.fst <$> some (a, s') = o
b : α
t' : WSeq α
dtm : some (b, t') ∈ t.destruct
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some (a, s')) (some (b, t'))
⊢ Prod.fst <$> some (a, s') ∈ t.head

Tactic:
rw [dst.left]

Goal state after:
case some.some
α : 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 : α
s' : WSeq α
dsm : some (a, s') ∈ s.destruct
dse : Prod.fst <$> some (a, s') = o
b : α
t' : WSeq α
dtm : some (b, t') ∈ t.destruct
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some (a, s')) (some (b, t'))
⊢ Prod.fst <$> some (b, s') ∈ t.head
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inr
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
l l' : List (Computation α)
⊢ Prop

Tactic:
· exact ∀ a', (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c

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

Goal state before:
pp: case some.none
α : 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
a : α × WSeq α
h : LiftRelO R (LiftRel R) (some a) none
⊢ LiftRelO S (fun s1 s2 ↦ ∃ s, s1 = map f1 s ∧ ∃ x, s2 = map f2 x ∧ LiftRel R s x)
    (Option.map (Prod.map f1 (map f1)) (some a)) (Option.map (Prod.map f2 (map f2)) none)

pp: case some.some
α : 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
a : α × WSeq α
b : β × WSeq β
h : LiftRelO R (LiftRel R) (some a) (some b)
⊢ LiftRelO S (fun s1 s2 ↦ ∃ s, s1 = map f1 s ∧ ∃ x, s2 = map f2 x ∧ LiftRel R s x)
    (Option.map (Prod.map f1 (map f1)) (some a)) (Option.map (Prod.map f2 (map f2)) (some b))

Tactic:
· cases a; cases h

Goal state after:
case some.some
α : 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
a : α × WSeq α
b : β × WSeq β
h : LiftRelO R (LiftRel R) (some a) (some b)
⊢ LiftRelO S (fun s1 s2 ↦ ∃ s, s1 = map f1 s ∧ ∃ x, s2 = map f2 x ∧ LiftRel R s x)
    (Option.map (Prod.map f1 (map f1)) (some a)) (Option.map (Prod.map f2 (map f2)) (some b))
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some.none
α : Type u
β : Type v
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t ↦ LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
a : α × WSeq α
h : LiftRelO R (LiftRel R) (some a) none
⊢ Computation.LiftRel
    (LiftRelO R fun s t ↦ LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x)
    (destruct_append.aux s2 (some a)) (destruct_append.aux t2 none)

pp: case some.some
α : Type u
β : Type v
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t ↦ LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
a : α × WSeq α
b : β × WSeq β
h : LiftRelO R (LiftRel R) (some a) (some b)
⊢ Computation.LiftRel
    (LiftRelO R fun s t ↦ LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x)
    (destruct_append.aux s2 (some a)) (destruct_append.aux t2 (some b))

Tactic:
· cases a; cases h

Goal state after:
case some.some
α : Type u
β : Type v
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t ↦ LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
a : α × WSeq α
b : β × WSeq β
h : LiftRelO R (LiftRel R) (some a) (some b)
⊢ Computation.LiftRel
    (LiftRelO R fun s t ↦ LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x)
    (destruct_append.aux s2 (some a)) (destruct_append.aux t2 (some b))
Module: Mathlib.Data.Tree.Traversable

Goal state before:
pp: case node
α : Type u_1
β : Type u_2
f : α → β
v : α
l r : BinaryTree α
hl : traverse (pure ∘ f) l = pure (map f l)
hr : traverse (pure ∘ f) r = pure (map f r)
⊢ node (f v) (map f l) <$> pure (map f r) = pure (node (f v) (map f l) (map f r))

Tactic:
map_pure

Goal state after:
case node
α : Type u_1
β : Type u_2
f : α → β
v : α
l r : BinaryTree α
hl : traverse (pure ∘ f) l = pure (map f l)
hr : traverse (pure ∘ f) r = pure (map f r)
⊢ pure (node (f v) (map f l) (map f r)) = pure (node (f v) (map f l) (map f r))
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
a : α
f : α → WSeq β
⊢ (ret a).bind f ~ʷ f a

Tactic:
simp [bind]

Goal state after:
Module: Mathlib.Data.Vector3

Goal state before:
pp: α : Type u_1
m n : ℕ
C : Vector3 α (n + 1) → Sort u
H : (a : α) → (t : Vector3 α n) → C (a :: t)
v : Vector3 α (n + 1)
⊢ C v

Tactic:
rw [← cons_head_tail v]; apply H

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: case snoc
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
f : α → β → σ → σ × γ
f' : β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a b s = f' b s
n✝ : ℕ
xs : Vector α n✝
ys : Vector β n✝
x : α
y : β
ih : ∀ {s : σ}, mapAccumr₂ f xs ys s = mapAccumr f' ys s
s : σ
⊢ mapAccumr₂ f (xs.snoc x) (ys.snoc y) s = mapAccumr f' (ys.snoc y) s

Tactic:
simp [h x y s, ih]

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: case snoc
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
f : α → β → σ → σ × γ
f' : α → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a b s = f' a s
n✝ : ℕ
xs : Vector α n✝
ys : Vector β n✝
x : α
y : β
ih : ∀ {s : σ}, mapAccumr₂ f xs ys s = mapAccumr f' xs s
s : σ
⊢ mapAccumr₂ f (xs.snoc x) (ys.snoc y) s = mapAccumr f' (xs.snoc x) s

Tactic:
simp [h x y s, ih]

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

Goal state before:
pp: case some
α : Type u
s : WSeq α
inst✝ : s.Productive
n : ℕ
h : (fun n ↦ (s.get? n).get) n = none
val✝ : α
e : (s.get? (n + 1)).get = some val✝
this : some val✝ ∈ s.get? (n + 1)
⊢ (fun n ↦ (s.get? n).get) (n + 1) = none

Tactic:
simp only [get?] at this h

Goal state after:
case some
α : Type u
s : WSeq α
inst✝ : s.Productive
n : ℕ
h : (s.drop n).head.get = none
val✝ : α
e : (s.get? (n + 1)).get = some val✝
this : some val✝ ∈ (s.drop (n + 1)).head
⊢ (fun n ↦ (s.get? n).get) (n + 1) = none
Module: Mathlib.Order.SemiconjSup

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

Tactic:
refine fun y => (H _).unique ?_

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

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

Tactic:
refine map_lt_of_translationNumber_lt_int _ ?_ _

Goal state after:
f : CircleDeg1Lift
x : ℝ
⊢ τ f < ↑(⌊τ f⌋ + 1)
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 : {g | (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s} = univ
this✝¹ : MeasurableSpace M := borel M
this✝ : BorelSpace M
⊢ ∀ (g : M), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s

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 : closure[inst✝⁹] {g | (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s} = univ
this✝¹ : MeasurableSpace M := borel M
this✝ : BorelSpace M
⊢ IsClosed[inst✝⁹] {g | (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s}

Tactic:
eq_univ_iff_forall

Goal state after:
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 : ∀ (x : M), x ∈ {g | (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s}
this✝¹ : MeasurableSpace M := borel M
this✝ : BorelSpace M
⊢ ∀ (g : M), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s

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 : closure[inst✝⁹] {g | (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s} = univ
this✝¹ : MeasurableSpace M := borel M
this✝ : BorelSpace M
⊢ IsClosed[inst✝⁹] {g | (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s}
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

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

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

Tactic:
· rintro hd ⟨r, hr⟩
    refine not_denseRange_zsmul (a := b / r.den) <| hd.mono ?_
    rw [← AddSubgroup.coe_zmultiples, SetLike.coe_subset_coe, AddSubgroup.closure_le,
      AddSubgroup.coe_zmultiples, pair_subset_iff]
    refine ⟨⟨r.num, ?_⟩, r.den, ?_⟩
    · simp [field, mul_div_left_comm _ b, ← Rat.cast_def, hr]
    · simp [field]

Goal state after:
case inr.mpr
a b : ℝ
hb : b ≠ 0
⊢ Irrational (a / b) → Dense ↑(AddSubgroup.closure {a, b})
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
h : μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j ↦ closedBall d (T / (2 * ↑(n j)))
hd : Tendsto (fun j ↦ μ (s ∩ I j) / μ (I j)) l (𝓝 1)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
huj' : 1 ≤ ↑(n j)
hI₀ : μ (I j) ≠ 0
hI₁ : μ (I j) ≠ ∞
⊢ ENNReal.ofReal (min T (T / ↑(n j))) * ↑(n j) = ENNReal.ofReal T

Tactic:
min_eq_right (div_le_self hT₀.le huj'),

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
h : μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j ↦ closedBall d (T / (2 * ↑(n j)))
hd : Tendsto (fun j ↦ μ (s ∩ I j) / μ (I j)) l (𝓝 1)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
huj' : 1 ≤ ↑(n j)
hI₀ : μ (I j) ≠ 0
hI₁ : μ (I j) ≠ ∞
⊢ ENNReal.ofReal (T / ↑(n j)) * ↑(n j) = ENNReal.ofReal T
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: 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
hsm : MeasurableSet s
hνs : ν s = 0
hμs : (μ.singularPart ν) sᶜ = 0
⊢ (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν) (f ⁻¹' s) = (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν) s

Tactic:
by
        rw [rnDeriv_add_singularPart, hfμ.measure_preimage hsm.nullMeasurableSet]

Goal state after:
Module: Mathlib.Dynamics.Flow

Goal state before:
pp: τ : Type u_1
α : Type u_2
ϕ : τ → α → α
s : Set α
⊢ IsInvariant ϕ s ↔ ∀ (t : τ), ϕ t '' s ⊆ s

Tactic:
IsInvariant,

Goal state after:
τ : Type u_1
α : Type u_2
ϕ : τ → α → α
s : Set α
⊢ (∀ (t : τ), MapsTo (ϕ t) s s) ↔ ∀ (t : τ), ϕ t '' s ⊆ s
Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage

Goal state before:
pp: case succ
X : Type u_1
T : X → X
U : SetRel X X
inst✝ : UniformSpace X
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
ih : ⋂ i, ⋂ (_ : i < n), (map T T)^[i] ⁻¹' U ∈ 𝓤 X
⊢ ⋂ i, ⋂ (_ : i < n + 1), (map T T)^[i] ⁻¹' U ∈ 𝓤 X

Tactic:
Set.biInter_lt_succ

Goal state after:
case succ
X : Type u_1
T : X → X
U : SetRel X X
inst✝ : UniformSpace X
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
ih : ⋂ i, ⋂ (_ : i < n), (map T T)^[i] ⁻¹' U ∈ 𝓤 X
⊢ (⋂ k, ⋂ (_ : k < n), (map T T)^[k] ⁻¹' U) ∩ (map T T)^[n] ⁻¹' U ∈ 𝓤 X
Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
inst✝ : UniformSpace X
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
⊢ dynEntourage T U n ∈ 𝓤 X

Tactic:
by
  rw [dynEntourage_eq_inter_Ico T U n]
  induction n with
  | zero => simp
  | succ n ih =>
    simp only [iInter_coe_set, mem_Ico, Nat.zero_le, true_and] at ih ⊢
    rw [Set.biInter_lt_succ]
    apply Filter.inter_mem ih
    rw [map_iterate T T n]
    exact uniformContinuous_def.1 (UniformContinuous.iterate T n h) U U_uni

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
this✝ : μ.rnDeriv ν' =ᵐ[ν.restrict t] (μ.restrict t).rnDeriv ν'
this : rnDeriv 0 ν' =ᵐ[ν'] 0
⊢ rnDeriv 0 ν' =ᵐ[ν.restrict h.nullSet] 0

Tactic:
have h_ac' : ν.restrict t ≪ ν' := restrict_le_self.absolutelyContinuous.trans hνν'

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

Goal state before:
pp: 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
x✝ : Nonempty ↥s
y : X
y_F : y ∈ F
k : Fin n
z : X
z_s : z ∈ s
hz : (T^[m * ↑k] y, z) ∈ dynEntourage T U m
⊢ ∃ z, y ∈ T^[m * ↑k] ⁻¹' ball (↑z) (dynEntourage T U m)

Tactic:
exact ⟨⟨z, z_s⟩, (dynEntourage T U m).symm hz⟩

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
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 : eval b (map i (X ^ n - C a)) = 0
⊢ (map i (X ^ n - 1)).Splits

Tactic:
rw [eval_map, eval₂_sub, eval₂_X_pow, eval₂_C, sub_eq_zero] at hb

Goal state after:
case neg
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
⊢ (map i (X ^ n - 1)).Splits
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
K' : Type u
inst✝³ : Field K'
inst✝² : Algebra R K'
inst✝¹ : IsAlgClosed K'
ι' : Type u
v' : ι' → K'
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v'
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K'
⊢ #K' = #ι'

Tactic:
simpa using cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt v' hv hR hK

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg.hq
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ Group.IsSolvable (X ^ n - map (algebraMap F (X ^ n - 1).SplittingField) (C x)).Gal

Tactic:
map_C

Goal state after:
case neg.hq
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ Group.IsSolvable (X ^ n - C ((algebraMap F (X ^ n - 1).SplittingField) x)).Gal
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case hq
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := ⋯
hp : p.comp (X ^ n) ≠ 0
⊢ Group.IsSolvable (p.comp (X ^ n)).Gal

Tactic:
refine gal_isSolvable_tower p (p.comp (X ^ n)) ?_ hα ?_
    · exact Gal.splits_in_splittingField_of_comp _ _ (by rwa [natDegree_X_pow])
    · obtain ⟨s, hs⟩ := splits_iff_exists_multiset.1 (SplittingField.splits p)
      rw [map_comp, Polynomial.map_pow, map_X, hs, mul_comp, C_comp]
      apply gal_mul_isSolvable (gal_C_isSolvable _)
      rw [multiset_prod_comp]
      apply gal_prod_isSolvable
      intro q hq
      rw [Multiset.mem_map] at hq
      obtain ⟨q, hq, rfl⟩ := hq
      rw [Multiset.mem_map] at hq
      obtain ⟨q, _, rfl⟩ := hq
      rw [sub_comp, X_comp, C_comp]
      exact gal_X_pow_sub_C_isSolvable n q

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
γ : Type u_4
xs : β ⊕ γ → M
xs' : α → M
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term (α ⊕ γ)
ih :
  ∀ (a : Fin l✝) {f : ↥(_ts✝ a).varFinsetLeft → β},
    (∀ (a_1 : ↥(_ts✝ a).varFinsetLeft), xs (Sum.inl (f a_1)) = xs' ↑a_1) →
      realize xs ((_ts✝ a).restrictVarLeft f) = realize (Sum.elim xs' (xs ∘ Sum.inr)) (_ts✝ a)
f : ↥(func _f✝ _ts✝).varFinsetLeft → β
hxs' : ∀ (a : ↥(func _f✝ _ts✝).varFinsetLeft), xs (Sum.inl (f a)) = xs' ↑a
i : Fin l✝
⊢ ∀ (a : ↥(_ts✝ i).varFinsetLeft), xs (Sum.inl ((f ∘ Set.inclusion ⋯) a)) = xs' ↑a

Tactic:
simp [hxs']

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
⊢ lift.{max u w, w} #↑(range (Term.realize Subtype.val)) ≤ #(L.Term ↑s)

Tactic:
← Cardinal.lift_id'.{w, max u w} #(L.Term s)

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
⊢ lift.{max u w, w} #↑(range (Term.realize Subtype.val)) ≤ lift.{w, max u w} #(L.Term ↑s)