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

Goal state before:
pp: case mpr
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
u : α
h' : u ∈ f '' univ
a' : (P F).A
f' : (P F).B a' → α
e : abs ⟨a', f'⟩ = abs ⟨a, f⟩
⊢ u ∈ f' '' univ

Tactic:
rw [← h _ _ _ _ e.symm]

Goal state after:
case mpr
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
u : α
h' : u ∈ f '' univ
a' : (P F).A
f' : (P F).B a' → α
e : abs ⟨a', f'⟩ = abs ⟨a, f⟩
⊢ u ∈ f '' univ
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
ds : Option (α × WSeq α)
dsm : ds ∈ s.destruct
dse : Prod.fst <$> ds = o
⊢ Prod.fst <$> ds ∈ t.head

Tactic:
obtain ⟨l, r⟩ := destruct_congr h

Goal state after:
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
ds : Option (α × WSeq α)
dsm : ds ∈ s.destruct
dse : Prod.fst <$> ds = o
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
⊢ Prod.fst <$> ds ∈ t.head
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inr.inl
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a✝ : some (some c) = S.get? 0
H : S.destruct = some (some c, S.tail)
a : α
h : parallel.aux2 l = Sum.inl a
C : corec parallel.aux1 (l, S) = pure a
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
rw [C]

Goal state after:
case inr.inl
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a✝ : some (some c) = S.get? 0
H : S.destruct = some (some c, S.tail)
a : α
h : parallel.aux2 l = Sum.inl a
C : corec parallel.aux1 (l, S) = pure a
⊢ (pure a).Terminates
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inr.inr
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? 0
H : S.destruct = some (some c, S.tail)
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    (corec parallel.aux1
        (match some (some c, S.tail) with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))).think
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
rw [C]

Goal state after:
case inr.inr
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? 0
H : S.destruct = some (some c, S.tail)
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    (corec parallel.aux1
        (match some (some c, S.tail) with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))).think
⊢ (corec parallel.aux1
        (match some (some c, S.tail) with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))).think.Terminates
Module: Mathlib.Data.Seq.Parallel

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

Tactic:
rw [C]

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

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

Tactic:
rw [C]

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

Goal state before:
pp: α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
⊢ List (Computation α) → α ⊕ List (Computation α) → Prop

Tactic:
by
    intro l a
    rcases a with a | l'
    · exact ∃ c ∈ l, a ∈ c
    · exact ∀ a', (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c

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

Goal state before:
pp: case right.HU
α : Type u
β : Type v
R : α → β → Prop
S✝ : WSeq (WSeq α)
T✝ : WSeq (WSeq β)
h✝ : LiftRel (LiftRel R) S✝ T✝
s1 : WSeq α
s2 : WSeq β
x✝¹ :
  (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2
s : WSeq α
t : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1 : s1 = s.append S.join
h2 : s2 = t.append T.join
st : LiftRel R s t
ST : LiftRel (LiftRel R) S T
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
x✝ : LiftRelO R (LiftRel R) none none
b : Option (β × WSeq β)
mb : b ∈ T.join.destruct
⊢ ∀ (s1 : WSeq β) (s2 : WSeq α),
    (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel (swap R) s t ∧ LiftRel (LiftRel (swap R)) S T) →
      ∃ s t S T, s2 = s.append S.join ∧ s1 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T

Tactic:
rw [← LiftRel.swap R, ← LiftRel.swap (LiftRel R)]

Goal state after:
case right.HU
α : Type u
β : Type v
R : α → β → Prop
S✝ : WSeq (WSeq α)
T✝ : WSeq (WSeq β)
h✝ : LiftRel (LiftRel R) S✝ T✝
s1 : WSeq α
s2 : WSeq β
x✝¹ :
  (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2
s : WSeq α
t : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1 : s1 = s.append S.join
h2 : s2 = t.append T.join
st : LiftRel R s t
ST : LiftRel (LiftRel R) S T
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
x✝ : LiftRelO R (LiftRel R) none none
b : Option (β × WSeq β)
mb : b ∈ T.join.destruct
⊢ ∀ (s1 : WSeq β) (s2 : WSeq α),
    (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ swap (LiftRel R) s t ∧ swap (LiftRel (LiftRel R)) S T) →
      ∃ s t S T, s2 = s.append S.join ∧ s1 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
S T : WSeq (WSeq α)
⊢ (S.append T).join ~ʷ S.join.append T.join

Tactic:
by
  refine
    ⟨fun s1 s2 =>
      ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T)),
      ⟨nil, S, T, by simp, by simp⟩, ?_⟩
  intro s1 s2 h
  apply
    liftRel_rec
      (fun c1 c2 =>
        ∃ (s : WSeq α) (S T : _),
          c1 = destruct (append s (join (append S T))) ∧
            c2 = destruct (append s (append (join S) (join T))))
      _ _ _
      (let ⟨s, S, T, h1, h2⟩ := h
      ⟨s, S, T, congr_arg destruct h1, congr_arg destruct h2⟩)
  rintro c1 c2 ⟨s, S, T, rfl, rfl⟩
  induction s using WSeq.recOn with
  | nil =>
    induction S using WSeq.recOn with
    | nil =>
      simp only [nil_append, join_nil]
      induction T using WSeq.recOn with
      | nil => simp
      | cons s T =>
        simp only [join_cons, destruct_think, Computation.destruct_think, liftRelAux_inr_inr]
        refine ⟨s, nil, T, ?_, ?_⟩ <;> simp
      | think T =>
        simp only [join_think, destruct_think, Computation.destruct_think, liftRelAux_inr_inr]
        refine ⟨nil, nil, T, ?_, ?_⟩ <;> simp
    | cons s S => simpa using ⟨s, S, T, rfl, rfl⟩
    | think S => refine ⟨nil, S, T, ?_, ?_⟩ <;> simp
  | cons a s => simpa using ⟨s, S, T, rfl, rfl⟩
  | think s => simpa using ⟨s, S, T, rfl, rfl⟩

Goal state after:
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)
c1 c2 : Computation (Option (α × WSeq α))
h :
  ∃ s S SS,
    c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct
s : WSeq α
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
⊢ 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)
    (s.append (S.append SS.join).join).destruct.destruct (s.append (S.join.append (map join SS).join)).destruct.destruct

Tactic:
clear h
      induction s using WSeq.recOn with
      | nil =>
        induction S using WSeq.recOn with
        | nil =>
          simp only [nil_append, join_nil]
          induction SS using WSeq.recOn with
          | nil => simp
          | cons S SS => refine ⟨nil, S, SS, ?_, ?_⟩ <;> simp
          | think SS => refine ⟨nil, nil, SS, ?_, ?_⟩ <;> simp
        | cons s S => simpa using ⟨s, S, SS, rfl, rfl⟩
        | think S => refine ⟨nil, S, SS, ?_, ?_⟩ <;> simp
      | cons a s => simpa using ⟨s, S, SS, rfl, rfl⟩
      | think s => simpa using ⟨s, S, SS, rfl, rfl⟩

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

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → γ
⊢ map₂ f nil nil = map₂ (flip f) nil nil

Tactic:
simp_all [flip]

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → γ
n✝ : ℕ
a✝¹ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
a✝ : map₂ f x✝ y✝ = map₂ (flip f) y✝ x✝
⊢ map₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝) = map₂ (flip f) (b✝ ::ᵥ y✝) (a✝¹ ::ᵥ x✝)

Tactic:
simp_all [flip]

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

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
⊢ mapAccumr₂ f nil nil s = mapAccumr₂ (flip f) nil nil s

Tactic:
simp_all [flip]

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
n✝ : ℕ
a✝¹ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
a✝ : mapAccumr₂ f x✝ y✝ s = mapAccumr₂ (flip f) y✝ x✝ s
⊢ mapAccumr₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝) s = mapAccumr₂ (flip f) (b✝ ::ᵥ y✝) (a✝¹ ::ᵥ x✝) s

Tactic:
simp_all [flip]

Goal state after:
Module: Mathlib.Data.Vector3

Goal state before:
pp: case refine_2.refine_2
α : Type u_1
n✝ : ℕ
p : α → Prop
v✝ : Vector3 α n✝
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
h : ∀ (i : Fin2 (n + 1)), p ((a :: v) i)
i : Fin2 n
⊢ p (v i)

Tactic:
· simpa using h (fs i)

Goal state after:
Module: Mathlib.Dynamics.FixedPoints.Prufer

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
⊢ g • g⁻¹ • s ⊆ g • s

Tactic:
replace hg : g⁻¹ ^ n ^ j = 1 := by rw [inv_zpow, hg, inv_one]

Goal state after:
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
hg : g⁻¹ ^ n ^ j = 1
⊢ g • g⁻¹ • s ⊆ g • s
Module: Mathlib.Dynamics.OmegaLimit

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

Tactic:
by
  ext y; constructor
  · simp only [mem_union, mem_omegaLimit_iff_frequently, union_inter_distrib_right, union_nonempty,
      frequently_or_distrib]
    contrapose!
    simp only [← subset_empty_iff]
    rintro ⟨⟨n₁, hn₁, h₁⟩, ⟨n₂, hn₂, h₂⟩⟩
    refine ⟨n₁ ∩ n₂, inter_mem hn₁ hn₂, h₁.mono fun t ↦ ?_, h₂.mono fun t ↦ ?_⟩
    exacts [Subset.trans <| inter_subset_inter_right _ <| preimage_mono inter_subset_left,
      Subset.trans <| inter_subset_inter_right _ <| preimage_mono inter_subset_right]
  · rintro (hy | hy)
    exacts [omegaLimit_mono_right _ _ subset_union_left hy,
      omegaLimit_mono_right _ _ subset_union_right hy]

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
u : Set τ
hu : u ∈ f
⊢ ω f ϕ s ⊆ closure[inst✝] (image2 ϕ u s)

Tactic:
rw [omegaLimit_eq_iInter]
  intro _ hx
  rw [mem_iInter] at hx
  exact hx ⟨u, hu⟩

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
inst✝ : UniformSpace X
F_comp : IsCompact F
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
⊢ ∃ s, IsDynCoverOf T F U n ↑s

Tactic:
obtain ⟨(V : SetRel X X), hV, hVsymm, hVU⟩ := symm_of_uniformity U_uni

Goal state after:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
inst✝ : UniformSpace X
F_comp : IsCompact F
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
V : SetRel X X
hV : V ∈ 𝓤 X
hVsymm : V.IsSymm
hVU : V ⊆ U
⊢ ∃ s, IsDynCoverOf T F U n ↑s
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case htc
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
i✝ : ↑f.sets
⊢ closure[inst✝¹] (image2 ϕ v s) ⊆ c

Tactic:
hv₂

Goal state after:
case htc
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
i✝ : ↑f.sets
⊢ c ⊆ c
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
s : Finset X
s_net : s = ∅
⊢ ↑s.card = ⊥

Tactic:
s_net,

Goal state after:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
s : Finset X
s_net : s = ∅
⊢ ↑∅.card = ⊥
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SFinite ν
hμν : μ ≪ ν
s : Set α
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν = μ s

Tactic:
by
  rw [← withDensity_apply' _ s, Measure.withDensity_rnDeriv_eq _ _ hμν]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hν_ac : μ ≪ ν + μ
a : α
h1 : (ν + μ).rnDeriv μ a = (ν.rnDeriv μ + μ.rnDeriv μ) a
h2 : μ.rnDeriv μ a = 1
h3 : (μ.rnDeriv (ν + μ))⁻¹ a = (ν + μ).rnDeriv μ a
⊢ μ.rnDeriv (ν + μ) a = (ν.rnDeriv μ a + 1)⁻¹

Tactic:
rw [Pi.inv_apply, h1, Pi.add_apply, h2, inv_eq_iff_eq_inv] at h3

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hν_ac : μ ≪ ν + μ
a : α
h1 : (ν + μ).rnDeriv μ a = (ν.rnDeriv μ + μ.rnDeriv μ) a
h2 : μ.rnDeriv μ a = 1
h3 : μ.rnDeriv (ν + μ) a = (ν.rnDeriv μ a + 1)⁻¹
⊢ μ.rnDeriv (ν + μ) a = (ν.rnDeriv μ a + 1)⁻¹
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
F : Set X
inst✝ : UniformSpace X
F_comp : IsCompact F
F_inv : MapsTo T F F
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SetRel.IsSymm V
V_U : V ○ V ⊆ U
s : Finset X
s_cover : IsDynCoverOf T F V 1 ↑s
⊢ (↑(#s)).log / ↑1 < ⊤

Tactic:
rw [Nat.cast_one, div_one, log_lt_top_iff, ← ENat.toENNReal_top]

Goal state after:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
inst✝ : UniformSpace X
F_comp : IsCompact F
F_inv : MapsTo T F F
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SetRel.IsSymm V
V_U : V ○ V ⊆ U
s : Finset X
s_cover : IsDynCoverOf T F V 1 ↑s
⊢ ↑(#s) < ↑⊤
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.Syntax

Goal state before:
pp: L : Language
α : Type u'
s : Set α
⊢ (fun ab ↦ ((L.con ab.1).term.equal (L.con ab.2).term).not) '' (s ×ˢ s ∩ (diagonal α)ᶜ) =
    ⋃ t,
      (fun ab ↦ ((L.con ab.1).term.equal (L.con ab.2).term).not) ''
        (↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) t) ×ˢ
            ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) t) ∩
          (diagonal α)ᶜ)

Tactic:
rw [← image_iUnion, ← iUnion_inter]

Goal state after:
L : Language
α : Type u'
s : Set α
⊢ (fun ab ↦ ((L.con ab.1).term.equal (L.con ab.2).term).not) '' (s ×ˢ s ∩ (diagonal α)ᶜ) =
    (fun ab ↦ ((L.con ab.1).term.equal (L.con ab.2).term).not) ''
      ((⋃ i,
          ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) i) ×ˢ
            ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) i)) ∩
        (diagonal α)ᶜ)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
k : ℕ
l : List (L.BoundedFormula α k)
f : L.BoundedFormula α k
⊢ ∀ (v : α → M) (xs : Fin k → M), (List.foldr imp f l).Realize v xs = ((∀ i ∈ l, i.Realize v xs) → f.Realize v xs)

Tactic:
intro v xs

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
k : ℕ
l : List (L.BoundedFormula α k)
f : L.BoundedFormula α k
v : α → M
xs : Fin k → M
⊢ (List.foldr imp f l).Realize v xs = ((∀ i ∈ l, i.Realize v xs) → f.Realize v xs)
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
x✝ : List (Fin n)
⊢ listDecode (flatMap (fun i ↦ (ts i).listEncode) x✝ ++ l) = List.map ts x✝ ++ listDecode l

Tactic:
induction finRange n with

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_2.refine_2.inl.inr
L : Language
α : Type u'
a : α
b : (i : ℕ) × L.Functions i
h :
  Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inl a) =
    Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inr b)
⊢ Sum.inl a = Sum.inr b

Tactic:
simp only [Sum.elim_inl, Sum.elim_inr, Sigma.mk.inj_iff, false_and, reduceCtorEq] at h

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u_3
n : ℕ
φ : L.BoundedFormula α n
v : α → ↥⊤
xs : Fin n → ↥⊤
⊢ φ.Realize v xs ↔ φ.Realize (Subtype.val ∘ v) (Subtype.val ∘ xs)

Tactic:
← StrongHomClass.realize_boundedFormula Substructure.topEquiv φ

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u_3
n : ℕ
φ : L.BoundedFormula α n
v : α → ↥⊤
xs : Fin n → ↥⊤
⊢ φ.Realize (⇑topEquiv ∘ v) (⇑topEquiv ∘ xs) ↔ φ.Realize (Subtype.val ∘ v) (Subtype.val ∘ xs)
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : L.Structure M
S : (L.sum L.skolem₁).Substructure M
⊢ ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → ↥(LHom.sumInl.substructureReduct S)) (a : M),
    φ.Realize default (Fin.snoc (Subtype.val ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (Subtype.val ∘ x) ↑b)

Tactic:
intro n φ x a h

Goal state after:
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : L.Structure M
S : (L.sum L.skolem₁).Substructure M
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥(LHom.sumInl.substructureReduct S)
a : M
h : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
⊢ ∃ b, φ.Realize default (Fin.snoc (Subtype.val ∘ x) ↑b)