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

Goal state before:
pp: α : 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 α)
⊢ S.think.join.destruct.tail = S.join.destruct ∧
    (S.think.destruct.bind destruct_join.aux).tail = S.destruct.bind destruct_join.aux

Tactic:
simp

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

Goal state before:
pp: case bisim.nil.nil
α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
⊢ Seq.BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join)
    (Seq.destruct (nil.append (map f nil.join))) (Seq.destruct (nil.append (map (map f) nil).join))

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
S✝ S : WSeq (WSeq α)
⊢ map f S.join = nil.append (map f S.join)

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
S✝ S : WSeq (WSeq α)
⊢ (map (map f) S).join = nil.append (map (map f) S).join

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
⊢ map f S.join = nil.append (map f S.join)

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
⊢ (map (map f) S).join = nil.append (map (map f) S).join

Tactic:
simp

Goal state after:
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
⊢ S.join = nil.append S.join

Tactic:
simp

Goal state after:
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
⊢ T.join = nil.append T.join

Tactic:
simp

Goal state after:
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
⊢ LiftRel R nil nil

Tactic:
simp

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

Goal state before:
pp: case inl
α : 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)
l : List (Computation α)
S : WSeq (Computation α)
this : parallel.aux2 (List.map (map f) l) = lmap f (rmap (List.map (map f)) (parallel.aux2 l))
a : α
⊢ match
    match
      match
        match
          match Sum.inl a with
          | Sum.inl a => Sum.inl a
          | Sum.inr b =>
            Sum.inr
              (match Seq.destruct S with
              | none => (b, Seq.nil)
              | some (none, S') => (b, S')
              | some (some c, S') => (c :: b, S')) with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (corec parallel.aux1 b) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (map f b) with
    | Sum.inl a => Sum.inl (f a)
    | Sum.inr b => Sum.inr b,
    match
      match lmap f (rmap (List.map (map f)) (Sum.inl a)) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (match Seq.destruct (WSeq.map (map f) S) with
          | none => (b, Seq.nil)
          | some (none, S') => (b, S')
          | some (some c, S') => (c :: b, S')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec parallel.aux1 b) with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' =>
    ∃ l S, s = map f (corec parallel.aux1 (l, S)) ∧ s' = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
  | x, x_1 => False

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case nil.nil.nil
α : Type u
S T : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
⊢ LiftRelAux (LiftRelO Eq fun s1 s2 ↦ ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
    (fun c1 c2 ↦ ∃ s S T, c1 = (s.append (S.append T).join).destruct ∧ c2 = (s.append (S.join.append T.join)).destruct)
    nil.join.destruct.destruct nil.join.destruct.destruct

Tactic:
simp

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

Goal state before:
pp: case inr.zero
α : Type u_1
h✝ : Infinite α
⊢ Nat.card (Sym α 0) = (Nat.card α).multichoose 0

Tactic:
simp

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

Goal state before:
pp: case inr.succ
α : Type u_1
h✝ : Infinite α
n✝ : ℕ
⊢ Nat.card (Sym α (n✝ + 1)) = (Nat.card α).multichoose (n✝ + 1)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Infinite α
e : ℕ ↪ α := Infinite.natEmbedding α
n : ℕ
⊢ ¬s(e 0, e (n + 1)).IsDiag

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Infinite α
e : ℕ ↪ α := Infinite.natEmbedding α
x✝¹ x✝ : ℕ
⊢ (fun n ↦ ⟨s(e 0, e (n + 1)), ⋯⟩) x✝¹ = (fun n ↦ ⟨s(e 0, e (n + 1)), ⋯⟩) x✝ → x✝¹ = x✝

Tactic:
simp

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

Goal state before:
pp: case nil.nil.cons.refine_1
α : Type u
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
s : WSeq α
T : WSeq (WSeq α)
⊢ (s.append T.join).destruct = (s.append (nil.append T).join).destruct

Tactic:
simp

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

Goal state before:
pp: case nil.nil.cons.refine_2
α : Type u
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
s : WSeq α
T : WSeq (WSeq α)
⊢ (s.append T.join).destruct = (s.append (nil.join.append T.join)).destruct

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case inr
α : Type u_1
h✝ : Infinite α
⊢ Nat.card (Sym2 α) = (Nat.card α + 1).choose 2

Tactic:
simp

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

Goal state before:
pp: case nil.nil.think.refine_1
α : Type u
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : WSeq (WSeq α)
⊢ T.join.destruct = (nil.append (nil.append T).join).destruct

Tactic:
simp

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

Goal state before:
pp: case nil.nil.think.refine_2
α : Type u
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : WSeq (WSeq α)
⊢ T.join.destruct = (nil.append (nil.join.append T.join)).destruct

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Sym.Sym2.Finsupp

Goal state before:
pp: case mk
α : Type u_1
M₀ : Type u_2
inst✝¹ : CommMonoidWithZero M₀
inst✝ : NoZeroDivisors M₀
f : α →₀ M₀
x✝ : Sym2 α
a b : α
⊢ Quot.mk (Rel α) (a, b) ∈ ↑f.support.sym2 ↔ Quot.mk (Rel α) (a, b) ∈ map ⇑f ⁻¹' Function.support mul

Tactic:
simp

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

Goal state before:
pp: case nil.think.refine_1
α : Type u
S✝ T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T S : WSeq (WSeq α)
⊢ (nil.append (S.think.append T).join).destruct.tail = (nil.append (S.append T).join).destruct

Tactic:
simp

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

Goal state before:
pp: case nil.think.refine_2
α : Type u
S✝ T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T S : WSeq (WSeq α)
⊢ (nil.append (S.think.join.append T.join)).destruct.tail = (nil.append (S.join.append T.join)).destruct

Tactic:
simp

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

Goal state before:
pp: α : Type u
SS : WSeq (WSeq (WSeq α))
⊢ SS.join.join = nil.append (nil.append SS.join).join

Tactic:
simp

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

Goal state before:
pp: α : Type u
SS : WSeq (WSeq (WSeq α))
⊢ (map join SS).join = nil.append (nil.join.append (map join SS).join)

Tactic:
simp

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

Goal state before:
pp: case nil.nil.nil
α : Type u
SS : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
⊢ LiftRelAux
    (LiftRelO Eq fun s1 s2 ↦
      ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun c1 c2 ↦
      ∃ s S SS,
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    nil.join.join.destruct.destruct (map join nil).join.destruct.destruct

Tactic:
simp

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

Goal state before:
pp: case nil.nil.cons.refine_1
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
⊢ (cons S SS).join.join.destruct.tail = (nil.append (S.append SS.join).join).destruct

Tactic:
simp

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

Goal state before:
pp: case nil.nil.cons.refine_2
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
⊢ (map join (cons S SS)).join.destruct.tail = (nil.append (S.join.append (map join SS).join)).destruct

Tactic:
simp

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

Goal state before:
pp: case nil.nil.think.refine_1
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
⊢ SS.think.join.join.destruct.tail = (nil.append (nil.append SS.join).join).destruct

Tactic:
simp

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

Goal state before:
pp: case nil.nil.think.refine_2
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
⊢ (map join SS.think).join.destruct.tail = (nil.append (nil.join.append (map join SS).join)).destruct

Tactic:
simp

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

Goal state before:
pp: case nil.think.refine_1
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
S : WSeq (WSeq α)
⊢ (nil.append (S.think.append SS.join).join).destruct.tail = (nil.append (S.append SS.join).join).destruct

Tactic:
simp

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

Goal state before:
pp: case nil.think.refine_2
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
S : WSeq (WSeq α)
⊢ (nil.append (S.think.join.append (map join SS).join)).destruct.tail =
    (nil.append (S.join.append (map join SS).join)).destruct

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n✝ : ℕ
x : α
s : σ
xs : Vector α n✝
C : {n : ℕ} → Vector α n → Sort u_5
n : ℕ
v : Vector α n
nil : C Vector.nil
snoc : {n : ℕ} → (xs : Vector α n) → (x : α) → C xs → C (xs.snoc x)
⊢ C v.reverse.reverse = C v

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n✝¹ : ℕ
x✝ : α
s : σ
xs✝ : Vector α n✝¹
C : {n : ℕ} → Vector α n → Sort u_5
n✝ : ℕ
v : Vector α n✝
nil : C Vector.nil
snoc : {n : ℕ} → (xs : Vector α n) → (x : α) → C xs → C (xs.snoc x)
n : ℕ
x : α
xs : Vector α n
r : C xs.reverse
⊢ C (xs.reverse.snoc x) = C (x ::ᵥ xs).reverse

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n✝ : ℕ
x : α
s : σ
xs : Vector α n✝
C : {n : ℕ} → Vector α n → Vector β n → Sort u_5
n : ℕ
v : Vector α n
w : Vector β n
nil : C Vector.nil Vector.nil
snoc : {n : ℕ} → (xs : Vector α n) → (ys : Vector β n) → (x : α) → (y : β) → C xs ys → C (xs.snoc x) (ys.snoc y)
⊢ C v.reverse.reverse w.reverse.reverse = C v w

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n✝¹ : ℕ
x✝ : α
s : σ
xs✝ : Vector α n✝¹
C : {n : ℕ} → Vector α n → Vector β n → Sort u_5
n✝ : ℕ
v : Vector α n✝
w : Vector β n✝
nil : C Vector.nil Vector.nil
snoc : {n : ℕ} → (xs : Vector α n) → (ys : Vector β n) → (x : α) → (y : β) → C xs ys → C (xs.snoc x) (ys.snoc y)
n : ℕ
x : α
y : β
xs : Vector α n
ys : Vector β n
r : C xs.reverse ys.reverse
⊢ C (xs.reverse.snoc x) (ys.reverse.snoc y) = C (x ::ᵥ xs).reverse (y ::ᵥ ys).reverse

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
a : α
⊢ ¬a ∈ nil.toList

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
⊢ (List.zipWith f ↑x ↑y).length = n

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
i : Fin n
⊢ (List.zipWith f ↑x ↑y).get (Fin.cast ⋯ i) = f ((↑x).get (Fin.cast ⋯ i)) ((↑y).get (Fin.cast ⋯ i))

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Vector3

Goal state before:
pp: case refine_1
α : Type u_1
n : ℕ
a b : α
v : Vector3 α n
i : Fin2 (n + 1)
j✝ : Fin2 (n + 1 + 1)
j : Fin2 (n + 1)
⊢ (a :: b :: v)
      (match fz with
      | fz => fz
      | k.fs => k.fs.fs) =
    (a :: v) fz

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Vector3

Goal state before:
pp: case refine_2
α : Type u_1
n : ℕ
a b : α
v : Vector3 α n
i : Fin2 (n + 1)
j✝ : Fin2 (n + 1 + 1)
j : Fin2 (n + 1)
⊢ ∀ (n_1 : Fin2 n),
    (a :: b :: v)
        (match n_1.fs with
        | fz => fz
        | k.fs => k.fs.fs) =
      (a :: v) n_1.fs

Tactic:
simp

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 β
⊢ ∀ (a b x : α ⊕ β), x ∈ sumLift₂ Icc Icc a b ↔ a ≤ x ∧ x ≤ b

Tactic:
simp

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 β
⊢ ∀ (a b x : α ⊕ β), x ∈ sumLift₂ Ico Ico a b ↔ a ≤ x ∧ x < b

Tactic:
simp

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 β
⊢ ∀ (a b x : α ⊕ β), x ∈ sumLift₂ Ioc Ioc a b ↔ a < x ∧ x ≤ b

Tactic:
simp

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 β
⊢ ∀ (a b x : α ⊕ β), x ∈ sumLift₂ Ioo Ioo a b ↔ a < x ∧ x < b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : LocallyFiniteOrderBot β
⊢ ∀ (a x : α ⊕ β), x ∈ Sum.elim (fun x ↦ map Embedding.inl (Iic x)) (fun x ↦ map Embedding.inr (Iic x)) a ↔ x ≤ a

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : LocallyFiniteOrderBot β
⊢ ∀ (a x : α ⊕ β), x ∈ Sum.elim (fun x ↦ map Embedding.inl (Iio x)) (fun x ↦ map Embedding.inr (Iio x)) a ↔ x < a

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderTop β
⊢ ∀ (a x : α ⊕ β), x ∈ Sum.elim (fun x ↦ map Embedding.inl (Ici x)) (fun x ↦ map Embedding.inr (Ici x)) a ↔ a ≤ x

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderTop β
⊢ ∀ (a x : α ⊕ β), x ∈ Sum.elim (fun x ↦ map Embedding.inl (Ioi x)) (fun x ↦ map Embedding.inr (Ioi x)) a ↔ a < x

Tactic:
simp

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 b x : α ⊕ₗ β),
    x ∈ map toLex.toEmbedding (sumLexLift Icc Icc (fun a x ↦ Ici a) (fun x ↦ Iic) (ofLex a) (ofLex b)) ↔ a ≤ x ∧ x ≤ b

Tactic:
simp

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 b x : α ⊕ₗ β),
    x ∈ map toLex.toEmbedding (sumLexLift Ico Ico (fun a x ↦ Ici a) (fun x ↦ Iio) (ofLex a) (ofLex b)) ↔ a ≤ x ∧ x < b

Tactic:
simp

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 b x : α ⊕ₗ β),
    x ∈ map toLex.toEmbedding (sumLexLift Ioc Ioc (fun a x ↦ Ioi a) (fun x ↦ Iic) (ofLex a) (ofLex b)) ↔ a < x ∧ x ≤ b

Tactic:
simp

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 b x : α ⊕ₗ β),
    x ∈ map toLex.toEmbedding (sumLexLift Ioo Ioo (fun a x ↦ Ioi a) (fun x ↦ Iio) (ofLex a) (ofLex b)) ↔ a < x ∧ x < b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : LocallyFiniteOrderBot β
⊢ ∀ (a x : α ⊕ₗ β),
    x ∈
        ((Sum.elim (fun x ↦ map (Embedding.inl.trans toLex.toEmbedding) (Iic x)) fun x ↦
              map toLex.toEmbedding (univ.disjSum (Iic x))) ∘
            ⇑ofLex)
          a ↔
      x ≤ a

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : LocallyFiniteOrderBot β
⊢ ∀ (a x : α ⊕ₗ β),
    x ∈
        ((Sum.elim (fun x ↦ map (Embedding.inl.trans toLex.toEmbedding) (Iio x)) fun x ↦
              map toLex.toEmbedding (univ.disjSum (Iio x))) ∘
            ⇑ofLex)
          a ↔
      x < a

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : Fintype β
inst✝ : LocallyFiniteOrderTop β
⊢ ∀ (a x : α ⊕ₗ β),
    x ∈
        ((Sum.elim (fun x ↦ map toLex.toEmbedding ((Ici x).disjSum univ)) fun x ↦
              map (Embedding.inr.trans toLex.toEmbedding) (Ici x)) ∘
            ⇑ofLex)
          a ↔
      a ≤ x

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : Fintype β
inst✝ : LocallyFiniteOrderTop β
⊢ ∀ (a x : α ⊕ₗ β),
    x ∈
        ((Sum.elim (fun x ↦ map toLex.toEmbedding ((Ioi x).disjSum univ)) fun x ↦
              map (Embedding.inr.trans toLex.toEmbedding) (Ioi x)) ∘
            ⇑ofLex)
          a ↔
      a < x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.ZMod.Coprime

Goal state before:
pp: a : ℤ
p : ℕ
pp : Fact (Nat.Prime p)
⊢ ↑a = 0 ↔ ¬IsCoprime (↑p) a

Tactic:
(Nat.prime_iff_prime_int.1 pp.1).coprime_iff_not_dvd,

Goal state after:
a : ℤ
p : ℕ
pp : Fact (Nat.Prime p)
⊢ ↑a = 0 ↔ ¬¬↑p ∣ a
Module: Mathlib.Data.WSeq.Defs

Goal state before:
pp: α : Type u
s✝ : WSeq α
s1 s2 : Computation ℕ
l : List α
a : α
s : WSeq α
h :
  s1 =
      Computation.corec
        (fun x ↦
          match x with
          | (n, s) =>
            match Seq.destruct s with
            | none => Sum.inl n
            | some (none, s') => Sum.inr (n, s')
            | some (some val, s') => Sum.inr (n + 1, s'))
        (l.length, cons a s) ∧
    s2 =
      Computation.map List.length
        (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, cons a s))
⊢ Computation.corec
      (fun x ↦
        match Seq.destruct x.2 with
        | none => Sum.inl x.1
        | some (none, s') => Sum.inr (x.1, s')
        | some (some val, s') => Sum.inr (x.1 + 1, s'))
      (l.length + 1, s) =
    Computation.corec
      (fun x ↦
        match Seq.destruct x.2 with
        | none => Sum.inl x.1
        | some (none, s') => Sum.inr (x.1, s')
        | some (some val, s') => Sum.inr (x.1 + 1, s'))
      ((a :: l).length, s)

Tactic:
simp

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

Goal state before:
pp: α : Type u
s✝ : WSeq α
s1 s2 : Computation ℕ
l : List α
a : α
s : WSeq α
h :
  s1 =
      Computation.corec
        (fun x ↦
          match x with
          | (n, s) =>
            match Seq.destruct s with
            | none => Sum.inl n
            | some (none, s') => Sum.inr (n, s')
            | some (some val, s') => Sum.inr (n + 1, s'))
        (l.length, cons a s) ∧
    s2 =
      Computation.map List.length
        (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, cons a s))
⊢ Computation.map List.length
      (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'))
        (a :: l, s)) =
    Computation.map List.length
      (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'))
        (a :: l, s))

Tactic:
simp

Goal state after: