mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a b : Σₗ' (i : ι), α i
hab : a < b
⊢ ¬b ≤ a

pp: case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a b : Σₗ' (i : ι), α i
⊢ a ≤ b ∧ ¬b ≤ a → a < b

Tactic:
· rintro (⟨i, a, hji⟩ | ⟨i, hba⟩) <;> obtain ⟨_, _, hij⟩ | ⟨_, hab⟩ := hab
        · exact hij.not_gt hji
        · exact lt_irrefl _ hji
        · exact lt_irrefl _ hij
        · exact hab.not_ge hba

Goal state after:
case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a b : Σₗ' (i : ι), α i
⊢ a ≤ b ∧ ¬b ≤ a → a < b
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderTop ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderTop (α ⊤)
x✝ : Σₗ' (i : ι), α i
a : ι
b : α a
⊢ ⟨a, b⟩ ≤ ⟨⊤, ⊤⟩

Tactic:
obtain rfl | ha := eq_top_or_lt_top a
    · exact Lex.right _ le_top
    · exact Lex.left _ _ ha

Goal state after:
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: x✝ : XgcdType
u : XgcdType := x✝
h : ¬u.r = 0
this : sizeOf u.step < sizeOf u
⊢ x✝.reduce.v = x✝.v

Tactic:
rw [reduce_b h, flip_v, reduce_v (step u), step_v u h, Prod.swap_swap]

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case mk.mk
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
⊢ r (Quot.mk Mcongr x) (Quot.mk Mcongr y) → Quot.mk Mcongr x = Quot.mk Mcongr y

Tactic:
intro rxy

Goal state after:
case mk.mk
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
⊢ Quot.mk Mcongr x = Quot.mk Mcongr y
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
⊢ ∀ (x : Functor.Comp F₂ F₁ α),
    id (fun p ↦ abs ⟨p.fst.fst, fun x ↦ abs ⟨p.fst.snd x, fun y ↦ p.snd ⟨x, y⟩⟩⟩)
        (id
          (fun y ↦
            ⟨⟨(repr y).fst, fun u ↦ (repr ((repr y).snd u)).fst⟩, id fun x ↦ (repr ((repr y).snd x.fst)).snd x.snd⟩)
          x) =
      x

Tactic:
by
    dsimp [Functor.Comp]
    intro x
    conv =>
      rhs
      rw [← abs_repr x]
    obtain ⟨a, f⟩ := repr x
    dsimp
    congr with x
    rcases h' : repr (f x) with ⟨b, g⟩
    dsimp; rw [← h', abs_repr]

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

Goal state before:
pp: case h1
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
⊢ Computation.LiftRel ?R (s.drop n).destruct (t.drop n).destruct

Tactic:
apply liftRel_dropn_destruct H n

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

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

Tactic:
cases b
    cases dst

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

Goal state before:
pp: α : Type u
l : List α
s : WSeq α
⊢ (Computation.corec
        (fun x ↦
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l, s.think)).destruct =
    Sum.inr
      (Computation.corec
        (fun x ↦
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l, s))

Tactic:
by simp [think]

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

Goal state before:
pp: case refine_2
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
⊢ ∀ {a b : Option (α × WSeq α)},
    a ∈ s.destruct → b ∈ t.destruct → LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) a b

Tactic:
· intro a b ma mb
      rcases a with - | a <;> rcases b with - | b
      · trivial
      · injection mem_unique (Computation.mem_map _ ma) ((h 0 _).2 (Computation.mem_map _ mb))
      · injection mem_unique (Computation.mem_map _ ma) ((h 0 _).2 (Computation.mem_map _ mb))
      · obtain ⟨a, s'⟩ := a
        obtain ⟨b, t'⟩ := b
        injection mem_unique (Computation.mem_map _ ma) ((h 0 _).2 (Computation.mem_map _ mb)) with
          ab
        refine ⟨ab, fun n => ?_⟩
        refine
          (get?_congr (flatten_equiv (Computation.mem_map _ ma)) n).symm.trans
            ((?_ : get? (tail s) n ~ get? (tail t) n).trans
              (get?_congr (flatten_equiv (Computation.mem_map _ mb)) n))
        rw [get?_tail, get?_tail]
        apply h

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

Goal state before:
pp: α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
⊢ ∃ c ∈ S, a ∈ c

Tactic:
by
  suffices
    ∀ C, a ∈ C → ∀ (l : List (Computation α)) (S),
      corec parallel.aux1 (l, S) = C → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c from
    let ⟨c, h1, h2⟩ := this _ h [] S rfl
    ⟨c, h1.resolve_left <| List.not_mem_nil, h2⟩
  let F : List (Computation α) → α ⊕ (List (Computation α)) → Prop := by
    intro l a
    rcases a with a | l'
    · exact ∃ c ∈ l, a ∈ c
    · exact ∀ a', (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
  have lem1 (l) : F l (parallel.aux2 l) := by
    induction l <;> simp only [parallel.aux2, List.foldr]
    case nil =>
      intro a h
      assumption
    case cons c l IH =>
      simp only [parallel.aux2] at IH
      -- Porting note: `revert IH` & `intro IH` are required.
      revert IH
      cases List.foldr (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c)) (Sum.inr List.nil) l <;>
        intro IH <;> simp only
      · rcases IH with ⟨c', cl, ac⟩
        exact ⟨c', List.Mem.tail _ cl, ac⟩
      · rcases h : destruct c with a | c' <;> simp only [rmap]
        · refine ⟨c, List.mem_cons_self, ?_⟩
          rw [destruct_eq_pure h]
          apply ret_mem
        · intro a' h
          rcases h with ⟨d, dm, ad⟩
          rcases List.mem_cons.mp dm with e | dl
          · rw [e] at ad
            refine ⟨c, List.mem_cons_self, ?_⟩
            rw [destruct_eq_think h]
            exact think_mem ad
          · obtain ⟨d, dm⟩ := IH a' ⟨d, dl, ad⟩
            obtain ⟨dm, ad⟩ := dm
            exact ⟨d, List.Mem.tail _ dm, ad⟩
  intro C aC
  -- Porting note: `revert this e'` & `intro this e'` are required.
  apply memRecOn aC <;> [skip; intro C' IH] <;> intro l S e <;> have e' := congr_arg destruct e <;>
    have := lem1 l <;> simp only [parallel.aux1, corec_eq, destruct_pure, destruct_think] at e' <;>
    revert this e' <;> rcases parallel.aux2 l with a' | l' <;> intro this e' <;>
    [injection e' with h'; injection e'; injection e'; injection e' with h']
  · rw [h'] at this
    rcases this with ⟨c, cl, ac⟩
    exact ⟨c, Or.inl cl, ac⟩
  · rcases e : Seq.destruct S with - | a <;> rw [e] at h'
    · exact
        let ⟨d, o, ad⟩ := IH _ _ h'
        let ⟨c, cl, ac⟩ := this a ⟨d, o.resolve_right (WSeq.notMem_nil _), ad⟩
        ⟨c, Or.inl cl, ac⟩
    · obtain ⟨o, S'⟩ := a
      obtain - | c := o <;> simp only at h' <;> rcases IH _ _ h' with ⟨d, dl | dS', ad⟩
      · exact
          let ⟨c, cl, ac⟩ := this a ⟨d, dl, ad⟩
          ⟨c, Or.inl cl, ac⟩
      · refine ⟨d, Or.inr ?_, ad⟩
        rw [Seq.destruct_eq_cons e]
        exact Seq.mem_cons_of_mem _ dS'
      · simp only [List.mem_cons] at dl
        rcases dl with dc | dl
        · rw [dc] at ad
          refine ⟨c, Or.inr ?_, ad⟩
          rw [Seq.destruct_eq_cons e]
          apply Seq.mem_cons
        · exact
            let ⟨c, cl, ac⟩ := this a ⟨d, dl, ad⟩
            ⟨c, Or.inl cl, ac⟩
      · refine ⟨d, Or.inr ?_, ad⟩
        rw [Seq.destruct_eq_cons e]
        exact Seq.mem_cons_of_mem _ dS'

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

Goal state before:
pp: case refine_1
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
h : sumLexLift f₁ f₂ g₁ g₂ a b = ∅
⊢ ∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f₁ a₁ b₁ = ∅

pp: case refine_2
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
h : sumLexLift f₁ f₂ g₁ g₂ a b = ∅
⊢ ∀ (a₁ : α₁) (b₂ : β₂), a = inl a₁ → b = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅

pp: case refine_3
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
h : sumLexLift f₁ f₂ g₁ g₂ a b = ∅
⊢ ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → f₂ a₂ b₂ = ∅

pp: case refine_4
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f₁ a₁ b₁ = ∅) ∧
    (∀ (a₁ : α₁) (b₂ : β₂), a = inl a₁ → b = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
      ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → f₂ a₂ b₂ = ∅
⊢ sumLexLift f₁ f₂ g₁ g₂ a b = ∅

Tactic:
any_goals rintro a b rfl rfl; exact map_eq_empty.1 h

Goal state after:
case refine_2
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
h : sumLexLift f₁ f₂ g₁ g₂ a b = ∅
⊢ ∀ (a₁ : α₁) (b₂ : β₂), a = inl a₁ → b = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅

case refine_4
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f₁ a₁ b₁ = ∅) ∧
    (∀ (a₁ : α₁) (b₂ : β₂), a = inl a₁ → b = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
      ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → f₂ a₂ b₂ = ∅
⊢ sumLexLift f₁ f₂ g₁ g₂ a b = ∅
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) < 1 / |2 ^ (n + 1)|

Tactic:
calc
    _ = dist ((f ^ 2 ^ n) 0 + (f ^ 2 ^ n) 0) ((f ^ 2 ^ n) ((f ^ 2 ^ n) 0)) / |2 ^ (n + 1)| := by
      simp_rw [transnumAuxSeq, Real.dist_eq]
      rw [← abs_div, sub_div, pow_succ, pow_succ', ← two_mul, mul_div_mul_left _ _ (two_ne_zero' ℝ),
        pow_mul, sq, mul_apply]
    _ < _ := by gcongr; exact (f ^ 2 ^ n).dist_map_map_zero_lt (f ^ 2 ^ n)

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

Goal state before:
pp: f g : CircleDeg1Lift
h : Commute f g
⊢ τ (f * g) = τ f + τ g

Tactic:
refine tendsto_nhds_unique ?_
    (f.tendsto_translationNumber_aux.add g.tendsto_translationNumber_aux)

Goal state after:
f g : CircleDeg1Lift
h : Commute f g
⊢ Tendsto (fun x ↦ f.transnumAuxSeq x + g.transnumAuxSeq x) atTop (𝓝 (τ (f * g)))
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Liftˣ
⊢ τ ↑f⁻¹ + τ ↑f = 0

Tactic:
simp [← translationNumber_mul_of_commute (Commute.refl _).units_inv_left]

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

Goal state before:
pp: f : CircleDeg1Lift
n : ℕ
this : 0 < ↑n + 1
⊢ dist ((f ^ (n + 1)) 0) ((↑n + 1) * τ f) ≤ 1

Tactic:
← Nat.cast_add_one

Goal state after:
f : CircleDeg1Lift
n : ℕ
this : 0 < ↑n + 1
⊢ dist ((f ^ (n + 1)) 0) (↑(n + 1) * τ f) ≤ 1
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: G : Type u_1
inst✝¹¹ : Group G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : ContinuousInv G
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : MulAction G X
inst✝³ : ContinuousSMul G X
g : G
hg : DenseRange fun x ↦ g ^ x
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul G X μ
⊢ Ergodic (fun x ↦ g • x) μ

Tactic:
by
  borelize G
  refine ⟨measurePreserving_smul _ _, ⟨fun s hsm hs ↦ ?_⟩⟩
  refine aeconst_of_dense_aestabilizer_smul hsm.nullMeasurableSet (hg.mono ?_)
  rw [← Subgroup.coe_zpowers, SetLike.coe_subset_coe, ← Subgroup.zpowers_inv, Subgroup.zpowers_le,
    MulAction.mem_aestabilizer, ← preimage_smul, hs]

Goal state after:
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
hs : NullMeasurableSet s volume
ι : Type u_1
l : Filter ι
inst✝ : l.NeBot
u : ι → AddCircle T
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[volume] s
hu₂ : Tendsto (addOrderOf ∘ u) l atTop
⊢ s =ᵐ[volume] ∅ ∨ s =ᵐ[volume] univ

Tactic:
set μ := (volume : Measure <| AddCircle T)

Goal state after:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : l.NeBot
u : ι → AddCircle T
hu₂ : Tendsto (addOrderOf ∘ u) l atTop
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[μ] s
⊢ s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] univ
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: case inl
a : ℝ
⊢ Dense ↑(AddSubgroup.closure {a, 0}) ↔ Irrational (a / 0)

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

Tactic:
· rw [pair_comm]
    simpa [← AddSubgroup.zmultiples_eq_closure] using! not_denseRange_zsmul

Goal state after:
case inr
a b : ℝ
hb : b ≠ 0
⊢ Dense ↑(AddSubgroup.closure {a, b}) ↔ Irrational (a / b)
Module: Mathlib.Dynamics.Ergodic.Extreme

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

Tactic:
rw [preimage_compl, hfs]

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
f g : X → X
K : Set X
hK₁ : IsClosed K
hK₂ : IsCompact K
hf : (fixedPoints f)ᶜ ⊆ K
L : Set X
hL₁ : IsClosed L
hL₂ : IsCompact L
hg : (fixedPoints g)ᶜ ⊆ L
⊢ ∃ K, IsClosed K ∧ IsCompact K ∧ (fixedPoints (f ∘ g))ᶜ ⊆ K

Tactic:
refine ⟨K ∪ L, hK₁.union hL₁, hK₂.union hL₂, ?_⟩

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
f g : X → X
K : Set X
hK₁ : IsClosed K
hK₂ : IsCompact K
hf : (fixedPoints f)ᶜ ⊆ K
L : Set X
hL₁ : IsClosed L
hL₂ : IsCompact L
hg : (fixedPoints g)ᶜ ⊆ L
⊢ (fixedPoints (f ∘ g))ᶜ ⊆ K ∪ L
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hfν : AEMeasurable f ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ (μ.withDensity f).rnDeriv ν =ᵐ[ν] fun x ↦ f x * μ.rnDeriv ν x

Tactic:
let μ' := ν.withDensity (μ.rnDeriv ν)
  have hμ'ν : μ' ≪ ν := withDensity_absolutelyContinuous _ _
  have h := rnDeriv_withDensity_left_of_absolutelyContinuous hμ'ν hfν
  have h1 : μ'.rnDeriv ν =ᵐ[ν] μ.rnDeriv ν :=
    Measure.rnDeriv_withDensity _ (Measure.measurable_rnDeriv _ _)
  have h2 : (μ'.withDensity f).rnDeriv ν =ᵐ[ν] (μ.withDensity f).rnDeriv ν := by
    exact rnDeriv_withDensity_withDensity_rnDeriv_left μ ν hf_ne_top
  filter_upwards [h, h1, h2] with x hx hx1 hx2
  rw [← hx2, hx, hx1]

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
s : Set α
α' : Type u_5
ϕ : τ → α' → β
f : Filter τ
g : α → α'
⊢ ω f ϕ (g '' s) = ω f (fun t x ↦ ϕ t (g x)) s

Tactic:
simp only [omegaLimit, image2_image_right]

Goal state after:
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 : IsDynNetIn T ∅ U n ↑s
⊢ ↑s.card = ⊥

Tactic:
replace s_net := subset_empty_iff.1 s_net.1

Goal state after:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
s : Finset X
s_net : ↑s = ∅
⊢ ↑s.card = ⊥
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
inst✝ : U.IsSymm
s : Finset X
h' : ↑(#s) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
y : X
y_F : y ∈ F
h : ∃ y_1 ∈ s, (y, y_1) ∈ dynEntourage T U n
⊢ ∃ y_1, (y_1 ∈ s ∧ ¬y_1 = x) ∧ (y, y_1) ∈ dynEntourage T U n

Tactic:
obtain ⟨z, z_s, hz⟩ := h

Goal state after:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
inst✝ : U.IsSymm
s : Finset X
h' : ↑(#s) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
y : X
y_F : y ∈ F
z : X
z_s : z ∈ s
hz : (y, z) ∈ dynEntourage T U n
⊢ ∃ y_1, (y_1 ∈ s ∧ ¬y_1 = x) ∧ (y, y_1) ∈ dynEntourage T U n
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = (ν.withDensity (μ.rnDeriv ν)).real Set.univ

Tactic:
← Measure.setIntegral_toReal_rnDeriv_eq_withDensity,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = ∫ (x : α) in Set.univ, (μ.rnDeriv ν x).toReal ∂ν
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case inl
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] := minpoly F (x ^ n)
h : p.comp (X ^ n) = 0
h' : p = 0
⊢ False

pp: case inr
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] := minpoly F (x ^ n)
h : p.comp (X ^ n) = 0
h' : eval ((X ^ n).coeff 0) p = 0 ∧ X ^ n = C ((X ^ n).coeff 0)
⊢ False

Tactic:
· exact minpoly.ne_zero (isIntegral_of_mem_solvableByRad (pow_mem hx n)) h'

Goal state after:
case inr
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] := minpoly F (x ^ n)
h : p.comp (X ^ n) = 0
h' : eval ((X ^ n).coeff 0) p = 0 ∧ X ^ n = C ((X ^ n).coeff 0)
⊢ False
Module: Mathlib.ModelTheory.Algebra.Ring.FreeCommRing

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
⊢ Term.realize v (termOfFreeCommRing p) = (FreeCommRing.lift v) p

Tactic:
termOfFreeCommRing

Goal state after:
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
⊢ Term.realize v (Classical.choose ⋯) = (FreeCommRing.lift v) p
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case hq.refine_2
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] := minpoly F (x ^ n)
hp : p.comp (X ^ n) ≠ 0
⊢ Group.IsSolvable (map (algebraMap F p.SplittingField) (p.comp (X ^ n))).Gal

Tactic:
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.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
S : L.Substructure M := { carrier := range (Term.realize Subtype.val), fun_mem := ⋯ }
⊢ ↑((closure L).toFun s) = range (Term.realize Subtype.val)

Tactic:
change _ = (S : Set M)

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
S : L.Substructure M := { carrier := range (Term.realize Subtype.val), fun_mem := ⋯ }
⊢ ↑((closure L).toFun s) = ↑S
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
h : ∀ (n : ℕ) (φ : L.BoundedFormula Empty n) (xs : Fin n → M), φ.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ φ.Realize default xs
⊢ ∀ {n : ℕ} (φ : L.Formula (Fin n)) (x : Fin n → M), φ.Realize (⇑f ∘ x) ↔ φ.Realize x

Tactic:
intro n φ x
    exact φ.realize_relabel_sumInr.symm.trans (_root_.trans (h n _ _) φ.realize_relabel_sumInr)

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝³ : L.Structure M
inst✝² : L.Structure N
inst✝¹ : L.Structure P
S : L.Substructure M
s : Set M
inst✝ : IsEmpty L.Constants
x : M
⊢ ∅ ∈ (closure L).closed

Tactic:
mem_closed_iff

Goal state after:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝³ : L.Structure M
inst✝² : L.Structure N
inst✝¹ : L.Structure P
S : L.Substructure M
s : Set M
inst✝ : IsEmpty L.Constants
x : M
⊢ ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f ∅
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
⊢ f.toHom.range = ⊤

Tactic:
ext n
  simp only [Hom.mem_range, coe_toHom, Substructure.mem_top, iff_true]
  exact ⟨f.symm n, apply_symm_apply _ _⟩

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 ⋯
⊢ ∃ v, M ⊨ equivSentence φ

Tactic:
exists v'

Goal state after:
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 ⋯
⊢ M ⊨ equivSentence φ
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ (Theory.ACF p).IsSatisfiable

Tactic:
cases hp with

Goal state after: