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

Goal state before:
pp: case fs
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✝ : Fin2 n
j : (P F).B a a✝.fs
⊢ α.RelLast R ((P F).appendContents f' f₀ a✝.fs j) ((P F).appendContents f' f₁ a✝.fs j)

Tactic:
apply Eq.refl

Goal state after:
Module: Mathlib.Data.Rat.Star

Goal state before:
pp: ⊢ closure (range fun x ↦ x * x) = nonneg ℚ

Tactic:
simpa only [sq] using addSubmonoid_closure_range_pow two_ne_zero even_two

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

Goal state before:
pp: F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α β : Type u
f : α → β
a :
  { A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A), B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.A
g :
  { A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A), B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.B
      a →
    α
⊢ abs
      ⟨({ A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A),
                  B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.map
              f ⟨a, g⟩).fst.fst,
        fun x ↦
        abs
          ⟨({ A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A),
                        B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.map
                    f ⟨a, g⟩).fst.snd
              x,
            fun y ↦
            ({ A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A),
                      B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.map
                  f ⟨a, g⟩).snd
              ⟨x, y⟩⟩⟩ =
    f <$> abs ⟨a.fst, fun x ↦ abs ⟨a.snd x, fun y ↦ g ⟨x, y⟩⟩⟩

Tactic:
obtain ⟨b, h⟩ := a

Goal state after:
F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α β : Type u
f : α → β
b : (P F₂).A
h : (P F₂).B b → (P F₁).A
g :
  { A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A), B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.B
      ⟨b, h⟩ →
    α
⊢ abs
      ⟨({ A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A),
                  B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.map
              f ⟨⟨b, h⟩, g⟩).fst.fst,
        fun x ↦
        abs
          ⟨({ A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A),
                        B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.map
                    f ⟨⟨b, h⟩, g⟩).fst.snd
              x,
            fun y ↦
            ({ A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A),
                      B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.map
                  f ⟨⟨b, h⟩, g⟩).snd
              ⟨x, y⟩⟩⟩ =
    f <$> abs ⟨⟨b, h⟩.fst, fun x ↦ abs ⟨⟨b, h⟩.snd x, fun y ↦ g ⟨x, y⟩⟩⟩
Module: Mathlib.Data.QPF.Univariate.Basic

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

Tactic:
rintro α p ⟨a, f⟩
    have h' := h
    rw [suppPreservation_iff_uniform] at h'
    dsimp only [SuppPreservation, supp] at h
    rw [liftp_iff_of_isUniform h', supp_eq_of_isUniform h', PFunctor.liftp_iff']
    simp

Goal state after:
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 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'

Tactic:
revert 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 : s.think = c
⊢ (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' →
    s ∈ l'
Module: Mathlib.Data.WSeq.Relation

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

Tactic:
let ⟨n, h⟩ := exists_get?_of_mem h
  let ⟨some (_, s'), sd, rfl⟩ := Computation.exists_of_mem_map h
  let ⟨some (b, t'), td, ⟨ab, _⟩⟩ := (liftRel_dropn_destruct H n).left sd
  exact ⟨b, get?_mem (Computation.mem_map (Prod.fst.{v, v} <$> ·) td), ab⟩

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
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'
⊢ (corec parallel.aux1 (l, S)).destruct = Sum.inr ?m.158

Tactic:
by
        simp only [corec_eq, rmap, parallel.aux1.eq_1]
        rw [h, H]

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

Goal state before:
pp: α : Type u
s : Seq α
⊢ (↑s).head = Computation.pure s.head

Tactic:
simp only [head, Option.map_eq_map, destruct_ofSeq, Computation.map_pure, Option.map_map]

Goal state after:
α : Type u
s : Seq α
⊢ Computation.pure (Option.map (Prod.fst ∘ fun a ↦ (a, ↑s.tail)) s.head) = Computation.pure s.head
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : Seq α
⊢ (↑s).head = Computation.pure s.head

Tactic:
by
  simp only [head, Option.map_eq_map, destruct_ofSeq, Computation.map_pure, Option.map_map]
  cases Seq.head s <;> rfl

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

Goal state before:
pp: case mp
ι : 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
x✝¹ : i = k
x✝ : ⋯ ▸ a ≤ c
⊢ (∃ (x : j = k), c ≤ ⋯ ▸ b) → ∃ (h : k = j), ⋯ ▸ c ≤ b

Tactic:
rintro ⟨⟨⟩, ht⟩

Goal state after:
case mp
ι : 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 c : α j
x✝¹ : i = j
x✝ : ⋯ ▸ a ≤ c
ht : c ≤ ⋯ ▸ b
⊢ ∃ (h : j = j), ⋯ ▸ c ≤ b
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: case mpr
ι : 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
x✝¹ : i = k
x✝ : ⋯ ▸ a ≤ c
⊢ (∃ (h : k = j), ⋯ ▸ c ≤ b) → ∃ (x : j = k), c ≤ ⋯ ▸ b

Tactic:
rintro ⟨⟨⟩, ht⟩

Goal state after:
case mpr
ι : 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 c : α j
x✝¹ : i = j
x✝ : ⋯ ▸ a ≤ c
ht : ⋯ ▸ c ≤ b
⊢ ∃ (x : j = j), c ≤ ⋯ ▸ b
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: case mp
ι : 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
x✝¹ : i = k
x✝ : ⋯ ▸ a ≤ c
⊢ (∃ (x : j = k), c < ⋯ ▸ b) → ∃ (h : k = j), ⋯ ▸ c < b

Tactic:
rintro ⟨⟨⟩, ht⟩

Goal state after:
case mp
ι : 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 c : α j
x✝¹ : i = j
x✝ : ⋯ ▸ a ≤ c
ht : c < ⋯ ▸ b
⊢ ∃ (h : j = j), ⋯ ▸ c < b
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: case mpr
ι : 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
x✝¹ : i = k
x✝ : ⋯ ▸ a ≤ c
⊢ (∃ (h : k = j), ⋯ ▸ c < b) → ∃ (x : j = k), c < ⋯ ▸ b

Tactic:
rintro ⟨⟨⟩, ht⟩

Goal state after:
case mpr
ι : 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 c : α j
x✝¹ : i = j
x✝ : ⋯ ▸ a ≤ c
ht : ⋯ ▸ c < b
⊢ ∃ (x : j = j), c < ⋯ ▸ b
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: case mp
ι : 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
x✝¹ : i = k
x✝ : ⋯ ▸ a < c
⊢ (∃ (x : j = k), c ≤ ⋯ ▸ b) → ∃ (h : k = j), ⋯ ▸ c ≤ b

Tactic:
rintro ⟨⟨⟩, ht⟩

Goal state after:
case mp
ι : 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 c : α j
x✝¹ : i = j
x✝ : ⋯ ▸ a < c
ht : c ≤ ⋯ ▸ b
⊢ ∃ (h : j = j), ⋯ ▸ c ≤ b
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: case mpr
ι : 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
x✝¹ : i = k
x✝ : ⋯ ▸ a < c
⊢ (∃ (h : k = j), ⋯ ▸ c ≤ b) → ∃ (x : j = k), c ≤ ⋯ ▸ b

Tactic:
rintro ⟨⟨⟩, ht⟩

Goal state after:
case mpr
ι : 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 c : α j
x✝¹ : i = j
x✝ : ⋯ ▸ a < c
ht : ⋯ ▸ c ≤ b
⊢ ∃ (x : j = j), c ≤ ⋯ ▸ b
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: case mp
ι : 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
x✝¹ : i = k
x✝ : ⋯ ▸ a < c
⊢ (∃ (x : j = k), c < ⋯ ▸ b) → ∃ (h : k = j), ⋯ ▸ c < b

Tactic:
rintro ⟨⟨⟩, ht⟩

Goal state after:
case mp
ι : 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 c : α j
x✝¹ : i = j
x✝ : ⋯ ▸ a < c
ht : c < ⋯ ▸ b
⊢ ∃ (h : j = j), ⋯ ▸ c < b
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: case mpr
ι : 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
x✝¹ : i = k
x✝ : ⋯ ▸ a < c
⊢ (∃ (h : k = j), ⋯ ▸ c < b) → ∃ (x : j = k), c < ⋯ ▸ b

Tactic:
rintro ⟨⟨⟩, ht⟩

Goal state after:
case mpr
ι : 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 c : α j
x✝¹ : i = j
x✝ : ⋯ ▸ a < c
ht : ⋯ ▸ c < b
⊢ ∃ (x : j = j), c < ⋯ ▸ b
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : 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
a : α
s : WSeq α
b : β
t : WSeq β
h1 : R a b
h2 : LiftRel R s t
⊢ Computation.LiftRel
    (LiftRelO R 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)
    (destruct_append.aux S.join (some (a, s))) (destruct_append.aux T.join (some (b, t)))

Tactic:
by
        simpa using ⟨h1, s, t, S, rfl, T, rfl, h2, ST⟩

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

Goal state before:
pp: case refl.refl.left
α : 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 α)) := ⋯
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
c' : Computation α
ad' : (a, c) ∈ map (fun a ↦ (a, c')) c'
cs' : c' ∈ S
e' : map (fun a ↦ (a, c')) c' = d'
a' : α
ac' : a' ∈ c'
i1 : a' = a
i2 : c' = c
⊢ a ∈ c

Tactic:
rwa [i1, i2] at ac'

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

Goal state before:
pp: α : Type u
S : WSeq (Computation α)
a : α
H : ∀ s ∈ S, s ~> a
c : Computation α
cs : c ∈ S
ac : a ∈ c
⊢ a ∈ parallel S

Tactic:
have := terminates_of_mem ac
  have := terminates_parallel cs
  exact mem_of_promises _ (parallel_promises H)

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

Goal state before:
pp: α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ s.Productive ↔ t.Productive

Tactic:
by
  simp only [productive_iff]; exact forall_congr' fun n => terminates_congr <| get?_congr h _

Goal state after:
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
x : ℝ
g : G
this : τ (f₂ g⁻¹) = -τ (f₂ g)
⊢ x + τ (f₂ g) + τ (f₂ g⁻¹) + 1 + 1 = x + 2

Tactic:
simp [this, add_assoc, one_add_one_eq_two]

Goal state after:
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
hμT : μ T ≠ 0
hTm : NullMeasurableSet T μ
x : α
hxt : x ∈ T
m : ℕ
hm₀ : m ≠ 0
hmt : f^[m] x ∈ T
⊢ False

Tactic:
refine hxt.2 <| mem_iUnion₂.2 ⟨N + m, ?_, hxt.1.1, ?_⟩

Goal state after:
case refine_1
α : 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
hμT : μ T ≠ 0
hTm : NullMeasurableSet T μ
x : α
hxt : x ∈ T
m : ℕ
hm₀ : m ≠ 0
hmt : f^[m] x ∈ T
⊢ N + m > N

case refine_2
α : 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
hμT : μ T ≠ 0
hTm : NullMeasurableSet T μ
x : α
hxt : x ∈ T
m : ℕ
hm₀ : m ≠ 0
hmt : f^[m] x ∈ T
⊢ x ∈ f^[N + m] ⁻¹' s
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
inst✝ : IsFiniteMeasure μ
hμ : Ergodic f μ
⊢ μ ∈ extremePoints ℝ≥0∞ {ν | MeasurePreserving f ν ν ∧ ν univ = μ univ}

Tactic:
mem_extremePoints_iff_left

Goal state after:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
inst✝ : IsFiniteMeasure μ
hμ : Ergodic f μ
⊢ μ ∈ {ν | MeasurePreserving f ν ν ∧ ν univ = μ univ} ∧
    ∀ x₁ ∈ {ν | MeasurePreserving f ν ν ∧ ν univ = μ univ},
      ∀ x₂ ∈ {ν | MeasurePreserving f ν ν ∧ ν univ = μ univ}, μ ∈ openSegment ℝ≥0∞ x₁ x₂ → x₁ = μ
Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage

Goal state before:
pp: X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Function.Semiconj φ S T
U : Set (Y × Y)
n k : ℕ
x✝ : k < n
⊢ map T^[k] T^[k] ∘ map φ φ ⁻¹' U = map φ φ ∘ map S^[k] S^[k] ⁻¹' U

Tactic:
map_comp_map,

Goal state after:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Function.Semiconj φ S T
U : Set (Y × Y)
n k : ℕ
x✝ : k < n
⊢ map (T^[k] ∘ φ) (T^[k] ∘ φ) ⁻¹' U = map φ φ ∘ map S^[k] S^[k] ⁻¹' U
Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage

Goal state before:
pp: X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Function.Semiconj φ S T
U : Set (Y × Y)
n k : ℕ
x✝ : k < n
⊢ map (T^[k] ∘ φ) (T^[k] ∘ φ) ⁻¹' U = map φ φ ∘ map S^[k] S^[k] ⁻¹' U

Tactic:
map_comp_map,

Goal state after:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Function.Semiconj φ S T
U : Set (Y × Y)
n k : ℕ
x✝ : k < n
⊢ map (T^[k] ∘ φ) (T^[k] ∘ φ) ⁻¹' U = map (φ ∘ S^[k]) (φ ∘ S^[k]) ⁻¹' U
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
h' : UniformContinuous φ
F : Set X
⊢ coverEntropyInf T (φ '' F) ≤ coverEntropyInf S F

Tactic:
coverEntropyInf_image_of_comap _ h F

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
h' : UniformContinuous φ
F : Set X
⊢ coverEntropyInf S F ≤ coverEntropyInf S F
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᵐ[ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun x ↦ 1) x
a : α
h4 : (μ + ν).rnDeriv (μ + ν) a = (μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)) a
h5 : (μ + ν).rnDeriv (μ + ν) a = 1
h6 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
⊢ μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹

Tactic:
rw [h5, Pi.add_apply] at h4

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᵐ[ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun x ↦ 1) x
a : α
h4 : 1 = μ.rnDeriv (μ + ν) a + ν.rnDeriv (μ + ν) a
h5 : (μ + ν).rnDeriv (μ + ν) a = 1
h6 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
⊢ μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᵐ[ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun x ↦ 1) x
this : μ.rnDeriv (μ + ν) =ᵐ[ν] fun x ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹
⊢ μ.rnDeriv (μ + ν) =ᵐ[ν] fun x ↦ μ.rnDeriv ν x / (μ.rnDeriv ν x + 1)

Tactic:
filter_upwards [this, μ.rnDeriv_lt_top ν] with a ha ha_lt_top

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᵐ[ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun x ↦ 1) x
this : μ.rnDeriv (μ + ν) =ᵐ[ν] fun x ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹
a : α
ha : μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹
ha_lt_top : μ.rnDeriv ν a < ∞
⊢ μ.rnDeriv (μ + ν) a = μ.rnDeriv ν a / (μ.rnDeriv ν a + 1)
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: case inr.inl
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
hF : coverMincard T F U n < ⊤
hG : coverMincard T G U n = ⊤
⊢ coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n

Tactic:
rw [hG, add_top]; exact le_top

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : (map (algebraMap F q.SplittingField) p).Splits
hp : Group.IsSolvable p.Gal
hq : Group.IsSolvable (map (algebraMap F p.SplittingField) q).Gal
⊢ Group.IsSolvable q.Gal

Tactic:
let K := p.SplittingField

Goal state after:
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : (map (algebraMap F q.SplittingField) p).Splits
hp : Group.IsSolvable p.Gal
hq : Group.IsSolvable (map (algebraMap F p.SplittingField) q).Gal
K : Type u_1 := p.SplittingField
⊢ Group.IsSolvable q.Gal
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
⊢ Nonempty (K ≃+* L)

Tactic:
obtain ⟨t, ht⟩ := exists_isTranscendenceBasis ℤ L

Goal state after:
K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
⊢ Nonempty (K ≃+* 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
hnp : N ↪[L] P
hmn : M ↪[L] N
n✝ : ℕ
r✝ : L.Relations n✝
x✝ : Fin n✝ → M
⊢ RelMap r✝ ((⇑hnp ∘ ⇑hmn) ∘ x✝) ↔ RelMap r✝ x✝

Tactic:
Function.comp_assoc,

Goal state after:
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
hnp : N ↪[L] P
hmn : M ↪[L] N
n✝ : ℕ
r✝ : L.Relations n✝
x✝ : Fin n✝ → M
⊢ RelMap r✝ (⇑hnp ∘ ⇑hmn ∘ x✝) ↔ RelMap r✝ x✝
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
hnp : N ≃[L] P
hmn : M ≃[L] N
n✝ : ℕ
r✝ : L.Relations n✝
x✝ : Fin n✝ → M
⊢ RelMap r✝ ((⇑hnp ∘ ⇑hmn) ∘ x✝) ↔ RelMap r✝ x✝

Tactic:
Function.comp_assoc,

Goal state after:
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
hnp : N ≃[L] P
hmn : M ≃[L] N
n✝ : ℕ
r✝ : L.Relations n✝
x✝ : Fin n✝ → M
⊢ RelMap r✝ (⇑hnp ∘ ⇑hmn ∘ x✝) ↔ RelMap r✝ x✝