mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by

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:
by

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:
by

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✝
s1 : WSeq α
s2 : WSeq β
x✝ :
  (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2
s✝ : WSeq α
t✝ : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1✝ : s1 = s✝.append S.join
h2✝ : s2 = t✝.append T.join
st : LiftRel R s✝ t✝
ST : LiftRel (LiftRel R) S T
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
a : α
s : WSeq α
b : β
t : WSeq β
h1 : R a b
h2 : LiftRel R s t
⊢ Computation.LiftRel
    (LiftRelO R fun s1 s2 ↦
      ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T)
    (destruct_append.aux S.join (some (a, s))) (destruct_append.aux T.join (some (b, t)))

Tactic:
by

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

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

Goal state before:
pp: α : 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 α)
⊢ parallel.aux2 (List.map (map f) l) = lmap f (rmap (List.map (map f)) (parallel.aux2 l))

Tactic:
by

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✝
s1 : WSeq α
s2 : WSeq β
x✝¹ :
  (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2
s : WSeq α
t : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1 : s1 = s.append S.join
h2 : s2 = t.append T.join
st : LiftRel R s t
ST : LiftRel (LiftRel R) S T
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
x✝ : LiftRelO R (LiftRel R) none none
⊢ Computation.LiftRel
    (LiftRelO R fun s1 s2 ↦
      ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T)
    (destruct_append.aux S.join none) (destruct_append.aux T.join none)

Tactic:
by

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✝
s1 : WSeq α
s2 : WSeq β
x✝ :
  (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2
s : WSeq α
t : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1 : s1 = s.append S.join
h2 : s2 = t.append T.join
st : LiftRel R s t
ST : LiftRel (LiftRel R) S T
⊢ Computation.LiftRel
    (LiftRelO R fun s1 s2 ↦
      ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T)
    s1.destruct s2.destruct

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
s1 s2 : WSeq α
f1 f2 : α → WSeq β
h1 : s1 ~ʷ s2
h2 : ∀ (a : α), f1 a ~ʷ f2 a
a b : α
h : a = b
⊢ LiftRel Eq (f1 a) (f2 b)

Tactic:
by

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

Goal state before:
pp: α : Type u
s : WSeq α
⊢ (ret s).join ~ʷ s

Tactic:
by

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

Goal state before:
pp: α : Type u
s✝¹ s' s✝ : WSeq α
h✝ : (map ret s✝).join = s'
c1 c2 : Computation (Option (α × WSeq α))
h : ∃ s, c1 = (map ret s).join.destruct ∧ c2 = s.destruct
s : WSeq α
⊢ LiftRelAux (LiftRelO Eq fun s1 s2 ↦ (map ret s2).join = s1)
    (fun c1 c2 ↦ ∃ s, c1 = (map ret s).join.destruct ∧ c2 = s.destruct) (map ret s).join.destruct.destruct
    s.destruct.destruct

Tactic:
by

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

Goal state before:
pp: α : Type u
s : WSeq α
⊢ (map ret s).join ~ʷ s

Tactic:
by

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:
by

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:
by

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

Goal state before:
pp: α : Type u_1
k : ℕ
⊢ Nat.card (Sym α k) = (Nat.card α).multichoose k

Tactic:
by

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

Goal state before:
pp: α : Type u_1
k : ℕ
⊢ Nat.card (Sym α k) = (Nat.card α + k - 1).choose k

Tactic:
by

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:
by

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:
by

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

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

Goal state before:
pp: α : 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 α)
⊢ BisimO
    (fun c1 c2 ↦
      ∃ l S,
        c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S))
    (map f (corec parallel.aux1 (l, S))).destruct
    (corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)).destruct

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M₀ : Type u_2
inst✝¹ : CommMonoidWithZero M₀
inst✝ : NoZeroDivisors M₀
f : α →₀ M₀
⊢ ↑f.support.sym2 = map ⇑f ⁻¹' Function.support mul

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M₀ : Type u_2
inst✝ : CommMonoidWithZero M₀
f : α →₀ M₀
p : Sym2 α
hp : (map (⇑f) p).mul ≠ 0
⊢ p ∈ f.support.sym2

Tactic:
by

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

Goal state before:
pp: α : 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 β
t : BinaryTree α
⊢ traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) t = Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g t)

Tactic:
by

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

Goal state before:
pp: α : Type u
S : WSeq (Computation α)
h : S.head ~> none
x✝ : (parallel S).Terminates
a : α
m : a ∈ parallel S
c : Computation α
cs : c ∈ S
right✝ : a ∈ c
n : ℕ
nm : some c ∈ S.get? n
⊢ False

Tactic:
let ⟨c', h'⟩ := WSeq.head_some_of_get?_some nm

Goal state after:
α : Type u
S : WSeq (Computation α)
h : S.head ~> none
x✝ : (parallel S).Terminates
a : α
m : a ∈ parallel S
c : Computation α
cs : c ∈ S
right✝ : a ∈ c
n : ℕ
nm : some c ∈ S.get? n
c' : Computation α
h' : some c' ∈ S.head
⊢ False
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
S : WSeq (Computation α)
h : S.head ~> none
x✝ : (parallel S).Terminates
a : α
m : a ∈ parallel S
⊢ False

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun c ↦ map (fun a ↦ (a, c)) c) S
⊢ S = WSeq.map (map fun c ↦ c.1) T

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
t : BinaryTree α
⊢ traverse (pure ∘ f) t = pure (map f t)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ s.bind (ret ∘ f) ~ʷ map f s

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
a : α
f : α → WSeq β
⊢ (ret a).bind f ~ʷ f a

Tactic:
by

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:
by

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:
by

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

Goal state before:
pp: α : 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)
s : WSeq α
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
h1 : s1 = s.append (S.append SS.join).join
h2 : s2 = s.append (S.join.append (map join SS).join)
⊢ s1.destruct = (s.append (S.append SS.join).join).destruct

Tactic:
by

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

Goal state before:
pp: α : 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)
s : WSeq α
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
h1 : s1 = s.append (S.append SS.join).join
h2 : s2 = s.append (S.join.append (map join SS).join)
⊢ s2.destruct = (s.append (S.join.append (map join SS).join)).destruct

Tactic:
by

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

Goal state before:
pp: α : Type u_1
F : Type u → Type u_3
G : Type u → Type u_4
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
β : Type u
f : α → F β
t : BinaryTree α
⊢ (fun {α} ↦ η.app α) (traverse f t) = traverse (η.app β ∘ f) t

Tactic:
by

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

Goal state before:
pp: α : 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 α))
h :
  ∃ s S SS,
    c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct
s : WSeq α
S : WSeq (WSeq α)
SS : WSeq (WSeq (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)
    (s.append (S.append SS.join).join).destruct.destruct (s.append (S.join.append (map join SS).join)).destruct.destruct

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun c ↦ map (fun a ↦ (a, c)) c) S
this✝ : S = WSeq.map (map fun c ↦ c.1) T
pe : parallel S = map (fun c ↦ c.1) (parallel T)
h' : a ∈ map (fun c ↦ c.1) (parallel T)
this : (parallel T).Terminates
a' : α
c : Computation α
e : (parallel T).get = (a', c)
⊢ a ∈ c ∧ c ∈ S

Tactic:
by

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

Goal state before:
pp: α : Type u
SS : WSeq (WSeq (WSeq α))
⊢ SS.join.join ~ʷ (map join SS).join

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
⊢ C a

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : WSeq α
f : α → WSeq β
g : β → WSeq γ
⊢ (s.bind f).bind g ~ʷ s.bind ((fun y ↦ y.bind g) ∘ f)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : WSeq α
f : α → WSeq β
g : β → WSeq γ
⊢ (s.bind f).bind g ~ʷ s.bind fun x ↦ (f x).bind g

Tactic:
by

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

Goal state before:
pp: α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
⊢ c ∈ sumLift₂ f g a b ↔
    (∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂

Tactic:
by

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

Goal state before:
pp: α : Type u
S T : WSeq (Computation α)
a : α
h1 : ∀ s ∈ S, s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ t ∈ T, t ~> a := (parallel_congr_lem H).mp h1
a' : α
h : a' ∈ parallel S
⊢ a' ∈ parallel T

Tactic:
by

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

Goal state before:
pp: α : Type u
S T : WSeq (Computation α)
a : α
h1 : ∀ s ∈ S, s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ t ∈ T, t ~> a := (parallel_congr_lem H).mp h1
a' : α
h : a' ∈ parallel T
⊢ a' ∈ parallel S

Tactic:
by

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

Goal state before:
pp: α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₁ : γ₁
⊢ inl c₁ ∈ sumLift₂ f g a b ↔ ∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ c₁ ∈ f a₁ b₁

Tactic:
by

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

Goal state before:
pp: α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₂ : γ₂
⊢ inr c₂ ∈ sumLift₂ f g a b ↔ ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ c₂ ∈ g a₂ b₂

Tactic:
by

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 γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
h : sumLift₂ f g a b = ∅
⊢ (∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → g a₂ b₂ = ∅

Tactic:
constructor <;>
    · rintro a b rfl rfl
      exact map_eq_empty.1 h

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

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

Tactic:
by

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

Goal state before:
pp: α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
⊢ (sumLift₂ f g a b).Nonempty ↔
    (∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ (f a₁ b₁).Nonempty) ∨ ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ (g a₂ b₂).Nonempty

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
x : α
xs : Vector α n
⊢ (x ::ᵥ xs).reverse = xs.reverse.snoc x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
x : α
xs : Vector α n
⊢ (xs.snoc x).reverse = x ::ᵥ xs.reverse

Tactic:
by

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

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

Tactic:
by

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:
by

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:
by

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:
by

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:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n : ℕ
x : α
xs : Vector α n
f : α → β
⊢ map f (xs.snoc x) = (map f xs).snoc (f x)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
n : ℕ
x : α
xs : Vector α n
ys : Vector β n
f : α → β → σ
y : β
⊢ map₂ f (xs.snoc x) (ys.snoc y) = (map₂ f xs ys).snoc (f x y)

Tactic:
by

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 : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × φ
x : α
y : β
⊢ mapAccumr₂ f (xs.snoc x) (ys.snoc y) s =
    let q := f x y s;
    let r := mapAccumr₂ f xs ys q.1;
    (r.1, r.2.snoc q.2)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α n
x✝ : ∃ i h, v.toList.get ⟨i, h⟩ = a
i : ℕ
hi : i < v.toList.length
h : v.toList.get ⟨i, hi⟩ = a
⊢ i < n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α n
x✝ : ∃ i h, v.toList.get (Fin.cast ⋯ ⟨i, h⟩) = a
i : ℕ
hi : i < n
h : v.toList.get (Fin.cast ⋯ ⟨i, hi⟩) = a
⊢ i < v.toList.length

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α n
⊢ a ∈ v.toList ↔ ∃ i, v.get i = a

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
a a' : α
v : Vector α n
⊢ a' ∈ (a ::ᵥ v).toList ↔ a' = a ∨ a' ∈ v.toList

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
⊢ a ∈ v.toList ↔ a = v.head ∨ a ∈ v.tail.toList

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α n
ha : a ∈ v.tail.toList
⊢ a ∈ v.toList

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n : ℕ
b : β
v : Vector α n
f : α → β
⊢ b ∈ (map f v).toList ↔ ∃ a, a ∈ v.toList ∧ f a = b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
b : β
v : Vector α 0
f : α → β
⊢ ¬b ∈ (map f v).toList

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n : ℕ
b : β
v : Vector α (n + 1)
f : α → β
⊢ b ∈ (map f v).toList ↔ f v.head = b ∨ ∃ a, a ∈ v.tail.toList ∧ f a = b

Tactic:
by

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:
by

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
⊢ (zipWith f x y).get i = f (x.get i) (y.get i)

Tactic:
by

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
⊢ (zipWith f x y).tail = zipWith f x.tail y.tail

Tactic:
by

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

Goal state before:
pp: α₁ : 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 : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
⊢ c ∈ sumLexLift f₁ f₂ g₁ g₂ a b ↔
    (∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
      (∃ a₁ b₂ c₁, a = inl a₁ ∧ b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ a₁ b₂ c₂, a = inl a₁ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
          ∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.UInt

Goal state before:
pp: n : UInt8
⊢ 2 ^ 8 < 55296

Tactic:
by

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

Goal state before:
pp: α₁ : 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 : β₁ ⊕ β₂
c₁ : γ₁
⊢ inl c₁ ∈ sumLexLift f₁ f₂ g₁ g₂ a b ↔
    (∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨ ∃ a₁ b₂, a = inl a₁ ∧ b = inr b₂ ∧ c₁ ∈ g₁ a₁ b₂

Tactic:
by

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

Goal state before:
pp: α₁ : 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 : β₁ ⊕ β₂
c₂ : γ₂
⊢ inr c₂ ∈ sumLexLift f₁ f₂ g₁ g₂ a b ↔
    (∃ a₁ b₂, a = inl a₁ ∧ b = inr b₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨ ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ c₂ ∈ f₂ a₂ b₂

Tactic:
by

Goal state after: