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

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

Tactic:
rw [mk_le_mk_iff] at h

Goal state after:
case mpr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
i : ι
a b : α i
hab : a ≤ b
h : ¬b ≤ a
⊢ ⟨i, a⟩ < ⟨i, b⟩
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → PartialOrder (α i)
⊢ ∀ (a b : (i : ι) × α i), a ≤ b → b ≤ a → a = b

Tactic:
rintro _ _ ⟨i, a, b, hab⟩ ⟨_, _, _, hba⟩
      exact congr_arg (Sigma.mk _ ·) <| hab.antisymm hba

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

Goal state before:
pp: α : Type u
a : α
s : WSeq α
⊢ (fun x ↦ a :: x) <$> s.toList =
    List.cons a <$>
      Computation.corec
        (fun x ↦
          match Seq.destruct x.2 with
          | none => Sum.inl x.1.reverse
          | some (none, s') => Sum.inr (x.1, s')
          | some (some a, s') => Sum.inr (a :: x.1, s'))
        ([], s)

Tactic:
rfl

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

Goal state before:
pp: case none
α : Type u
s : Seq α
⊢ (match
      match Option.map (fun a' ↦ (a', (some <$> s).tail)) (some <$> none) with
      | none => Sum.inl none
      | some (none, s') => Sum.inr s'
      | some (some a, s') => Sum.inl (some (a, s')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b =>
      Sum.inr
        (Computation.corec
          (fun s ↦
            match Option.map (fun a' ↦ (a', Seq.tail s)) (Seq.get? s 0) with
            | none => Sum.inl none
            | some (none, s') => Sum.inr s'
            | some (some a, s') => Sum.inl (some (a, s')))
          b)) =
    Sum.inl (Option.map (fun a ↦ (a, some <$> s.tail)) none)

Tactic:
rfl

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

Goal state before:
pp: case none
α : Type u
s : Seq α
⊢ Computation.pure (Option.map (Prod.fst ∘ fun a ↦ (a, ↑s.tail)) none) = Computation.pure none

Tactic:
rfl

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

Goal state before:
pp: case some
α : Type u
s : Seq α
val✝ : α
⊢ Computation.pure (Option.map (Prod.fst ∘ fun a ↦ (a, ↑s.tail)) (some val✝)) = Computation.pure (some val✝)

Tactic:
rfl

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

Goal state before:
pp: case nil
α : Type u
⊢ nil = some <$> Seq.nil

Tactic:
rfl

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

Goal state before:
pp: case none
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
a✝ : γ
⊢ Option.map (g ∘ f) none = some a✝ ↔ (Option.map g ∘ Option.map f) none = some a✝

Tactic:
rfl

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

Goal state before:
pp: case some
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
val✝ : α
a✝ : γ
⊢ Option.map (g ∘ f) (some val✝) = some a✝ ↔ (Option.map g ∘ Option.map f) (some val✝) = some a✝

Tactic:
rfl

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

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

pp: case bisim.cons
α : Type u
β : Type v
f : α → β
s : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
x✝ : α
s✝ : WSeq α
h : c1 = (map f (cons x✝ s✝)).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (cons x✝ s✝).destruct
⊢ BisimO (fun c1 c2 ↦ ∃ s, c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    (map f (cons x✝ s✝)).destruct.destruct
    (Computation.map (Option.map (Prod.map f (map f))) (cons x✝ s✝).destruct).destruct

pp: case bisim.think
α : Type u
β : Type v
f : α → β
s : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
s✝ : WSeq α
h : c1 = (map f s✝.think).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s✝.think.destruct
⊢ BisimO (fun c1 c2 ↦ ∃ s, c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    (map f s✝.think).destruct.destruct (Computation.map (Option.map (Prod.map f (map f))) s✝.think.destruct).destruct

Tactic:
case nil | cons => simp

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

Goal state before:
pp: s : String
h : s ≠ ""
⊢ s.toList = Legacy.front s :: (Legacy.drop s 1).toList

Tactic:
by
    obtain ⟨l, rfl⟩ := s.exists_eq_ofList
    match l with
    | [] => simp at h
    | c::cs => simp [Legacy.front, Pos.Raw.get, Pos.Raw.utf8GetAux]

Goal state after:
Module: Mathlib.Data.SubtypeNeLift

Goal state before:
pp: case neg
ι : Type u_1
inst✝ : DecidableEq ι
M : ι → Type u_2
φ : (i : ι) → M i
i₀ i : ι
h : ¬i = i₀
⊢ subtypeNeLift i₀ (fun i ↦ φ ↑i) (φ i₀) i = φ i

Tactic:
subtypeNeLift_of_neq _ _ _ _ h

Goal state after:
case neg
ι : Type u_1
inst✝ : DecidableEq ι
M : ι → Type u_2
φ : (i : ι) → M i
i₀ i : ι
h : ¬i = i₀
⊢ φ ↑⟨i, h⟩ = φ i
Module: Mathlib.Data.WSeq.Basic

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

pp: case cons
α : Type u
s t : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
x✝ : α
s✝ : WSeq α
h : c1 = (nil.append (cons x✝ s✝)).destruct ∧ c2 = nil.destruct.bind (destruct_append.aux (cons x✝ s✝))
⊢ BisimO (fun c1 c2 ↦ ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (nil.append (cons x✝ s✝)).destruct.destruct (nil.destruct.bind (destruct_append.aux (cons x✝ s✝))).destruct

pp: case think
α : Type u
s t : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
s✝ : WSeq α
h : c1 = (nil.append s✝.think).destruct ∧ c2 = nil.destruct.bind (destruct_append.aux s✝.think)
⊢ BisimO (fun c1 c2 ↦ ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (nil.append s✝.think).destruct.destruct (nil.destruct.bind (destruct_append.aux s✝.think)).destruct

Tactic:
case nil | cons => simp

Goal state after:
case think
α : Type u
s t : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
s✝ : WSeq α
h : c1 = (nil.append s✝.think).destruct ∧ c2 = nil.destruct.bind (destruct_append.aux s✝.think)
⊢ BisimO (fun c1 c2 ↦ ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (nil.append s✝.think).destruct.destruct (nil.destruct.bind (destruct_append.aux s✝.think)).destruct
Module: Mathlib.Data.WSeq.Basic

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

pp: case cons
α : Type u
S : WSeq (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux
x✝ : WSeq α
s✝ : WSeq (WSeq α)
⊢ BisimO (fun c1 c2 ↦ c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux)
    (cons x✝ s✝).join.destruct.destruct ((cons x✝ s✝).destruct.bind destruct_join.aux).destruct

pp: case think
α : Type u
S : WSeq (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux
s✝ : WSeq (WSeq α)
⊢ BisimO (fun c1 c2 ↦ c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux)
    s✝.think.join.destruct.destruct (s✝.think.destruct.bind destruct_join.aux).destruct

Tactic:
case nil | cons => simp

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

Goal state before:
pp: case nil
α : 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 α)
⊢ 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) []) =
    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 []) [] 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

Goal state after:
Module: Mathlib.Data.Sym.NatCard

Goal state before:
pp: α : Type u_1
⊢ Nat.card { a // ¬a.IsDiag } = (Nat.card α).choose 2

Tactic:
by
  cases finite_or_infinite α
  · obtain ⟨_⟩ := nonempty_fintype α; let := Classical.decEq α
    simp_rw [Nat.card_eq_fintype_card]
    exact card_subtype_not_diag
  · simp

Goal state after:
Module: Mathlib.Data.Tree.Traversable

Goal state before:
pp: case nil
α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
⊢ pure nil = Functor.Comp.mk (pure (pure nil))

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Tree.Traversable

Goal state before:
pp: case node
α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
v : α
l r : BinaryTree α
hl : traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) l = Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g l)
hr : traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) r = Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g r)
⊢ Functor.Comp.mk
      ((fun a x x_1 ↦ node <$> f a <*> traverse f x <*> traverse f x_1) <$> g v <*> traverse g l <*> traverse g r) =
    Functor.Comp.mk ((fun a x x_1 ↦ traverse f (node a x x_1)) <$> g v <*> traverse g l <*> traverse g r)

Tactic:
rfl

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

Goal state before:
pp: case refine_2.inl.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
val✝¹ : α₁
val✝ : β₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inl val✝¹ = inl a₁ → inr val✝ = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inl val✝¹ = inr a₂ → inr val✝ = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inl val✝¹) (inr val✝) = ∅

Tactic:
rfl

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

Goal state before:
pp: case refine_2.inr.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
val✝¹ : α₂
val✝ : β₁
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inr val✝¹ = inl a₁ → inl val✝ = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inr val✝¹ = inr a₂ → inl val✝ = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inr val✝¹) (inl val✝) = ∅

Tactic:
rfl

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

Goal state before:
pp: case zero
α : Type u_1
n : ℕ
val : α
⊢ replicate (0 + 1) val = (replicate 0 val).snoc val

Tactic:
rfl

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

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
σ : Type u_3
n : ℕ
x : α
xs : Vector α n
f : α → σ → σ × β
s : σ
⊢ mapAccumr f (nil.snoc x) s =
    let q := f x s;
    let r := mapAccumr f nil q.1;
    (r.1, r.2.snoc q.2)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.W.Constructions

Goal state before:
pp: f : Natβ Natα.succ → WType Natβ
⊢ (fun x ↦ f ()) = f

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.W.Constructions

Goal state before:
pp: γ : Type u
x : γ
f : Listβ γ (Listα.cons x) → WType (Listβ γ)
⊢ (fun x ↦ f PUnit.unit) = f

Tactic:
rfl

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 : ℕ
f : α → β → σ → σ × γ
f' : β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a b s = f' b s
s : σ
⊢ mapAccumr₂ f nil nil s = mapAccumr f' nil s

Tactic:
rfl

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 : ℕ
f : α → β → σ → σ × γ
f' : α → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a b s = f' a s
s : σ
⊢ mapAccumr₂ f nil nil s = mapAccumr f' nil s

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Vector3

Goal state before:
pp: case refine_1
α : Type u_1
n : ℕ
a : α
v : Vector3 α n
j : Fin2 (n + 1)
⊢ insert a v fz fz = (a :: v) fz

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Vector3

Goal state before:
pp: case refine_2
α : Type u_1
n : ℕ
a : α
v : Vector3 α n
j : Fin2 (n + 1)
n✝ : Fin2 n
⊢ insert a v fz n✝.fs = (a :: v) n✝.fs

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Vector3

Goal state before:
pp: case refine_1
α : Type u_1
m n : ℕ
a : α
t : Vector3 α m
v : Vector3 α n
i : Fin2 (n + 1)
e✝ : n + 1 + m = n + m + 1
e : n + 1 + 0 = n + 0 + 1
⊢ insert a ([] +-+ v) (Eq.recOn e (i.add 0)) = Eq.recOn e ([] +-+ insert a v i)

Tactic:
rfl

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

Goal state before:
pp: case refine_4.inr.inl
α₁ : 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 γ₂
val✝¹ : α₂
val✝ : β₁
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inr val✝¹ = inl a₁ → inl val✝ = inl b₁ → f₁ a₁ b₁ = ∅) ∧
    (∀ (a₁ : α₁) (b₂ : β₂), inr val✝¹ = inl a₁ → inl val✝ = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
      ∀ (a₂ : α₂) (b₂ : β₂), inr val✝¹ = inr a₂ → inl val✝ = inr b₂ → f₂ a₂ b₂ = ∅
⊢ sumLexLift f₁ f₂ g₁ g₂ (inr val✝¹) (inl val✝) = ∅

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
a₁ a₂ : α
⊢ Icc (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Icc a₁ a₂))

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
a₁ a₂ : α
⊢ Ico (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Ico a₁ a₂))

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
a₁ a₂ : α
⊢ Ioc (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Ioc a₁ a₂))

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
a₁ a₂ : α
⊢ Ioo (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Ioo a₁ a₂))

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
b₁ b₂ : β
⊢ Icc (inrₗ b₁) (inrₗ b₂) = map toLex.toEmbedding (map Embedding.inr (Icc b₁ b₂))

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
b₁ b₂ : β
⊢ Ico (inrₗ b₁) (inrₗ b₂) = map toLex.toEmbedding (map Embedding.inr (Ico b₁ b₂))

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
b₁ b₂ : β
⊢ Ioc (inrₗ b₁) (inrₗ b₂) = map toLex.toEmbedding (map Embedding.inr (Ioc b₁ b₂))

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder α
inst✝² : LocallyFiniteOrder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot β
b₁ b₂ : β
⊢ Ioo (inrₗ b₁) (inrₗ b₂) = map toLex.toEmbedding (map Embedding.inr (Ioo b₁ b₂))

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Fintype α
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : OrderBot α
inst✝³ : OrderBot β
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
⊢ LocallyFiniteOrder.toLocallyFiniteOrderBot = instLocallyFiniteOrderBot

Tactic:
rfl

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁷ : Fintype α
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : OrderBot α
inst✝³ : OrderBot β
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
⊢ LocallyFiniteOrder.toLocallyFiniteOrderBot = instLocallyFiniteOrderBot
Module: Mathlib.Dynamics.Ergodic.Action.Regular

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulRightInvariant
⊢ ErgodicSMul Gᵐᵒᵖ G μ

Tactic:
by
  refine ⟨fun {s} hsm hs ↦ ?_⟩
  suffices (∃ᵐ x ∂μ, x ∈ s) → ∀ᵐ x ∂μ, x ∈ s by
    simp only [eventuallyConst_set, ← not_frequently]
    exact or_not_of_imp this
  intro hμs
  obtain ⟨a, has, ha⟩ : ∃ a ∈ s, ∀ᵐ b ∂μ, (a * b ∈ s ↔ a ∈ s) := by
    refine (hμs.and_eventually ?_).exists
    rw [ae_ae_comm]
    · exact ae_of_all _ fun b ↦ (hs ⟨b⟩).mem_iff
    · exact ((hsm.preimage <| measurable_fst.mul measurable_snd).mem.iff
        (hsm.preimage measurable_fst).mem).setOf
  simpa [has] using (quasiMeasurePreserving_mul_left μ a⁻¹).ae ha

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

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

Tactic:
rfl

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

Goal state before:
pp: M : Type u_1
inst✝⁹ : TopologicalSpace M
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : SMul M X
inst✝³ : ContinuousSMul M X
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul M X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : Dense {g | (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s}
this✝¹ : MeasurableSpace M := borel M
this✝ : BorelSpace M
⊢ ∀ (g : M), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s

Tactic:
dense_iff_closure_eq,

Goal state after:
M : Type u_1
inst✝⁹ : TopologicalSpace M
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : SMul M X
inst✝³ : ContinuousSMul M X
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul M X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : closure[inst✝⁹] {g | (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s} = univ
this✝¹ : MeasurableSpace M := borel M
this✝ : BorelSpace M
⊢ ∀ (g : M), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: X : Type u_2
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : R1Space X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
M : Type u_3
inst✝⁶ : Monoid M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : MulAction M X
inst✝³ : ContinuousSMul M X
g : M
hg : DenseRange fun x ↦ g ^ x
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul M X μ
this✝¹ : MeasurableSpace M := borel M
this✝ : BorelSpace M
s : Set X
hsm : MeasurableSet s
hs : (fun x ↦ g • x) ⁻¹' s = s
n : ℕ
⊢ g ^ n ∈ {g | (fun x ↦ g • x) ⁻¹' s = s}

Tactic:
mem_ofPred,

Goal state after:
X : Type u_2
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : R1Space X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
M : Type u_3
inst✝⁶ : Monoid M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : MulAction M X
inst✝³ : ContinuousSMul M X
g : M
hg : DenseRange fun x ↦ g ^ x
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul M X μ
this✝¹ : MeasurableSpace M := borel M
this✝ : BorelSpace M
s : Set X
hsm : MeasurableSet s
hs : (fun x ↦ g • x) ⁻¹' s = s
n : ℕ
⊢ (fun x ↦ g ^ n • x) ⁻¹' s = s
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x ↦ g * x) μ
a : G
h : a ∉ closure[inst✝⁴] (range fun x ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst✝⁴] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ m, g ^ m • V
hso : IsOpen[inst✝⁴] s
hsne : s.Nonempty
⊢ ∀ (i : ℤ) ⦃a_1 : G⦄, a_1 ∈ g ^ i • V → a_1 ∉ a • V

Tactic:
rintro m _ ⟨x, hx, rfl⟩ ⟨y, hy, hxy⟩

Goal state after:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x ↦ g * x) μ
a : G
h : a ∉ closure[inst✝⁴] (range fun x ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst✝⁴] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ m, g ^ m • V
hso : IsOpen[inst✝⁴] s
hsne : s.Nonempty
m : ℤ
x : G
hx : x ∈ V
y : G
hy : y ∈ V
hxy : (fun x ↦ a • x) y = (fun x ↦ g ^ m • x) x
⊢ False
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: case inl
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x ↦ g * x) μ
a : G
h✝ : a ∉ closure[inst✝⁴] (range fun x ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst✝⁴] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ m, g ^ m • V
hso : IsOpen[inst✝⁴] s
hsne : s.Nonempty
hd : Disjoint s (a • V)
hgs : (fun x ↦ g * x) ⁻¹' s = s
h : μ s = 0
⊢ False

Tactic:
exact hso.measure_ne_zero _ hsne h

Goal state after: