mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ (Ordnode.node s l x r) o₂
⊢ Valid' o₁ (l.node' x r).eraseMax ↑(findMax' x r) ∧ (l.node' x r).size = (l.node' x r).eraseMax.size + 1

Tactic:
by
  have := H.2.eq_node'; rw [this] at H; clear this
  induction r generalizing l x o₁ with
  | nil => exact ⟨H.left, rfl⟩
  | node rs rl rx rr _ IHrr =>
    have := H.2.2.2.eq_node'; rw [this] at H ⊢
    rcases IHrr H.right with ⟨h, e⟩
    refine ⟨Valid'.balanceL H.left h (Or.inr ⟨_, Or.inr e, H.3.1⟩), ?_⟩
    rw [eraseMax, size_balanceL H.3.2.1 h.3 H.2.2.1 h.2 (Or.inr ⟨_, Or.inr e, H.3.1⟩)]
    rw [size_node, e]; rfl

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil.node.node.node
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
⊢ (if rls < ratio * rrs then
      node (rls + rrs + 1 + 1) (node (rls + 1) nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
    else
      node (rls + rrs + 1 + 1) (node (rll.size + 1) nil x rll) rlx
        (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))) =
    if 0 + (rls + rrs + 1) ≤ 1 then nil.node' x ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr))
    else nil.rotateL x ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr))

Tactic:
· symm; rw [zero_add, if_neg, rotateL]
        · dsimp only [size_node]; split_ifs
          · simp [node3L, node']; abel
          · simp [node4L, node', sr.2.1.1]; abel
        · exact not_le_of_gt (Nat.succ_lt_succ (add_pos sr.2.1.pos sr.2.2.pos))

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case mpr.inl
n : ℕ
h₁ : n ≤ n
h₂ : n ≤ n + 1
⊢ Raised n n

pp: case mpr.inr
n m : ℕ
h₁✝ : n ≤ m
h₂ : m ≤ n + 1
h₁ : n < m
⊢ Raised n m

Tactic:
· exact Or.inl rfl

Goal state after:
case mpr.inr
n m : ℕ
h₁✝ : n ≤ m
h₂ : m ≤ n + 1
h₁ : n < m
⊢ Raised n m
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case inl
k m : ℕ
⊢ Raised (k + m) (k + m)

pp: case inr
k n : ℕ
⊢ Raised (k + n) (k + (n + 1))

Tactic:
· exact Or.inl rfl

Goal state after:
case inr
k n : ℕ
⊢ Raised (k + n) (k + (n + 1))
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case inl
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
⊢ Raised (l.size + r₁.size + 1) (l.size + r₁.size + 1)

pp: case inr
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
⊢ Raised (l.size + r₁.size + 1) (l.size + (r₁.size + 1) + 1)

Tactic:
· exact Or.inl rfl

Goal state after:
case inr
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
⊢ Raised (l.size + r₁.size + 1) (l.size + (r₁.size + 1) + 1)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mk.mk
F : Type u → Type u
q : QPF F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
x✝ : Fix F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), g₁ (Quot.mk (⇑Wsetoid) (f a)) = g₂ (Quot.mk (⇑Wsetoid) (f a))
⊢ g₁ ⟦WType.mk a f⟧ = g₂ ⟦WType.mk a f⟧

Tactic:
← Fix.ind_aux a f

Goal state after:
case mk.mk
F : Type u → Type u
q : QPF F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
x✝ : Fix F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), g₁ (Quot.mk (⇑Wsetoid) (f a)) = g₂ (Quot.mk (⇑Wsetoid) (f a))
⊢ g₁ (mk (abs ⟨a, fun x ↦ ⟦f x⟧⟩)) = g₂ (mk (abs ⟨a, fun x ↦ ⟦f x⟧⟩))
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mk.mk
F : Type u → Type u
q : QPF F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
x✝ : Fix F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), p (Quot.mk (⇑Wsetoid) (f a))
⊢ p ⟦WType.mk a f⟧

Tactic:
← Fix.ind_aux a f

Goal state after:
case mk.mk
F : Type u → Type u
q : QPF F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
x✝ : Fix F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), p (Quot.mk (⇑Wsetoid) (f a))
⊢ p (mk (abs ⟨a, fun x ↦ ⟦f x⟧⟩))
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ (f ⊚ TypeVec.id) <$$> x = f <$$> x ∧ (prod.snd ⊚ subtypeVal R) <$$> h <$$> x = g <$$> x

Tactic:
rw [MvFunctor.map_map, comp_assoc, hh, ← comp_assoc, snd_prod_mk, comp_assoc, snd_diag]

Goal state after:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ (f ⊚ TypeVec.id) <$$> x = f <$$> x ∧ (g ⊚ TypeVec.id) <$$> x = g <$$> x
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: r : ℝ
hr : 0 < r
⊢ r.sign = 1

Tactic:
rw [sign, if_pos hr, if_neg hr.not_gt]

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

Goal state before:
pp: case some.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
b : Option (α × WSeq α)
hb : b ∈ t.destruct
a : α × WSeq α
ha : some a ∈ s.destruct
t1 : LiftRelO R (LiftRel R) (some a) b
c : α × WSeq α
hc : some c ∈ u.destruct
t2 : LiftRelO R (LiftRel R) b (some c)
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) (some a) (some c)

Tactic:
obtain ⟨a, s⟩ := a
    rcases b with - | b
    · cases t1
    obtain ⟨b, t⟩ := b
    obtain ⟨c, u⟩ := c
    obtain ⟨ab, st⟩ := t1
    obtain ⟨bc, tu⟩ := t2
    exact ⟨trans_of R ab bc, t, st, tu⟩

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

Goal state before:
pp: α : 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
⊢ Computation.LiftRel (LiftRelO Eq fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s.destruct t.destruct

Tactic:
refine liftRel_def.2 ⟨?_, ?_⟩

Goal state after:
case refine_1
α : 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
⊢ s.destruct.Terminates ↔ t.destruct.Terminates

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
Module: Mathlib.Data.Sigma.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

Tactic:
rintro (⟨b, a, hji⟩ | ⟨b, a, hba⟩) <;> obtain ⟨_, _, hij⟩ | ⟨_, _, hab⟩ := hab

Goal state after:
case refine_1.left.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i✝ j✝ : ι
b : α i✝
a : α j✝
hji : i✝ < j✝
hij : j✝ < i✝
⊢ False

case refine_1.left.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i✝ : ι
b a : α i✝
hji : i✝ < i✝
hab : a < b
⊢ False

case refine_1.right.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i✝ : ι
b a : α i✝
hba : b ≤ a
hij : i✝ < i✝
⊢ False

case refine_1.right.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i✝ : ι
b a : α i✝
hba : b ≤ a
hab : a < b
⊢ False
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: case refine_2.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i✝ : ι
a b : α i✝
hab : a ≤ b
hba : ¬⟨i✝, b⟩ ≤ ⟨i✝, a⟩
⊢ ⟨i✝, a⟩ < ⟨i✝, b⟩

Tactic:
exact Sigma.Lex.right _ _ (hab.lt_of_not_ge fun h => hba <| Sigma.Lex.right _ _ h)

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

Goal state before:
pp: case neg
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : ¬c₁ = c₂
⊢ c₁ < c₂ ↔ c₁ :: cs₁ < c₂ :: cs₂

Tactic:
refine ⟨List.Lex.rel, fun e ↦ ?_⟩
      cases e <;> rename_i h'
      · assumption
      · contradiction

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

Goal state before:
pp: case h2.inr.some.none.inl
α : Type u
S✝ : WSeq (Computation α)
a : α
h : a ∈ parallel S✝
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e✝ : corec parallel.aux1 (l, S) = C'.think
l' : List (Computation α)
this : F l (Sum.inr l')
S' : Stream'.Seq (Option (Computation α))
h' : corec parallel.aux1 (l', S') = C'
e : Seq.destruct S = some (none, S')
d : Computation α
ad : a ∈ d
dl : d ∈ l'
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
exact
          let ⟨c, cl, ac⟩ := this a ⟨d, dl, ad⟩
          ⟨c, Or.inl cl, ac⟩

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

Goal state before:
pp: case cons
α : Type u
β : Type v
f : α → β
S✝ : WSeq (Computation α)
c1 c2 : Computation β
h : ∃ l S, c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
S : WSeq (Computation α)
head✝ : Computation α
tail✝ : List (Computation α)
tail_ih✝ :
  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 []) (List.map (map f) tail✝) =
    match
      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 []) tail✝ with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (List.map (map f) b) with
    | Sum.inl a => Sum.inl (f a)
    | Sum.inr b => Sum.inr b
⊢ 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 []) (List.map (map f) (head✝ :: tail✝)) =
    match
      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 []) (head✝ :: tail✝) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (List.map (map f) b) with
    | Sum.inl a => Sum.inl (f a)
    | Sum.inr b => Sum.inr b

Tactic:
grind [destruct_map, lmap, rmap]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
this : MeasurePreserving (⇑e ∘ f ∘ ⇑e.symm) μ' μ' ↔ MeasurePreserving f μ μ
h : PreErgodic (⇑e ∘ f ∘ ⇑e.symm) μ' ↔ PreErgodic f μ
⊢ Ergodic (⇑e ∘ f ∘ ⇑e.symm) μ' ↔ Ergodic f μ

Tactic:
exact ⟨fun hf => { this.mp hf.toMeasurePreserving, h.mp hf.toPreErgodic with },
    fun hf => { this.mpr hf.toMeasurePreserving, h.mpr hf.toPreErgodic with }⟩

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : Ergodic f μ
hs : NullMeasurableSet s μ
hs' : s ≤ᵐ[μ] f ⁻¹' s
h_fin : μ (f ⁻¹' s) ≠ ∞
⊢ f ⁻¹' s =ᵐ[μ] s

Tactic:
exact (ae_eq_of_ae_subset_of_measure_ge hs' (hf.measure_preimage hs).le hs h_fin).symm

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

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
⊢ f (fract x) - fract x = f x - x

Tactic:
Int.fract,

Goal state after:
f : CircleDeg1Lift
x : ℝ
⊢ f (x - ↑⌊x⌋) - (x - ↑⌊x⌋) = f x - x
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C
n : ℕ
⊢ dist (f.transnumAuxSeq n) (x (2 ^ n) / 2 ^ n) ≤ C / 2 ^ n

Tactic:
have : 0 < (2 ^ n : ℝ) := pow_pos zero_lt_two _

Goal state after:
f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C
n : ℕ
this : 0 < 2 ^ n
⊢ dist (f.transnumAuxSeq n) (x (2 ^ n) / 2 ^ n) ≤ C / 2 ^ n
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
hf : Continuous ⇑f
z : ℝ
hz : ∀ (x : ℝ), f x < x + z
x : ℝ
hx : ∀ y ∈ Icc 0 1, f y - y ≤ f x - x
⊢ τ f < z

Tactic:
refine lt_of_le_of_lt ?_ (sub_lt_iff_lt_add'.2 <| hz x)

Goal state after:
f : CircleDeg1Lift
hf : Continuous ⇑f
z : ℝ
hz : ∀ (x : ℝ), f x < x + z
x : ℝ
hx : ∀ y ∈ Icc 0 1, f y - y ≤ f x - x
⊢ τ f ≤ f x - x
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: case mpr
p : ℝ
inst✝ : Fact (0 < p)
s : AddSubgroup (AddCircle p)
h : ¬Dense ↑s
⊢ ∃ a, addOrderOf a ≠ 0 ∧ s = AddSubgroup.zmultiples a

Tactic:
obtain ⟨a, rfl⟩ : ∃ a, s = .zmultiples a := by
      rw [← QuotientAddGroup.dense_preimage_mk, ← QuotientAddGroup.coe_mk',
        ← AddSubgroup.coe_comap, xor_iff_not_iff'.1 (AddSubgroup.dense_xor_cyclic _)] at h
      rcases h with ⟨a, ha⟩
      use a
      rw [← QuotientAddGroup.coe_mk', ← AddMonoidHom.map_zmultiples, ← ha,
        AddSubgroup.map_comap_eq_self_of_surjective]
      exact Quot.mk_surjective

Goal state after:
case mpr
p : ℝ
inst✝ : Fact (0 < p)
a : AddCircle p
h : ¬Dense ↑(AddSubgroup.zmultiples a)
⊢ ∃ a_1, addOrderOf a_1 ≠ 0 ∧ AddSubgroup.zmultiples a = AddSubgroup.zmultiples a_1
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
n : ℕ
⊢ μ {x | x ∈ s ∧ ∀ m ≥ n, f^[m] x ∉ s} = 0

Tactic:
by_contra H
  have : NullMeasurableSet (s ∩ { x | ∀ m ≥ n, f^[m] x ∉ s }) μ := by
    simp only [ofPred_forall, ← compl_ofPred]
    exact hs.inter <| .biInter (to_countable _) fun m _ ↦
      (hs.preimage <| hf.toQuasiMeasurePreserving.iterate m).compl
  rcases (hf.exists_gt_measure_inter_ne_zero this H) n with ⟨m, hmn, hm⟩
  rcases nonempty_of_measure_ne_zero hm with ⟨x, ⟨_, hxn⟩, hxm, -⟩
  exact hxn m hmn.lt.le hxm

Goal state after:
Module: Mathlib.Topology.Order.CountableSeparating

Goal state before:
pp: case refine_2
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}
⊢ ∀ s ∈ Iio '' t, s ∈ range Iio

Tactic:
exact image_subset_range _ _

Goal state after:
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Inhabited A
G : Type u_2
inst✝² : Monoid G
inst✝¹ : IsLeftCancelMul G
inst✝ : DiscreteTopology A
p : Pattern A G
g : G
⊢ IsOpen[Pi.topologicalSpace] {x | p.mulOccursInAt x g}

Tactic:
by
  simpa [mulOccursInAt_eq_cylinder] using isOpen_cylinder _ _

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 α
y : β
⊢ y ∈ ω f ϕ s ↔ ∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, (s ∩ ϕ t ⁻¹' n).Nonempty

Tactic:
by
  simp_rw [frequently_iff, omegaLimit_def, mem_iInter, mem_closure_iff_nhds]
  constructor
  · intro h _ hn _ hu
    rcases h _ hu _ hn with ⟨_, _, _, ht, _, hx, rfl⟩
    exact ⟨_, ht, _, hx, by rwa [mem_preimage]⟩
  · intro h _ hu _ hn
    rcases h _ hn hu with ⟨_, ht, _, hx, hϕtx⟩
    exact ⟨_, hϕtx, _, ht, _, hx, rfl⟩

Goal state after:
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_3
G : Type u_4
inst✝¹ : Finite A
inst✝ : Inhabited A
U : Finset G
val✝ : Fintype A
f : ↥U → A
i : ↥U
⊢ (fun p i ↦ (↑p).config ↑i)
      ((fun f ↦ ⟨{ config := fun g ↦ if h : g ∈ U then f ⟨g, h⟩ else default, support := U, condition := ⋯ }, ⋯⟩) f) i =
    f i

Tactic:
simp [i.2]

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 α
v : Set τ
hv : v ∈ f
⊢ ω f ϕ s = ⋂ u, closure[inst✝] (image2 ϕ (↑u ∩ v) s)

Tactic:
by
  rw [omegaLimit_eq_biInter_inter _ _ _ hv]
  apply biInter_eq_iInter

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 α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst✝] n
v : Set τ
hn₂ : ⋂ u, closure[inst✝] (image2 ϕ (↑u ∩ v) s) ⊆ n
hv₁ : v ∈ f
hv₂ : closure[inst✝] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst✝] (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u ↦ (closure[inst✝] (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen[inst✝] (j u)
this : ⋃ u ∈ f, j u = ⋃ u, j ↑u
⊢ ⋂ i, k \ j ↑i ⊆ n

Tactic:
j,

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst✝] n
v : Set τ
hn₂ : ⋂ u, closure[inst✝] (image2 ϕ (↑u ∩ v) s) ⊆ n
hv₁ : v ∈ f
hv₂ : closure[inst✝] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst✝] (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u ↦ (closure[inst✝] (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen[inst✝] (j u)
this : ⋃ u ∈ f, j u = ⋃ u, j ↑u
⊢ ⋂ i, k \ (closure[inst✝] (image2 ϕ (↑i ∩ v) s))ᶜ ⊆ n
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 : ℕ
V : SetRel X X
hV : V ∈ 𝓤 X
hVsymm : V.IsSymm
hVU : V ⊆ U
uni_ite : dynEntourage T V n ∈ 𝓤 X
⊢ ∃ s, IsDynCoverOf T F U n ↑s

Tactic:
let openCover x := ball x (dynEntourage T V n)

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
uni_ite : dynEntourage T V n ∈ 𝓤 X
openCover : X → Set X := fun x ↦ ball x (dynEntourage T V n)
⊢ ∃ s, IsDynCoverOf T F U n ↑s
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: case inr
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
n : ℕ
h : coverMincard T F U n < ⊤
t : Finset X
t_cover : IsDynCoverOf T F U n ↑t
t_mincard : ↑t.card = coverMincard T F U n
⊢ netMaxcard T F U n ≤ coverMincard T F U n

Tactic:
← t_mincard

Goal state after:
case inr
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
n : ℕ
h : coverMincard T F U n < ⊤
t : Finset X
t_cover : IsDynCoverOf T F U n ↑t
t_mincard : ↑t.card = coverMincard T F U n
⊢ netMaxcard T F U n ≤ ↑t.card
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case h₂
F : Type u_1
inst✝ : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, Group.IsSolvable p.Gal
p : F[X]
t : Multiset F[X]
hps : p ∈ s
a✝ : t ⊆ s
⊢ Group.IsSolvable t.prod.Gal → Group.IsSolvable (insert p t).prod.Gal

Tactic:
ht

Goal state after:
case h₂
F : Type u_1
inst✝ : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, Group.IsSolvable p.Gal
p : F[X]
t : Multiset F[X]
hps : p ∈ s
a✝ : t ⊆ s
ht : Group.IsSolvable t.prod.Gal
⊢ Group.IsSolvable (insert p t).prod.Gal
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
c : (X ^ n - C a).SplittingField
hc : c ^ n = 1
⊢ c ^ n = (aeval c) 1

Tactic:
aeval_one

Goal state after:
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
c : (X ^ n - C a).SplittingField
hc : c ^ n = 1
⊢ c ^ n = 1
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
this✝¹ : SigmaFinite (map f ν)
this✝ : SigmaFinite (map f (μ.singularPart ν))
this : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν)))
h_add :
  (fun x ↦ (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν] fun x ↦
    ((map f (μ.singularPart ν)).rnDeriv (map f ν) + (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν)) (f x)
⊢ (μ.singularPart ν).rnDeriv ν =ᵐ[ν] fun x ↦ (map f (μ.singularPart ν)).rnDeriv (map f ν) (f x)

Tactic:
refine (Measure.rnDeriv_singularPart μ ν).trans ?_
    symm
    suffices (fun x ↦ ((μ.singularPart ν).map f).rnDeriv (ν.map f) x) =ᵐ[ν.map f] 0 by
      rw [Filter.EventuallyEq, hf.ae_map_iff] at this
      exact this
    refine Measure.rnDeriv_eq_zero_of_mutuallySingular ?_ Measure.AbsolutelyContinuous.rfl
    exact hf.mutuallySingular_map (μ.mutuallySingular_singularPart ν)

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M : Type w
inst✝ : L.Structure M
α : Type w'
ie : IsEmpty α
⊢ ((LHom.id L).sumElim (LHom.ofIsEmpty (constantsOn α) L)).comp (L.lhomWithConstants α) = LHom.id L

Tactic:
rw [lhomWithConstants, LHom.sumElim_comp_inl]

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
t : L.Term α
⊢ (t.substFunc fun {n} ↦ Functions.term) = t

Tactic:
induction t

Goal state after:
case var
L : Language
α : Type u'
a✝ : α
⊢ ((var a✝).substFunc fun {n} ↦ Functions.term) = var a✝

case func
L : Language
α : Type u'
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
_ts_ih✝ : ∀ (a : Fin l✝), ((_ts✝ a).substFunc fun {n} ↦ Functions.term) = _ts✝ a
⊢ ((func _f✝ _ts✝).substFunc fun {n} ↦ Functions.term) = func _f✝ _ts✝
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : L.HomClass F M N
g : F
t : L.Term α
v : α → M
⊢ Term.realize (⇑g ∘ v) t = g (Term.realize v t)

Tactic:
induction t

Goal state after:
case var
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : L.HomClass F M N
g : F
v : α → M
a✝ : α
⊢ Term.realize (⇑g ∘ v) (var a✝) = g (Term.realize v (var a✝))

case func
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : L.HomClass F M N
g : F
v : α → M
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
_ts_ih✝ : ∀ (a : Fin l✝), Term.realize (⇑g ∘ v) (_ts✝ a) = g (Term.realize v (_ts✝ a))
⊢ Term.realize (⇑g ∘ v) (func _f✝ _ts✝) = g (Term.realize v (func _f✝ _ts✝))
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
ι : Sort u_3
S : ι → L.Substructure M
⊢ ↑(⨅ i, S i) = ⋂ i, ↑(S i)

Tactic:
by
  simp only [iInf, coe_sInf, Set.biInter_range]

Goal state after: