mathlib-initiative/mathlib-tactics huggingface dataset:
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
β : Type u_1
Q : β → Prop
u v : β → Cofix F α
h :
  ∀ (x : β),
    Q x →
      ∃ a f' f₀ f₁,
        (u x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₀⟩ ∧
          (v x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₁⟩ ∧
            ∀ (i : (P F).last.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' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → Cofix F α
ux'eq : (u x').dest = MvQPF.abs ⟨a, (P F).appendContents f' f₀⟩
vx'eq : (v x').dest = MvQPF.abs ⟨a, (P F).appendContents f' f₁⟩
h' : ∀ (i : (P F).last.B a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
⊢ ∃ a f₀ f₁,
    x.dest = MvQPF.abs ⟨a, f₀⟩ ∧
      y.dest = MvQPF.abs ⟨a, f₁⟩ ∧ ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast R (f₀ i j) (f₁ i j)

Tactic:
refine
        ⟨a, q.P.appendContents f' f₀, q.P.appendContents f' f₁, xeq.symm ▸ ux'eq,
          yeq.symm ▸ vx'eq, ?_⟩

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u_1
Q : β → Prop
u v : β → Cofix F α
h :
  ∀ (x : β),
    Q x →
      ∃ a f' f₀ f₁,
        (u x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₀⟩ ∧
          (v x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₁⟩ ∧
            ∀ (i : (P F).last.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' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → Cofix F α
ux'eq : (u x').dest = MvQPF.abs ⟨a, (P F).appendContents f' f₀⟩
vx'eq : (v x').dest = MvQPF.abs ⟨a, (P F).appendContents f' f₁⟩
h' : ∀ (i : (P F).last.B a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
⊢ ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast R ((P F).appendContents f' f₀ i j) ((P F).appendContents f' f₁ i j)
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
c : Computation (WSeq α)
⊢ Computation.IsBisimulation fun c1 c2 ↦ c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct

Tactic:
intro c1

Goal state after:
α : Type u
c : Computation (WSeq α)
c1 : Computation (Option (α × WSeq α))
⊢ ∀ ⦃s₂ : Computation (Option (α × WSeq α))⦄,
    (fun c1 c2 ↦ c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct) c1 s₂ →
      BisimO (fun c1 c2 ↦ c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct) c1.destruct s₂.destruct
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
o : Option α
s' : Seq (Option α)
h : some a = o ∨ C s'
⊢ C (Seq.cons o s')

Tactic:
rcases o with - | b

Goal state after:
case none
α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
s' : Seq (Option α)
h : some a = none ∨ C s'
⊢ C (Seq.cons none s')

case some
α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
s' : Seq (Option α)
b : α
h : some a = some b ∨ C s'
⊢ C (Seq.cons (some b) s')
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x✝ : α
s✝ : WSeq α
m : (cons x✝ s✝).destruct = Computation.pure (some (a', s'))
this : (cons x✝ s✝).destruct.destruct = (Computation.pure (some (a', s'))).destruct
⊢ a ∈ cons x✝ s✝ ↔ a = a' ∨ a ∈ s'

Tactic:
simp only [destruct_cons, destruct_pure, Sum.inl.injEq, Option.some.injEq,
      Prod.mk.injEq] at this

Goal state after:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x✝ : α
s✝ : WSeq α
m : (cons x✝ s✝).destruct = Computation.pure (some (a', s'))
this : x✝ = a' ∧ s✝ = s'
⊢ a ∈ cons x✝ s✝ ↔ a = a' ∨ a ∈ s'
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h2
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
s' : WSeq α
n : ℕ
h : some a ∈ s'.get? n
⊢ some a ∈ (s'.drop n).head.think

Tactic:
apply think_mem h

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

Goal state before:
pp: case mpr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α i)
i : ι
a b : α i
h : ⋯ ▸ ⟨i, a⟩.snd < ⟨i, b⟩.snd
⊢ ⟨i, a⟩ < ⟨i, b⟩

Tactic:
exact LT.fiber _ _ _ h

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

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

Tactic:
intro c1

Goal state after:
case bisim
α : Type u
β : Type v
f : α → β
s : WSeq α
c1 : Computation (Option (β × WSeq β))
⊢ ∀ ⦃s₂ : Computation (Option (β × WSeq β))⦄,
    (fun c1 c2 ↦ ∃ s, c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct) c1
        s₂ →
      BisimO
        (fun c1 c2 ↦ ∃ s, c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
        c1.destruct s₂.destruct
Module: Mathlib.Data.WSeq.Basic

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

Tactic:
intro c1

Goal state after:
α : Type u
s t : WSeq α
c1 : Computation (Option (α × WSeq α))
⊢ ∀ ⦃s₂ : Computation (Option (α × WSeq α))⦄,
    (fun c1 c2 ↦ ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)) c1 s₂ →
      BisimO (fun c1 c2 ↦ ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)) c1.destruct
        s₂.destruct
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
S : WSeq (WSeq α)
⊢ Computation.IsBisimulation fun c1 c2 ↦ c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux

Tactic:
intro c1

Goal state after:
α : Type u
S : WSeq (WSeq α)
c1 : Computation (Option (α × WSeq α))
⊢ ∀ ⦃s₂ : Computation (Option (α × WSeq α))⦄,
    (fun c1 c2 ↦ c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux) c1 s₂ →
      BisimO (fun c1 c2 ↦ c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux) c1.destruct
        s₂.destruct
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
β : Type v
f : α → β
S : WSeq (Computation α)
⊢ IsBisimulation fun c1 c2 ↦
    ∃ l S, c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)

Tactic:
intro c1

Goal state after:
α : Type u
β : Type v
f : α → β
S : WSeq (Computation α)
c1 : Computation β
⊢ ∀ ⦃s₂ : Computation β⦄,
    (fun c1 c2 ↦
          ∃ l S,
            c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S))
        c1 s₂ →
      BisimO
        (fun c1 c2 ↦
          ∃ l S,
            c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S))
        c1.destruct s₂.destruct
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
SS : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
⊢ ∀ {ca cb : Computation (Option (α × WSeq α))},
    (∃ s S SS,
        ca = (s.append (S.append SS.join).join).destruct ∧
          cb = (s.append (S.join.append (map join SS).join)).destruct) →
      LiftRelAux
        (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))
        (fun c1 c2 ↦
          ∃ s S SS,
            c1 = (s.append (S.append SS.join).join).destruct ∧
              c2 = (s.append (S.join.append (map join SS).join)).destruct)
        ca.destruct cb.destruct

Tactic:
intro c1

Goal state after:
α : Type u
SS : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 : Computation (Option (α × WSeq α))
⊢ ∀ {cb : Computation (Option (α × WSeq α))},
    (∃ s S SS,
        c1 = (s.append (S.append SS.join).join).destruct ∧
          cb = (s.append (S.join.append (map join SS).join)).destruct) →
      LiftRelAux
        (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))
        (fun c1 c2 ↦
          ∃ s S SS,
            c1 = (s.append (S.append SS.join).join).destruct ∧
              c2 = (s.append (S.join.append (map join SS).join)).destruct)
        c1.destruct cb.destruct
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case refl.refl
α : 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
this✝ : S = WSeq.map (map fun c ↦ c.1) T
pe : parallel S = map (fun c ↦ c.1) (parallel T)
h' : a ∈ map (fun c ↦ c.1) (parallel T)
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
ad' : (a, c) ∈ d'
⊢ a ∈ c ∧ c ∈ S

Tactic:
rcases WSeq.exists_of_mem_map dT' with ⟨c', cs', e'⟩

Goal state after:
case refl.refl
α : 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
this✝ : S = WSeq.map (map fun c ↦ c.1) T
pe : parallel S = map (fun c ↦ c.1) (parallel T)
h' : a ∈ map (fun c ↦ c.1) (parallel T)
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
ad' : (a, c) ∈ d'
c' : Computation α
cs' : c' ∈ S
e' : map (fun a ↦ (a, c')) c' = d'
⊢ a ∈ c ∧ c ∈ S
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (s : σ), s ∈ S → (f a s).1 ∈ S
out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).2 = (f a s').2
⊢ (mapAccumr f xs s₀).2 = map (fun x ↦ (f x s₀).2) xs

Tactic:
Vector.map_eq_mapAccumr

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (s : σ), s ∈ S → (f a s).1 ∈ S
out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).2 = (f a s').2
⊢ (mapAccumr f xs s₀).2 = (mapAccumr (fun x x_1 ↦ ((), (f x s₀).2)) xs ()).2
Module: Mathlib.Dynamics.Ergodic.Action.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : SMul G α
inst✝ : ErgodicSMul G α μ
s : Set α
h : ∀ (g : G), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
g : G
⊢ (fun x ↦ g • x) ⁻¹' t =ᵐ[μ] t

Tactic:
refine .trans (.trans ?_ (h g)) hst

Goal state after:
G : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : SMul G α
inst✝ : ErgodicSMul G α μ
s : Set α
h : ∀ (g : G), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
g : G
⊢ (fun x ↦ g • x) ⁻¹' t =ᵐ[μ] (fun x ↦ g • x) ⁻¹' s
Module: Mathlib.Dynamics.Ergodic.Action.Basic

Goal state before:
pp: case refine_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
x✝ :
  MeasurePreserving f μ μ ∧
    ∀ {s : Set α}, MeasurableSet s → (∀ (g : IterateMulAct f), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s) → EventuallyConst s (ae μ)
h₁ : MeasurePreserving f μ μ
h₂ :
  ∀ {s : Set α}, MeasurableSet s → (∀ (g : IterateMulAct f), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s) → EventuallyConst s (ae μ)
⊢ ∀ ⦃s : Set α⦄, MeasurableSet s → f ⁻¹' s = s → EventuallyConst s (ae μ)

pp: case refine_2
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
h : Ergodic f μ
⊢ ∀ {s : Set α}, MeasurableSet s → (∀ (g : IterateMulAct f), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s) → EventuallyConst s (ae μ)

Tactic:
· intro s hm hs
    refine h₂ hm fun n ↦ ?_
    nth_rewrite 2 [← Function.IsFixedPt.preimage_iterate hs n.val]
    rfl

Goal state after:
case refine_2
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
h : Ergodic f μ
⊢ ∀ {s : Set α}, MeasurableSet s → (∀ (g : IterateMulAct f), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s) → EventuallyConst s (ae μ)
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)
⊢ False

Tactic:
obtain ⟨V, hV₁, hVo, hV⟩ :
      ∃ V : Set G, 1 ∈ V ∧ IsOpen V ∧ ∀ x ∈ V, ∀ y ∈ V, ∀ m : ℤ, g ^ m ≠ a * x / y := by
    rw [← mem_compl_iff, ← interior_compl, mem_interior_iff_mem_nhds] at h
    have : Tendsto (fun (x, y) ↦ a * x / y) (𝓝 1) (𝓝 a) :=
      Continuous.tendsto' (by fun_prop) _ _ (by simp)
    rw [nhds_prod_eq] at this
    simpa [(nhds_basis_opens (1 : G)).prod_self.mem_iff, prod_subset_iff, and_assoc] using this h

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
⊢ False
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
t : ℕ → Set α := fun n ↦ s ∩ f^[n] ⁻¹' s
H : ¬∃ᶠ (m : ℕ) in atTop, μ (s ∩ f^[m] ⁻¹' s) ≠ 0
N : ℕ
hN : μ (t N) ≠ 0
hmax : ∀ n > N, μ (t n) = 0
htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ
T : Set α := t N \ ⋃ n, ⋃ (_ : n > N), t n
hT : T = t N \ ⋃ n, ⋃ (_ : n > N), t n
⊢ μ (t N \ ⋃ n, ⋃ (_ : n > N), t n) ≠ 0

Tactic:
measure_sdiff_null

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : μ s ≠ 0
t : ℕ → Set α := fun n ↦ s ∩ f^[n] ⁻¹' s
H : ¬∃ᶠ (m : ℕ) in atTop, μ (s ∩ f^[m] ⁻¹' s) ≠ 0
N : ℕ
hN : μ (t N) ≠ 0
hmax : ∀ n > N, μ (t n) = 0
htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ
T : Set α := t N \ ⋃ n, ⋃ (_ : n > N), t n
hT : T = t N \ ⋃ n, ⋃ (_ : n > N), t n
⊢ μ (t N) ≠ 0

α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : μ s ≠ 0
t : ℕ → Set α := fun n ↦ s ∩ f^[n] ⁻¹' s
H : ¬∃ᶠ (m : ℕ) in atTop, μ (s ∩ f^[m] ⁻¹' s) ≠ 0
N : ℕ
hN : μ (t N) ≠ 0
hmax : ∀ n > N, μ (t n) = 0
htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ
T : Set α := t N \ ⋃ n, ⋃ (_ : n > N), t n
hT : T = t N \ ⋃ n, ⋃ (_ : n > N), t n
⊢ μ (⋃ n, ⋃ (_ : n > N), t n) = 0
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: case refine_4
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))
hn : 1 ≤ ↑n
hI : I =ᵐ[volume] closedBall x (T / (2 * ↑n))
this : Fintype ↥G
hG_card : #Finset.univ = n
⊢ volume univ ≤ ∑' (g : ↥G), volume I

Tactic:
AddCircle.measure_univ,

Goal state after:
case refine_4
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))
hn : 1 ≤ ↑n
hI : I =ᵐ[volume] closedBall x (T / (2 * ↑n))
this : Fintype ↥G
hG_card : #Finset.univ = n
⊢ ENNReal.ofReal T ≤ ∑' (g : ↥G), volume I
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : OpensMeasurableSpace α
f : α → α
μ : Measure α
h : Conservative f μ
this : ∀ s ∈ countableBasis α, ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
x : α
hx : ∀ i ∈ countableBasis α, x ∈ i → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ i
s : Set α
hs : s ∈ 𝓝 x
o : Set α
hoS : o ∈ countableBasis α
hxo : x ∈ o
hos : o ⊆ s
⊢ ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s

Tactic:
exact (hx o hoS hxo).mono fun n hn => hos hn

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✝ 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 = ∅
⊢ ∀ ⦃c : X⦄, x < c → ¬c < y

Tactic:
simpa using Set.ext_iff.mp he

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝² : μ.HaveLebesgueDecomposition ν
inst✝¹ : ν.HaveLebesgueDecomposition μ
inst✝ : SigmaFinite μ
hμν : μ ≪ ν
hνμ : ν ≪ μ
⊢ (μ.rnDeriv ν)⁻¹ =ᵐ[μ] ν.rnDeriv μ

Tactic:
by
  suffices μ.withDensity (μ.rnDeriv ν)⁻¹ = μ.withDensity (ν.rnDeriv μ) by
    calc (μ.rnDeriv ν)⁻¹ =ᵐ[μ] (μ.withDensity (μ.rnDeriv ν)⁻¹).rnDeriv μ :=
          (rnDeriv_withDensity _ (measurable_rnDeriv _ _).inv).symm
    _ = (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ := by rw [this]
    _ =ᵐ[μ] ν.rnDeriv μ := rnDeriv_withDensity _ (measurable_rnDeriv _ _)
  rw [withDensity_rnDeriv_eq _ _ hνμ, ← withDensity_rnDeriv_eq _ _ hμν]
  conv in ((ν.withDensity (μ.rnDeriv ν)).rnDeriv ν)⁻¹ => rw [withDensity_rnDeriv_eq _ _ hμν]
  change (ν.withDensity (μ.rnDeriv ν)).withDensity (fun x ↦ (μ.rnDeriv ν x)⁻¹) = ν
  rw [withDensity_inv_same (measurable_rnDeriv _ _)
    (by filter_upwards [hνμ.ae_le (rnDeriv_pos hμν)] with x hx using hx.ne')
    (rnDeriv_ne_top _ _)]

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

Goal state before:
pp: case h
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ Monotone fun n ↦ ↑(coverMincard T F U n)

Tactic:
exact fun _ _ m_n ↦ ENat.toENNReal_mono (coverMincard_monotone_time T F U m_n)

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

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n_pos : n ≠ 0
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(coverMincard T F U n)).log / ↑n

Tactic:
have cv_mono : Monotone fun m ↦ (coverMincard T F (U ○ U) m).toENNReal :=
    fun _ _ k_m ↦ ENat.toENNReal_mono (coverMincard_monotone_time T F (U ○ U) k_m)
  have h := cv_mono.expGrowthSup_comp_mul n_pos
  rw [mul_comm, ← div_eq_iff (natCast_ne_bot n) (natCast_ne_top n) (Nat.cast_ne_zero.2 n_pos)] at h
  rw [coverEntropyEntourage, ← h]
  apply monotone_div_right_of_nonneg n.cast_nonneg'
  rw [← expGrowthSup_pow]
  refine expGrowthSup_monotone fun m ↦ ?_
  rw [← ENat.toENNReal_pow]
  exact ENat.toENNReal_mono (coverMincard_mul_le_pow F_inv n m)

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Cardinality

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
L : Type u
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : IsTorsionFree R L
inst✝ : Algebra.IsAlgebraic R L
⊢ #L ≤ max #R ℵ₀

Tactic:
simpa only [lift_id] using lift_cardinalMk_le_max R L

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M : Type w
inst✝ : L.Structure M
L'' : Language
e'✝ : L' ≃ᴸ L''
e✝ e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
⊢ e'.toLHom.comp e'.invLHom = LHom.id L''

Tactic:
e'.right_inv

Goal state after:
L : Language
L' : Language
M : Type w
inst✝ : L.Structure M
L'' : Language
e'✝ : L' ≃ᴸ L''
e✝ e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
⊢ LHom.id L'' = LHom.id L''
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
f g : M ≃[L] N
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
⊢ f = g

Tactic:
by
    cases f
    cases g
    simp only [mk.injEq]
    ext x
    exact funext_iff.1 h₁ x

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
t : L.Term (α ⊕ γ)
f : ↥t.varFinsetLeft → β
xs : β ⊕ γ → M
xs' : α → M
hxs' : ∀ (a : ↥t.varFinsetLeft), xs (Sum.inl (f a)) = xs' ↑a
⊢ realize xs (t.restrictVarLeft f) = realize (Sum.elim xs' (xs ∘ Sum.inr)) t

Tactic:
induction t with
  | var a => cases a <;> simp [restrictVarLeft, hxs']
  | func _ _ ih =>
    exact congr rfl (funext fun i => ih i (by simp [hxs']))

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
s : Set α
⊢ L.distinctConstantsTheory s =
    ⋃ t, L.distinctConstantsTheory ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) t)

Tactic:
classical
    simp only [distinctConstantsTheory]
    rw [← image_iUnion, ← iUnion_inter]
    refine congr(_ '' ($(?_) ∩ _))
    ext ⟨i, j⟩
    simp only [prodMk_mem_set_prod_eq, Finset.coe_map, Function.Embedding.coe_subtype, mem_iUnion,
      mem_image, Finset.mem_coe, Subtype.exists, exists_and_right, exists_eq_right]
    refine ⟨fun h => ⟨{⟨i, h.1⟩, ⟨j, h.2⟩}, ⟨h.1, ?_⟩, ⟨h.2, ?_⟩⟩, ?_⟩
    · simp
    · simp
    · rintro ⟨t, ⟨is, _⟩, ⟨js, _⟩⟩
      exact ⟨is, js⟩

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case equal
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
n✝ : ℕ
t₁✝ t₂✝ : L.Term (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i ↦ x i a) fun i ↦ v i a) = fun i ↦ Sum.elim x v i a
⊢ Term.realize (Sum.elim (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) t₁✝ =
      Term.realize (Sum.elim (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) t₂✝ ↔
    ∀ᶠ (a : α) in ↑u, Term.realize (fun i ↦ Sum.elim x v i a) t₁✝ = Term.realize (fun i ↦ Sum.elim x v i a) t₂✝

Tactic:
erw [(Sum.comp_elim ((↑) : (∀ a, M a) → (u : Filter α).Product M) x v).symm,
      term_realize_cast, term_realize_cast]

Goal state after:
case equal
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
n✝ : ℕ
t₁✝ t₂✝ : L.Term (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i ↦ x i a) fun i ↦ v i a) = fun i ↦ Sum.elim x v i a
⊢ ((Quotient.mk' fun a ↦ Term.realize (fun i ↦ Sum.elim x v i a) t₁✝) =
      Quotient.mk' fun a ↦ Term.realize (fun i ↦ Sum.elim x v i a) t₂✝) ↔
    ∀ᶠ (a : α) in ↑u, Term.realize (fun i ↦ Sum.elim x v i a) t₁✝ = Term.realize (fun i ↦ Sum.elim x v i a) t₂✝
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
⊢ ∅ = ofPred ⊥.Realize

Tactic:
by
    ext
    simp

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
⊢ univ = ofPred ⊤.Realize

Tactic:
by
    ext
    simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case mpr
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : DecidableEq α
inst✝ : Nonempty M
φ : L.Formula α
h : M ⊨ φ.exClosure
v : ↥(BoundedFormula.freeVarFinset φ) → M
hv : Realize (BoundedFormula.restrictFreeVar φ id) v
v' : α → M := fun a ↦ if hmem : a ∈ BoundedFormula.freeVarFinset φ then v ⟨a, hmem⟩ else Classical.choice ⋯
⊢ (equivSentence.symm (equivSentence φ)).Realize v'

Tactic:
simpa [Equiv.symm_apply_apply, Formula.Realize] using
      (BoundedFormula.realize_restrictFreeVar v' (by grind)).1 hv

Goal state after: